Tutorial Animation Tips: Difference between revisions

No edit summary
No edit summary
Line 4: Line 4:
Make sure you have the Lift.mch model from the first part of the tutorial: [[Tutorial First Step|Starting ProB and first animation steps]].
Make sure you have the Lift.mch model from the first part of the tutorial: [[Tutorial First Step|Starting ProB and first animation steps]].


== Installation ==
== Operation with many solutions for the parameters ==


Add the following operation to the Lift model:
Add the following operation to the Lift model:
Line 34: Line 34:


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


 
[[file:ProB_Lift_ExecuteOperationMenu.png|center||350px]]
[[file:ProB_ExecuteOperation.png|center||350px]]


After that, select the <tt>jump</tt> operation  
After that, select the <tt>jump</tt> operation  


[[file:ProB_Lift_ExecuteOperation_OpSelectionDialog.png|center||350px]]
[[file:ProB_ExecuteOperation.png|center||350px]]


and you will be provided with the following dialog:
and you will be provided with the following dialog:

Revision as of 15:03, 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:


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

ProB Lift MAX OPERATIONS.png

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