Tutorial Animation Tips

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

Installation

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:

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 two solutions to overcome this.

Increasing MAX_OPERATIONS

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.