Tutorial First Model Checking - Revision history

Joy Clark: spellig and punctuation

2011-04-18T12:14:48Z

spellig and punctuation

Ingo Weigelt: fixed link to Tutorial First Step

2010-01-22T11:23:22Z

fixed link to Tutorial First Step

← Older revision		Revision as of 11:23, 22 January 2010
Line 2:		Line 2:


	We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First ~~Steps~~]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.		We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Step]]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.

	== Simple Model Checking ==		== Simple Model Checking ==

Michael Leuschel: /* View Statespace */

2010-01-18T15:14:35Z

View Statespace

← Older revision		Revision as of 15:14, 18 January 2010
Line 55:		Line 55:

	[[file:ProB_GraphicalViewerPreferences_Shapes.png\|center]]		[[file:ProB_GraphicalViewerPreferences_Shapes.png\|center]]

			You can obtain more information about the state space visualisation in the user manual: [[State Space Visualization]].

Michael Leuschel: /* View Statespace */

2010-01-18T15:05:42Z

View Statespace

← Older revision		Revision as of 15:05, 18 January 2010
Line 45:		Line 45:

	We can obtain a graphical visualization of the state space explored by ProB.		We can obtain a graphical visualization of the state space explored by ProB.
	For this, be sure that you have correctly [[Graphical Viewer\|installed and setup the graphical viewer as desribed in the user manual].		For this, be sure that you have correctly [[Graphical Viewer\|installed and setup the graphical viewer as desribed in the user manual]].
	Now, choose the "View Statespace" command in the "Animate" menu:		Now, choose the "View Statespace" command in the "Animate" menu:

Michael Leuschel: /* Simple Model Checking */

2010-01-18T15:04:38Z

Simple Model Checking

← Older revision		Revision as of 15:04, 18 January 2010
Line 18:		Line 18:
	[[file:ProB_LiftAfterModelCheck.png\|center\|\|700px]]		[[file:ProB_LiftAfterModelCheck.png\|center\|\|700px]]

	The red "'''KO'''" button in the "State Properties" pane tells us that the model checker has moved us into a state where the invariant is violated. The "History" pane tells us the sequence of operations that has led to this error.		The red "'''KO'''" button in the "State Properties" pane tells us that the model checker has moved us into a state where the invariant is violated. Indeed, the <tt>floor</tt> variable has taken up a negative value, while the invariant requires floor to be between 0 and 99.
			The "History" pane tells us the sequence of operations that has led to this error.
	(Note that this sequence is not necessarily the shortest sequence that leads to an error or to this error. However, by selecting "Breadth First" in the model check dialog above, one can ensure that the shortest paths are found.)		(Note that this sequence is not necessarily the shortest sequence that leads to an error or to this error. However, by selecting "Breadth First" in the model check dialog above, one can ensure that the shortest paths are found.)

Michael Leuschel at 15:03, 18 January 2010

2010-01-18T15:03:23Z

← Older revision		Revision as of 15:03, 18 January 2010
Line 52:		Line 52:

	Note: you can influence the colouring and shapes used by ProB, by selecting "Graphical Viewer Preferences..." in the "Preferences" menu.		Note: you can influence the colouring and shapes used by ProB, by selecting "Graphical Viewer Preferences..." in the "Preferences" menu.

			[[file:ProB_GraphicalViewerPreferences_Shapes.png\|center]]

Michael Leuschel at 15:02, 18 January 2010

2010-01-18T15:02:05Z

@@ Line 25: / Line 25: @@
 We can obtain some statistics about how many states ProB has explored by selecting the "Compute Coverage" command in the "Analyse" menu:
-[[file:ProB_LiftAfterModelCheck_Coverage.png|center||700px]]
+[[file:ProB_LiftAfterModelCheck_Coverage.png|center]]
@@ Line 40: / Line 40: @@
 In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one initialisation, 8 <tt>inc</tt> operations and 8 <tt>dec</tt> operations.

Michael Leuschel at 14:56, 18 January 2010

2010-01-18T14:56:12Z

@@ Line 3: / Line 3: @@
 We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Steps]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.
 The model checker can be used to systematically execute the operations and tries to find an erroneous state (e.g., where the invariant is violated).
@@ Line 15: / Line 17: @@
 [[file:ProB_LiftAfterModelCheck.png|center||700px]]

Michael Leuschel: Created page with 'Category:User Manual We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Steps]. There we have also seen …'

2010-01-18T14:37:10Z

Created page with 'Category:User Manual We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Steps]. There we have also seen …'

New page

[[Category:User Manual]]

We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Steps]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.

The model checker can be used to systematically execute the operations and tries to find an erroneous state (e.g., where the invariant is violated).
Select the "Model Check..." command in the "Verify" menu:
[[file:ProBWinModelCheckCommand.png|center]]
This brings up the following dialog box:
[[file:ProBWinModelCheckDialog.png|center]]
Now click the "Model Check" button. After a short while, ProB will give you the following error message:
[[file:ProBWinModelCheckCounterExampleFound.png|center]]

The lower half of the ProB window should now look as follows:

[[file:ProB_LiftAfterModelCheck.png|center||700px]]

← Older revision		Revision as of 12:14, 18 April 2011
Line 2:		Line 2:


	We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Step]]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.		We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder as outlined in [[Tutorial First Step]]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.

	== Simple Model Checking ==		== Simple Model Checking ==
Line 36:		Line 36:
	* the enabled operations have not been computed.		* the enabled operations have not been computed.
	As such, an open node may contain an invariant violation and/or could be a deadlocking node.		As such, an open node may contain an invariant violation and/or could be a deadlocking node.
	A live node, is a node which is not deadlocked and not open.		A live node is a node which is not deadlocked and not open.

	We can also see, that ~~all in all~~ there are 17 transitions among these 11 nodes. A transition is either an operation or an ~~initialisation~~ (there can be one more transition, which we will examine later in the tutorial).		We can also see that there are in total 17 transitions among these 11 nodes. A transition is either an operation or an initialization (there can be one more transition, which we will examine later in the tutorial).

	In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one ~~initialisation~~, 8 <tt>inc</tt> operations and 8 <tt>dec</tt> operations.		In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one initialization, 8 <tt>inc</tt> operations and 8 <tt>dec</tt> operations.

	== View Statespace ==		== View Statespace ==
Line 50:		Line 50:
	[[file:ProB_LiftAfterModelCheck_Statespace.png\|center]]		[[file:ProB_LiftAfterModelCheck_Statespace.png\|center]]

	We can now see the 11 nodes. The two open nodes are marked in red. You can also see that there is a virtual root node (the inverted triangle at the top), representing the "state" of the machine before ~~initialisation~~. The current node is depicted by the blue hexagon in the right hand corner.		We can now see the 11 nodes. The two open nodes are marked in red. You can also see that there is a virtual root node (the inverted triangle at the top), representing the "state" of the machine before initialization. The current node is depicted by the blue hexagon in the right hand corner.

	Note: you can influence the ~~colouring~~ and shapes used by ProB, by selecting "Graphical Viewer Preferences..." in the "Preferences" menu.		Note: you can influence the coloring and shapes used by ProB, by selecting "Graphical Viewer Preferences..." in the "Preferences" menu.

	[[file:ProB_GraphicalViewerPreferences_Shapes.png\|center]]		[[file:ProB_GraphicalViewerPreferences_Shapes.png\|center]]

	You can obtain more information about the state space ~~visualisation~~ in the user manual: [[State Space Visualization]].		You can obtain more information about the state space visualization in the user manual: [[State Space Visualization]].