Eval Console: Difference between revisions

No edit summary
No edit summary
Line 20: Line 20:


You can use the up and down arrow keys to navigate to earlier predicates or expressions you have entered.
You can use the up and down arrow keys to navigate to earlier predicates or expressions you have entered.
If you change the state, then the expressions and predicates are evaluated in that state.
For example, if you execute the operations Push(RANGE3), Push(RANGE1), Push(RANGE2), then a transcript of using the console is as follows:
[[File:StackConstructiveProBEvalConsoleFull2.png|center|500px]]

Revision as of 16:44, 27 February 2012

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

  • 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:
StackConstructiveProBEvalCommand.png

This will bring up a new window, the "Eval Console":


StackConstructiveProBEvalConsoleEmpty.png


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:

StackConstructiveProBEvalConsoleFull.png

You can use the up and down arrow keys to navigate to earlier predicates or expressions you have entered.

If you change the state, then the expressions and predicates are evaluated in that state. For example, if you execute the operations Push(RANGE3), Push(RANGE1), Push(RANGE2), then a transcript of using the console is as follows:

StackConstructiveProBEvalConsoleFull2.png