Tutorial Setup Phases

We assume that you grasped the first steps of opening and animating a B machine as outlined in [[Tutorial First Steps].

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: