Also see the following tutorials:

• Tutorial First Step
• Tutorial Animation Tips
• Tutorial Setup Phases
• Tutorial Understanding the Complexity of B Animation

General Presentation

The ProB Main Window

The menu bar contains the various commands to access the features of ProB. It includes the traditional "File" menu with a sub-menu "Recent Files" to quickly access the files previously opened in ProB. Notice the commands "Open\Save", "Reopen\Save" and "Reopen"; the latter reopens the currently opened file and reinitializes the state of the animation and the model checking processes completely. The "About" menu provides help on the tool and includes a command to check if an update is available on the ProB website. By default, ProB starts with a limited set of commands in the Beginner mode. The Normal mode gives access to more features and can be set in the menu "Preferences|User Mode".

Under the menu bar, the main window contains four panes:

• In the top pane, the specification of the B machine is displayed with the syntax highlighted and can also be edited by typing directly in this pane; you can find out more about this editor and how to use external editors in our wiki page on editors.
• At the bottom, the animation window is composed of three panes which display at the current point during the animation:
  1. The current state of the B machine (State Properties), listing the current values of the machine variables;
  2. The enabled operations (Enabled Operations), listing the operations whose preconditions and guards are true in this state (see here for what the different colours mean);
  3. The history of operations leading to this state (History).

Preferences

The "Preferences" menu allows the various features of ProB to be configured. When ProB is started for the first time, it creates a file prob_preferences.pl that stores those preferences.

• The sub-menu "Font" changes the font size of the B specification displayed in the main window.

The next three commands correspond to groups of preferences displayed in separate pop-up windows.

• The command "Animation Preferences" ... configures important aspects of ProB relative to the animation and model checking of the B specifications. These preferences influence directly the way ProB interprets the B specification and are described in "Animation and Visualisation", amongst others.

• The command "Graphical Viewer Preferences" ... allows the user to set the options of the visualization tool used by ProB and the shapes and colors used to display the nodes of the state space.

• The command "Syntax Highlight Preferences" ... allows the user to activate the syntax highlight of the B specification in the main window and also to select the various colors corresponding to the syntactic elements of the B notation.

IMPORTANT: Changes in the animation preferences take effect only after reloading the machine.

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

The Analyse menu

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:
  1. live: states already computed by ProB;
  2. deadlocked: states where the B machine is deadlocked;
  3. invariant violated: states where the invariant is violated;
  4. 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.

Colours of enabled operations

The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is taken:

blue

The operation does not change the state (behaves like skip).

green

The operation leads to a new, not yet explored state.

red

The operation leads to a state where the invariant is violated.

orange

The operation leads to a deadlock state, i.e. a state where no operation is enabled.

black

Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither an invariant violating or deadlock state.

Controlling ProB Preferences

ProB provides a variety of preferences to control its behaviour. A list of the most important preferences can be found in the manual page for probcli. We also have a separate manual page about setting the sizes of deferred sets.

Setting Preferences in a B machine

This only works for classical B models. For a preference P you can add the following definition to the DEFINITIONS section of the main machine:

SET_PREF_P == VAL

This will set the preference P to the value VAL for this model only.

Setting Preferences from the command-line

You can set a preference P to a value VAL for a particular run of probcli by adding the command-line switch -p P VAL, e.g.,

probcli -p P VAL mymachine.mch -mc 9999

You can obtain a list of preferences by calling probcli as follows:

probcli -help -v

You can use a preference file generated by ProB Tcl/Tk:

    -prefs FILE

This will import all preferences from this file, as set by ProB Tcl/Tk.

You can also set the scope for a particular deferred set GS using the following command-line switch:

    -card GS Val

Setting Preferences from ProB Tcl/Tk

ProB Tcl/Tk stores your preferences settings in a file ProB_Preferences.pl.

The ProB preferences are grouped into various categories. In the "Preferences" Menu you can modify the preferences for each category:

For example, if you choose the graphical viewer preferences you will get this dialog: