Animation
|
Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
The animation facilities of ProB allow users to gain confidence in their specifications. These features try to be as user-friendly as possible (e.g., the user does not have to guess the right values for the operation arguments or choice variables, and he uses the mouse to operate the animation).
Basic Animation
When the B specification is opened, the syntax and type checker analyses it and, if a syntax or type error is detected, it is then reported, highlighted in yellow in the specification. Furthermore, if the B specification contains features of B that are not supported by ProB or constraints that are not satisfiable, an appropriate message is displayed. When these checks are passed, the B machine is loaded, but it has no state yet. ProB will then display the operations that can be performed in the Enabled Operations pane. These operations can be of two types described below.
Operations from the B Machine
These operations are the ones whose preconditions and guards are satisfiable in the current state. The parameter values that make true the precondition and guard are automatically computed by ProB, and one entry for the operation is displayed in the Enabled Operations pane for each group of parameter values. Each parameter value is displayed as a set between curly brackets, and the group of parameter values are enclosed between brackets after the operation name.
The computation of the parameter values greatly facilitates the work of the user, as he does not have to enumerate the possible values and check the preconditions and guards. This computation process involves trying to solve the various constraints imposed on the parameter values in the preconditions and guards.
HINT: If no operation is enabled, the state of the B machine corresponds to a deadlock
Virtual Operations
There are three particular operations that correspond to specific tasks performed by ProB:
- SETUP_CONSTANTS This virtual operation corresponds to the assignment of values to the constants of the B machine. These values must satisfy the PROPERTIES clause. ProB automatically computes the possible values and displays one initialise constants virtual operation for each possible group of of constant values. If the PROPERTIES clause is not satisfiable, an error message is displayed.
- INITIALISATION This virtual operation plays the same role as initialise constants but for initial values of the variables (clauses VARIABLES and INITIALISATION) instead of constants. If the INITIALISATION clause does not satisfy the constraints in the INVARIANT clause, an error message is displayed.
Note, there are also forward and backward buttons in the Operations pane. These enable the user to explore interactively the behaviour of the B machine.
Animating the B machine
If the B machine has constants, one or several initialise constants operations are displayed. The user selects one of these operations, then the corresponding values of the constants are displayed in the State Properties pane and the selected initialise constants operation is displayed in the History pane. In the State Properties pane, functions and relations are displayed by indicating each of their tuples on a different line.
At that point during the animation (also reached directly if the B machine has no constants), ProB displays one or several initialise machine operations. The user selects one of these operations, and then the machine is in its initial state. The initial values of the variables are displayed in the State Properties pane and the initialise machine operation selected is displayed in the History. From that moment on, an indicator of the status of the invariant is displayed at the top of the State Properties pane and the backtrack operation is displayed at the bottom of the Enabled Operations pane. The invariant status indicator is invariant ok if the invariant is satisfied or invariant violated if the invariant is violated.
From there, the user selects operations among the enabled ones. If the selected operation is backtrack, the last selected operation is removed from the top of the History pane and the previous state is displayed in the State Properties pane. If the operation was not backtrack, it is added to the History pane, the effect of the operation are computed and the state is updated in the State Properties pane
At each point during the animation process, several useful commands displaying various information on the B machine are available in the Analyse menu. The Compute Coverage command opens a window that displays three groups of information:
- NODES This is the number of nodes (i.e. states) explored so far; there are four kinds of nodes:
- live: states already computed by ProB;
- deadlocked: states where the B machine is deadlocked;
- invariant violated: states where the invariant is violated;
- open: states that are reachable from the live nodes by an enabled operation.
- COVERED OPERATIONS This is the number of operations that have been enabled so far, including the initialise machine operations.
- UNCOVERED OPERATIONS This is the names of the operations that have not been enabled so far.
The Analyse Invariant command opens a window displaying the truth values of the various conjuncts of the invariant of the B machine, while the Analyse Properties command plays the same role but for the constant properties and the Analyse Assertions plays this role for the assertions.
Animation Preferences
The animation process in ProB can be configured via several preferences set in the preference window Preferences|Animation Preferences.
First, the preference Show effect of initialisation and setup constants in operation name toggles the display of the values of the constants and the initial values of the variables when the corresponding virtual operations are shown in the Enabled Operations pane.
The preference Nr of Initialisations shown determines the number of maximum initialise machine operations that ProB should compute. Similarly, the preference Max Number of Enablings shown sets the maximum number of groups of parameter values computed for each operation of the B machine.
The preference Check invariant will toggle the display of the invariant status indicator in the State Properties pane.
Other Animation Features
Several other commands are provided by ProB in the Animate menu for animating B specifications. The Reset command will set the state of the machine to the root, as if the machine has just been opened, i.e. when the initialise constants or initialise machine operations are displayed in the Enabled Operations pane. The Random Animation(10) command operates a sequence of 10 randomly chosen operations from the B specification. The variant Random Animation enables to specify the number of operation to operate randomly. In the File menu, the command Save State stores the current state of the B machine, which can then be reloaded with the command Load Saved State.