Tutorial Setup Phases
We assume that you grasped the first steps of opening and animating a B machine as outlined in Tutorial First Step.
In this lesson, we examine more closely the various steps that ProB undertakes before a machine can be animated.
First, open the machine "Jukebox.mch" which can be found in the SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples folder. The main ProB window should look more or less as follows:
In general, before the operations of a machine can be applied, ProB needs to traverse three phases:
- 1. Loading the machine and determining the sizes of the deferred sets, as well as fixing the values of MININT and MAXINT.
- 2. Setting up the constants of the machine, such that the PROPERTIES and CONSTRAINTS are satisfied.
- 3. Performing a valid initialisation of the machine.
This process is illustrated in the following picture:
We now examine these phases on the Jukebox machine in more detail
1. Loading
Here ProB parses and type checks the machine.
Then it will fix the values of MININT and MAXINT. There are two ways you can influence this:
- by using "Animation Preferences..." command in the "Preferences" menu and modifying the corresponding preferences.
- by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form SET_PREF_MAXINT == 5 or SET_PREF_MININT == -2147483648.
Note that these preferences determine the elements of the sets INT (implementable integers), NAT (implementable natural numbers) and NAT1. In addition, they are used to control the enumeration of variables of type INTEGER</tt) (mathematical integers), in case a definite value cannot be inferred from the machine.
Afterwards, ProB will determine the cardinality of all deferred sets (such as TRACK in the Jukebox machine).There are several ways you can influence this:
- by using "Animation Preferences..." command in the "Preferences" menu and modifying the preference "Size of unspecified deferred sets in SETS section".
- by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form scope_TRACK == 5 (where TRACK is the name of the deferred set you wish to influence and 5 is its desired cardinality). This will override the default size.
- by including a predicate of the form card(TRACK)=5 in the PROPERTIES or CONSTRAINTS section of your machine.
As you can see above in the "State Properties" pane, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:
2. SETUP_CONSTANTS
In this phase ProB will try and find values for the constants and parameters of your machine, so that the PROPERTIES and CONSTRAINTS are true. Note that ProB will not (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.
ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labelled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.
By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:
3. INITIALISATION
In this phase the values for the constants have been found, but the initial values of the variables still remain to be determined. For this, ProB will try to execute the INITIALISATION substitution. As we can see above, ProB has found just one possible way to initialise the variables credit and playset. Double-clicking on INITIALISATION(0,{}) leads the animator into a state where all constants and variables are valued, and where the INVARIANT can be checked and operations can be applied:
Let us conclude by choosing the "View Statespace" command in the "Animate" menu:
As you can see, there is only one root node: in order to change MAXINT, MININT or the deferred set sizes you have to reload the machine. There are, however, three different ways to setup the constants. The model checker will explore all of them. Let us choose the "Model Check..." command in the "Verify" menu and then press on the "Model Check" button.
If we now choose the "View Statespace" command in the "Animate" menu, we get the following picture:
We can see (or guess at least) that ProB has validated the machine and explored the statespace not just for limit=2 but also for limit=1 and limit=3.