Line 20: | Line 20: | ||

The orange "max" button to the left of "Enabled Operation" tells you that not all possible parameter values for the operations were computed. | 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 | There are several solutions to overcome this. | ||

=== Increasing MAX_OPERATIONS === | === Increasing MAX_OPERATIONS === | ||

Line 56: | Line 56: | ||

The above predicate, <tt>level>96 & level mod 2 =0</tt> would select the same value <tt>98</tt> for level. | The above predicate, <tt>level>96 & level mod 2 =0</tt> would select the same value <tt>98</tt> for level. | ||

When there are multiple solutions, ProB will only execute the operation for the first solution found. | 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. | |||

You add the following lines to your model: | |||

DEFINITIONS | |||

SET_PREF_RANDOM_ENUMERATION_ORDER == TRUE | |||

Alternatively, you can set this preference using the "Advanced Preferences" pane in the Preferences menu. | |||

[[file:ProB_Lift_MAX_OPERATIONS.png|center||350px]] | |||

=== Using Constraint-Based Validation Techniques === | |||

You can also use the constraint solver to construct sequences which are of interest to you. |

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

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 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.

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

After that, select the `jump` operation

and you will be provided with the following dialog:

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

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

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.

You can also tell ProB to try and perform random enumerations. You add the following lines to your model:

DEFINITIONS SET_PREF_RANDOM_ENUMERATION_ORDER == TRUE

Alternatively, you can set this preference using the "Advanced Preferences" pane in the Preferences menu.

You can also use the constraint solver to construct sequences which are of interest to you.