Eval Console - Revision history

David Geleßus: Update download page link

2021-02-04T15:50:08Z

Update download page link

← Older revision		Revision as of 15:50, 4 February 2021
Line 1:		Line 1:
	For this tutorial, load for example the file <tt>StackConstructive.mch</tt> included in the <tt>examples/Tutorial</tt> directory of the [~~http://www.stups.uni-duesseldorf.de/ProB/index.php5/~~Download ProB distribution] (this example is also discussed in the [[Tutorial Modeling Infinite Datatypes]]).		For this tutorial, load for example the file <tt>StackConstructive.mch</tt> included in the <tt>examples/Tutorial</tt> directory of the [[Download\|ProB distribution]] (this example is also discussed in the [[Tutorial Modeling Infinite Datatypes]]).

	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.

Michael Leuschel at 16:39, 8 July 2014

2014-07-08T16:39:29Z

← Older revision		Revision as of 16:39, 8 July 2014
Line 32:		Line 32:
	<pre>		<pre>
	>>> let x = 2**10		>>> let x = 2**10
	~~Expression Value =~~		1024
	1024
	>>> let y = x+x		>>> let y = x+x
	~~Expression Value =~~		2048
	2048
	>>> :b		>>> :b
	x = 1024		x = 1024
	y = 2048		y = 2048
	>>> {v\| v>x & v<y & v mod x = 1}		>>> {v\| v>x & v<y & v mod x = 1}
	~~Expression Value =~~		{1025}
	{1025}
	>>>		>>>
	</pre>		</pre>

Michael Leuschel at 16:38, 8 July 2014

2014-07-08T16:38:51Z

@@ Line 27: / Line 27: @@
 The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.
 We now also have made two versions of a [[ProB Logic Calculator|ProB Logic Calculator available online]].
 The second one works similarly to the Eval console above, but is not linked to any B machine. You can try it out directly on this page below:
 {{Template:shell2}}

Michael Leuschel at 08:43, 31 March 2012

2012-03-31T08:43:20Z

← Older revision		Revision as of 08:43, 31 March 2012
Line 28:		Line 28:
	The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.		The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.

	We now also have an online ~~version of~~ the console:		We now also have made two versions of a [[ProB Logic Calculator\|ProB Logic Calculator available online]].
	{{Template:~~shell~~}}		The second one works similarly to the Eval console above, but is not linked to any B machine. You can try it out directly on this page below:
			{{Template:shell2}}

Michael Leuschel at 11:37, 30 March 2012

2012-03-30T11:37:03Z

← Older revision		Revision as of 11:37, 30 March 2012
Line 27:		Line 27:

	The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.		The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.

			We now also have an online version of the console:
			{{Template:shell}}

Michael Leuschel at 18:13, 27 February 2012

2012-02-27T18:13:48Z

← Older revision		Revision as of 18:13, 27 February 2012
Line 25:		Line 25:

	[[File:StackConstructiveProBEvalConsoleFull2.png\|center\|500px]]		[[File:StackConstructiveProBEvalConsoleFull2.png\|center\|500px]]

			The console works the same way for Event-B models, Z and TLA specifications. However, in all those cases the Eval console uses the classical B parser and you have to use classical B syntax for entering predicates or expressions. The console also works in CSP mode and uses a CSP parser there.

Michael Leuschel at 16:48, 27 February 2012

2012-02-27T16:48:14Z

← Older revision		Revision as of 16:48, 27 February 2012
Line 1:		Line 1:
	For this tutorial, load for example the file <tt>StackConstructive.mch</tt> included in the <tt>examples/Tutorial</tt> directory of the [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download ProB distribution].		For this tutorial, load for example the file <tt>StackConstructive.mch</tt> included in the <tt>examples/Tutorial</tt> directory of the [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download ProB distribution] (this example is also discussed in the [[Tutorial Modeling Infinite Datatypes]]).

	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.

Michael Leuschel at 16:46, 27 February 2012

2012-02-27T16:46:44Z

← Older revision		Revision as of 16:46, 27 February 2012
Line 22:		Line 22:

	If you change the state, then the expressions and predicates are evaluated in that state.		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:		For example, if you execute the operations Push(RANGE3), Push(RANGE1), Push(RANGE2) by double-clicking on the respective lines in the "Enabled Operations" pane, then a transcript of using the console is as follows:

	[[File:StackConstructiveProBEvalConsoleFull2.png\|center\|500px]]		[[File:StackConstructiveProBEvalConsoleFull2.png\|center\|500px]]

Michael Leuschel at 16:44, 27 February 2012

2012-02-27T16:44:43Z

← Older revision		Revision as of 16:44, 27 February 2012
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]]

Michael Leuschel at 16:37, 27 February 2012

2012-02-27T16:37:22Z

← Older revision		Revision as of 16:37, 27 February 2012
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]]