Tutorial CSP First Step - Revision history

Ivaylo Dobrikov: /* Other Features */

2016-02-22T16:02:45Z

Other Features

← Older revision		Revision as of 16:02, 22 February 2016
Line 73:		Line 73:
	ProB should respond: <tt>Formula TRUE. No counterexample found.</tt>		ProB should respond: <tt>Formula TRUE. No counterexample found.</tt>
	Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.		Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.
	It is also possible to perform various refinement checks and other assertion checks (see [http://stups.hhu.de/ProB/w/Checking_CSP_Assertions ~~Checkin_CSP_Assertions~~]).		It is also possible to perform various refinement checks and other assertion checks (see [http://stups.hhu.de/ProB/w/Checking_CSP_Assertions Checking CSP Assertions' tutorial]).
	The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:		For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|200px]]		[[file:ProB_CSPBusStatespace.png\|center\|\|200px]]

Ivaylo Dobrikov: /* Other Features */

2015-08-30T10:13:08Z

Other Features

← Older revision		Revision as of 10:13, 30 August 2015
Line 73:		Line 73:
	ProB should respond: <tt>Formula TRUE. No counterexample found.</tt>		ProB should respond: <tt>Formula TRUE. No counterexample found.</tt>
	Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.		Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.
	It is also possible to perform ~~trace~~ refinement checks (see [~~[Refinement_Checking]~~]).		It is also possible to perform various refinement checks and other assertion checks (see [http://stups.hhu.de/ProB/w/Checking_CSP_Assertions Checkin_CSP_Assertions]).
	The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:		For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|200px]]		[[file:ProB_CSPBusStatespace.png\|center\|\|200px]]

Michael Leuschel: /* Error Highlighting */

2015-08-11T08:01:19Z

Error Highlighting

← Older revision		Revision as of 08:01, 11 August 2015
Line 61:		Line 61:
	ProB will report the following error:		ProB will report the following error:

	! Mismatch in number of arguments for synchronisation on channel alight37B with extra argument(s):		Mismatch in number of arguments for synchronisation on channel alight37B with extra argument(s):
	! 1		1
	### Line: 11, Column: 30		### Line: 11, Column: 30

Michael Leuschel: /* Error Highlighting */

2015-08-11T08:00:51Z

Error Highlighting

← Older revision		Revision as of 08:00, 11 August 2015
Line 61:		Line 61:
	ProB will report the following error:		ProB will report the following error:

	Mismatch in number of arguments for channel ~~synchronisation~~:		! Mismatch in number of arguments for synchronisation on channel alight37B with extra argument(s):
	~~Channel:ExtraArgs = alight37B:[int(~~1)]		! 1
	### Line: 11, Column: 30		### Line: 11, Column: 30

Michael Leuschel: /* Other Features */

2015-08-10T15:29:50Z

Other Features

← Older revision		Revision as of 15:29, 10 August 2015
Line 76:		Line 76:
	The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:		For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|~~400px~~]]		[[file:ProB_CSPBusStatespace.png\|center\|\|200px]]

Michael Leuschel: /* Other Features */

2015-08-10T15:29:37Z

Other Features

← Older revision		Revision as of 15:29, 10 August 2015
Line 75:		Line 75:
	It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).		It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).
	The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "~~View~~ Statespace" in the "~~Animate~~" menu, the following graph will be displayed:		For example, if you select the command "Statespace" in the "Visualize" menu (after having fully explored the system), the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]		[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]

Michael Leuschel at 15:22, 10 August 2015

2015-08-10T15:22:11Z

← Older revision		Revision as of 15:22, 10 August 2015
Line 24:		Line 24:
	** The "History" pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.		** The "History" pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.

	Now, double click on "<tt>MAIN</tt>" process in the "Enabled Operations" Pane. This has the effect of computing the events offered by <tt>MAIN</tt>. The ~~lower half of the~~ ProB window should now look as follows (the upper half will remain unchanged):		Now, double click on "<tt>MAIN</tt>" process in the "Enabled Operations" Pane. This has the effect of computing the events offered by <tt>MAIN</tt>. The ProB window should now look as follows (the upper half will remain unchanged):

	[[file:ProB_CSPAfterInit.png\|center\|\|~~700px~~]]		[[file:ProB_CSPAfterInit.png\|center\|\|500px]]

Ivaylo Dobrikov at 13:19, 28 July 2015

2015-07-28T13:19:50Z

← Older revision		Revision as of 13:19, 28 July 2015
Line 1:		Line 1:
	[Category:User Manual]]		[Category:User Manual]

Joy Clark: grammar and punctuation

2011-04-18T12:51:15Z

grammar and punctuation

Michael Leuschel: /* Other Features */

2010-10-11T08:28:43Z

Other Features

← Older revision		Revision as of 08:28, 11 October 2010
Line 70:		Line 70:
	== Other Features ==		== Other Features ==

	You can check more sophisticated temporal properties using the LTL model checker of ProB; see the [[LTL_Model_Checking\|corresponding part of the tutorial]]. For example, you can try and validate the following LTL formula <tt>G([~~board37a~~] => F [alight37B])</tt>.		You can check more sophisticated temporal properties using the LTL model checker of ProB; see the [[LTL_Model_Checking\|corresponding part of the tutorial]]. For example, you can try and validate the following LTL formula <tt>G([board37A] => F [alight37B])</tt>.
			ProB should respond: <tt>Formula TRUE. No counterexample found.</tt>
			Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.
	It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).		It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).
	The state space visualisation features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualisation features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "View Statespace" in the "Animate" menu, the following graph will be displayed:		For example, if you select the command "View Statespace" in the "Animate" menu, the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]		[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]

← Older revision		Revision as of 12:51, 18 April 2011
Line 22:		Line 22:
	** The "State Properties" pane contains information about the current state of the specification. We will explain the contents of this pane in more detail later.		** The "State Properties" pane contains information about the current state of the specification. We will explain the contents of this pane in more detail later.
	** The Pane called "Enabled Operations" contains a list of events that your CSP specification offers. At the very first step you have to choose a process to animate. If your CSP specification contains a MAIN process (as is the case in buses.csp), only this process will be shown.		** The Pane called "Enabled Operations" contains a list of events that your CSP specification offers. At the very first step you have to choose a process to animate. If your CSP specification contains a MAIN process (as is the case in buses.csp), only this process will be shown.
	** The History pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.		** The "History" pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.

	Now, double click on "<tt>MAIN</tt>" process in the "Enabled Operations" Pane. This has the effect of computing the events offered by <tt>MAIN</tt>. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):		Now, double click on "<tt>MAIN</tt>" process in the "Enabled Operations" Pane. This has the effect of computing the events offered by <tt>MAIN</tt>. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):
Line 35:		Line 35:

	By repeatedly single clicking on the event you can cycle through the various locations that contributed to the event. To execute an event, simply double-click on it.		By repeatedly single clicking on the event you can cycle through the various locations that contributed to the event. To execute an event, simply double-click on it.
	Try this out for yourself: double-click on <tt>tau(int_choice_left)</tt> and then single-click on the <tt>board37</tt> event which is offered. This time the event is a ~~synchronisation~~ of two events(note that ProB uses a different colour for highlighting the source locations). The source highlighting should look as follows:		Try this out for yourself: double-click on <tt>tau(int_choice_left)</tt> and then single-click on the <tt>board37</tt> event which is offered. This time the event is a synchronization of two events(note that ProB uses a different colour for highlighting the source locations). The source highlighting should look as follows:
	[[file:ProB_CSPAfterBoardSingleClick.png\|center\|\|500px]]		[[file:ProB_CSPAfterBoardSingleClick.png\|center\|\|500px]]

Line 58:		Line 58:
	[] alight37A -> STOP)		[] alight37A -> STOP)

	Now save and reload the specification and again choose the "Model Check..." command in the Verify menu. Now uncheck the "~~FInd~~ Deadlocks" ~~checkbox~~ and press "Model Check".		Now save and reload the specification and again choose the "Model Check..." command in the Verify menu. Now uncheck the "Find Deadlocks" check-box and press "Model Check".
	ProB will report the following error:		ProB will report the following error:

Line 74:		Line 74:
	Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.		Similarly, you can check the absence of divergence by checking the LTL formula <tt>G not G [tau]</tt>.
	It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).		It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).
	The state space ~~visualisation~~ features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].		The state space visualization features of ProB are also available for CSP; see [[State_Space_Visualization\|the corresponding part of the tutorial]].
	For example, if you select the command "View Statespace" in the "Animate" menu, the following graph will be displayed:		For example, if you select the command "View Statespace" in the "Animate" menu, the following graph will be displayed:
	[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]		[[file:ProB_CSPBusStatespace.png\|center\|\|400px]]