Tutorial Animation Tips: Difference between revisions
No edit summary |
|||
| Line 36: | Line 36: | ||
For this, select the "Execute an Operation..." command in the animate menu: | For this, select the "Execute an Operation..." command in the animate menu: | ||
[[file:ProB_Lift_ExecuteOperationMenu.png|center|| | [[file:ProB_Lift_ExecuteOperationMenu.png|center||200px]] | ||
After that, select the <tt>jump</tt> operation | After that, select the <tt>jump</tt> operation | ||
| Line 44: | Line 44: | ||
and you will be provided with the following dialog: | and you will be provided with the following dialog: | ||
[[file:ProB_Lift_ExecuteOperation_Dialog.png|center|| | [[file:ProB_Lift_ExecuteOperation_Dialog.png|center||490px]] | ||
Type in <tt>98</tt> into the level field and hit the "Execute" button. | Type in <tt>98</tt> into the level field and hit the "Execute" button. | ||
[[file:ProB_Lift_OpPane_WithJump_Exec98.png|center|| | [[file:ProB_Lift_OpPane_WithJump_Exec98.png|center||450px]] | ||
Note: instead or in addition to providing concrete values, you can also specify a predicate that constrains the values of the parameters: | |||
[[file:ProB_Lift_ExecuteOperation_Dialog_Pred.png|center||490px]] | |||
Revision as of 15:05, 15 December 2013
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:
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.
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:
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:
