No edit summary |
No edit summary |
||
Line 2: | Line 2: | ||
After loading the file, double click on the green line "SETUP_CONSTANTS" in the "Enabled Operations" pane. Now double click on the green "INITIALISATION" line in the same pane. | After loading the file, double click on the green line "SETUP_CONSTANTS" in the "Enabled Operations" pane. Now double click on the green "INITIALISATION" line in the same pane. | ||
To start the "Eval..." interactive console you can either double-click any line in the "State Properties" pane or right-click (Control-Click on a Mac) on the "State Properties" pane and select the "Eval..." entry as shown below: | To start the "Eval..." interactive console you can either | ||
* use the "Eval..." command in the Analyse menu, | |||
* double-click any line in the "State Properties" pane or | |||
* right-click (Control-Click on a Mac) on the "State Properties" pane and select the "Eval..." entry as shown below: | |||
[[File:StackConstructiveProBEvalCommand.png|center|500px]] | [[File:StackConstructiveProBEvalCommand.png|center|500px]] |
For this tutorial, load for example the file StackConstructive.mch included in the examples/Tutorial directory of the ProB distribution.
After loading the file, double click on the green line "SETUP_CONSTANTS" in the "Enabled Operations" pane. Now double click on the green "INITIALISATION" line in the same pane. To start the "Eval..." interactive console you can either
This will bring up a new window, the "Eval Console":
You can now enter predicates or expressions and hit return or enter to evaluate them in the current state of the machine. Below is a small transcript:
You can use the up and down arrow keys to navigate to earlier predicates or expressions you have entered.