Tutorial Animation Tips

Make sure you have the Lift.mch model from the first part of the tutorial: Starting ProB and first animation steps.

Operation with many solutions for the parameters

Add the following operation to the Lift model:

jump(level) = PRE level : 0..99 THEN floor := level END

Now reload your model and initialise the machine. Your ProB window should now look as follows:

ProB LiftWithJump.png

As you can see, only 10 values for the level parameter of the jump operation are displayed in the "Enabled Operations" pane. The orange "max" button to the left of "Enabled Operation" tells you that not all possible parameter values for the operations were computed.

There are several solutions to overcome this.


First, you could increase the "MAX_OPERATIONS" preference of ProB by selecting the "Animation Preferences" command in the "Preferences" menu:


You should then set the preference "" to at least 101 and then re-load the B machine.

ProB Lift OpPane WithJump101.png

Executing an Operation by Predicate

The alternative is to provide the parameter value for level yourself. For this, select the "Execute an Operation..." command in the animate menu:

ProB Lift ExecuteOperationMenu.png

After that, select the jump operation

ProB ExecuteOperation.png

and you will be provided with the following dialog:

ProB Lift ExecuteOperation Dialog.png

Type in 98 into the level field and hit the "Execute" button.

ProB Lift OpPane WithJump Exec98.png

Note: instead or in addition to providing concrete values, you can also specify a predicate that constrains the values of the parameters:

ProB Lift ExecuteOperation Dialog Pred.png

The above predicate, level>96 & level mod 2 =0 would select the same value 98 for level. When there are multiple solutions, ProB will only execute the operation for the first solution found.

Using Random enumeration

You can also tell ProB to try and perform random enumerations. This feature is available in ProB 1.5.0 or newer. You add the following lines to your model:


Alternatively, you can set this preference using the "Advanced Preferences" pane in the Preferences menu. After reloading the machine you should see a picture similar to the following one:

ProB Lift Randomise.png

Using Constraint-Based Validation Techniques

You can also use the constraint solver to construct sequences which are of interest to you. Let us add the following operation to the lift model:

top_reached = PRE floor=99 THEN skip END

Now suppose we want to execute this new operation as early as possible. We can ask the constraint solver to generate a feasible sequence of operations. First select the "Find Sequence..." command in the Verify menu:


Now type in

 jump ; top_reached

in this dialog box:


ProB will then find a solution operation sequence for you and execute it:


Alternatively, you could for example use the constraint-based test-case generator to find for every operation the shortest trace that enables it. More details are available in the Tutorial_Model-Based_Testing section.