Consistency Checking - Revision history

David Geleßus: Update PDF link

2021-02-04T17:22:24Z

Update PDF link

← Older revision		Revision as of 17:22, 4 February 2021
Line 46:		Line 46:
	The preferences "Nr of Initialisations shown" and "Max Number of Enablings shown" (described in [[Animation#Animation Preferences\|Animation Preferences]]) affect the model checking in exactly the same way as they do for the animation. These preferences are particularly important for the model checking, as setting the number of initializations or the number times than an operation may be enabled too low will lead to computing and searching a state space that is too small. On the other hand, the user may have to set these preferences to a lower value if the exhaustive state space is too big to be covered by ProB.		The preferences "Nr of Initialisations shown" and "Max Number of Enablings shown" (described in [[Animation#Animation Preferences\|Animation Preferences]]) affect the model checking in exactly the same way as they do for the animation. These preferences are particularly important for the model checking, as setting the number of initializations or the number times than an operation may be enabled too low will lead to computing and searching a state space that is too small. On the other hand, the user may have to set these preferences to a lower value if the exhaustive state space is too big to be covered by ProB.

	Once the state space of the B specification has been computed by ProB, the commands from the "Analyse" menu (see [[Animation#The Analyse menu\|The Analyse menu]]) and the visualization features (see [[State Space Visualization]]) are then very useful to examine the state space. The features used to visualize a reduced state space are particularly useful as examining a huge state space may not yield to interesting observations due to excessive cluttering <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 ~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/~~publications~~/~~prob_visualise~~.pdf~~[wiki:Visualisation#VisualizeStateSpace~~</ref>.		Once the state space of the B specification has been computed by ProB, the commands from the "Analyse" menu (see [[Animation#The Analyse menu\|The Analyse menu]]) and the visualization features (see [[State Space Visualization]]) are then very useful to examine the state space. The features used to visualize a reduced state space are particularly useful as examining a huge state space may not yield to interesting observations due to excessive cluttering <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref>.

	== Machines with Invariant Violations and Deadlocks ==		== Machines with Invariant Violations and Deadlocks ==

Michael Leuschel: /* Using the Model Checker */

2015-04-16T14:48:33Z

Using the Model Checker

← Older revision		Revision as of 14:48, 16 April 2015
Line 24:		Line 24:

	By default the model checking is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is selected in the "Search Strategy" pop-up menu.		By default the model checking is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is selected in the "Search Strategy" pop-up menu.
			As of version 1.5.1, additional options for <b>directed</b> model checking are available. For example, one can have truly random exploration or provide a custom heuristic function to guide the model checker. These features are illustrated using the [[Blocks World (Directed Model Checking)\|the blocks world example]].

	The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.		The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.

Michael Leuschel: /* Consistency Checking (Model Checking) */

2015-03-10T10:04:17Z

Consistency Checking (Model Checking)

Michael Leuschel at 10:01, 10 March 2015

2015-03-10T10:01:58Z

← Older revision		Revision as of 10:01, 10 March 2015
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
			= Consistency Checking (Model Checking) =
	By manually animating a B machine, it is possible to discover problems with the specification, such as invariant violations or deadlocks. The ProB model checker can do this exploration systematically and automatically. It will alert you as soon as a problem has been found, and will then present the shortest trace (within currently explored states) that leads from an initial state to the error.		By manually animating a B machine, it is possible to discover problems with the specification, such as invariant violations or deadlocks. The ProB model checker can do this exploration systematically and automatically. It will alert you as soon as a problem has been found, and will then present the shortest trace (within currently explored states) that leads from an initial state to the error.

Michael Leuschel at 07:46, 5 August 2014

2014-08-05T07:46:58Z

← Older revision		Revision as of 07:46, 5 August 2014
Line 15:		Line 15:
	As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.		As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.

	== Using the ~~Temporal~~ Model Checker (TMC) ==		== Using the Model Checker (TMC) ==

	To model check a B machine loaded in ProB, launch the command from "Verify\|~~Temporal~~		To model check a B machine loaded in ProB, launch the command from "Verify\|
	Model Check".		Model Check".

Michael Leuschel: /* Using the Temporal Model Checker (TMC) */

2012-02-27T15:55:20Z

Using the Temporal Model Checker (TMC)

← Older revision		Revision as of 15:55, 27 February 2012
Line 25:		Line 25:

	The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.		The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.

	Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion).		Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion).
	Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).		Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state). More details about assertions and goals can be found below.

	The temporal model checker (TMC) is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.		The temporal model checker (TMC) is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.

Michael Leuschel: /* Using the Temporal Model Checker (TMC) */

2012-02-27T15:54:01Z

Using the Temporal Model Checker (TMC)

← Older revision		Revision as of 15:54, 27 February 2012
Line 28:		Line 28:
	Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).		Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).

	The temporal model checker (TMC) is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.		The temporal model checker (TMC) is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.

	=== Incremental Model Checking ===		=== Incremental Model Checking ===

Michael Leuschel: /* Using the Temporal Model Checker (TMC) */

2012-02-27T15:53:50Z

Using the Temporal Model Checker (TMC)

← Older revision		Revision as of 15:53, 27 February 2012
Line 22:		Line 22:
	[[File:Temporal_Model_Checker_settings.png\|center]]		[[File:Temporal_Model_Checker_settings.png\|center]]

	By default the model checking is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is ~~toggled on~~.		By default the model checking is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is selected in the "Search Strategy" pop-up menu.

	The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.		The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.
	Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion).		Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion).
	Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).		Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).

	The temporal model checker is started by clicking on the "Model Check" button. When the ~~TMC~~ computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until ~~the number of nodes indicated in the "Enter max nr. of nodes to check" entry is reached or~~ a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the "Cancel" button.		The temporal model checker (TMC) is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.

	=== Incremental Model Checking ===		=== Incremental Model Checking ===
Line 37:		Line 38:
	=== Results of the Model Checking ===		=== Results of the Model Checking ===
	When the state space has been computed by ProB, the pop-up window is replaced by a dialog window stating "No error state found". All new nodes visited. If ProB finds a node where one of the property that was checked is not verified, it displays a similar pop-up window but with the text Error state was found for new node: invariant violation or Error state was found for new node: deadlock. Then, ProB displays in the animation panes the state of the B machine corresponding to the property violation. From there, the user can examine the state in the "State Properties" pane, the enabled operations (including the backtrack virtual operation to go back to the valid state that lead to the property violation) in the "Enabled Operations" pane, and the trace (sequence of operations) leading to the invalid state in the "History" pane.		When the state space has been computed by ProB, the pop-up window is replaced by a dialog window stating "No error state found". All new nodes visited. If ProB finds a node where one of the property that was checked is not verified, it displays a similar pop-up window but with the text Error state was found for new node: invariant violation or Error state was found for new node: deadlock. Then, ProB displays in the animation panes the state of the B machine corresponding to the property violation. From there, the user can examine the state in the "State Properties" pane, the enabled operations (including the backtrack virtual operation to go back to the valid state that lead to the property violation) in the "Enabled Operations" pane, and the trace (sequence of operations) leading to the invalid state in the "History" pane.

	=== Preferences of the Model Checking ===		=== Preferences of the Model Checking ===

Michael Leuschel at 15:51, 27 February 2012

2012-02-27T15:51:34Z

← Older revision		Revision as of 15:51, 27 February 2012
Line 20:		Line 20:
	Model Check".		Model Check".

	[[File:Temporal_Model_Checker_settings.png]]		[[File:Temporal_Model_Checker_settings.png\|center]]

	~~The entry "Enter max nr. of nodes to check" in the pop-up window indicates~~ the ~~number of states that ProB should compute. (This field has disappeared in version 1.3.1.) This computation~~ is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is toggled on. The two ~~toggles~~ "Find Deadlocks" and "Find Invariant Violations" ~~add to this computation~~ a ~~verification of~~ the ~~corresponding property each time~~ a new ~~node is computed~~. The temporal model checker is started by clicking on the "Model Check" button. When the TMC computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until the number of nodes indicated in the "Enter max nr. of nodes to check" entry is reached or a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the "Cancel" button.		By default the model checking is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is toggled on.
			The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.
			Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion).
			Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state).

			The temporal model checker is started by clicking on the "Model Check" button. When the TMC computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until the number of nodes indicated in the "Enter max nr. of nodes to check" entry is reached or a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the "Cancel" button.

	=== Incremental Model Checking ===		=== Incremental Model Checking ===

Joy Clark: " "

2011-04-18T11:44:49Z

" "

← Older revision		Revision as of 10:04, 10 March 2015
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	= Consistency ~~Checking (~~Model Checking) =		= Checking Consistency via Model Checking =
	By manually animating a B machine, it is possible to discover problems with the specification, such as invariant violations or deadlocks. The ProB model checker can do this exploration systematically and automatically. It will alert you as soon as a problem has been found, and will then present the shortest trace (within currently explored states) that leads from an initial state to the error.		By manually animating a B machine, it is possible to discover problems with the specification, such as invariant violations or deadlocks. The ProB model checker can do this exploration systematically and automatically. It will alert you as soon as a problem has been found, and will then present the shortest trace (within currently explored states) that leads from an initial state to the error.

Line 16:		Line 16:
	As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.		As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.

	== Using the Model Checker ~~(TMC)~~ ==		== Using the Model Checker ==

	To model check a B machine loaded in ProB, launch the command from "Verify\|		To model check a B machine loaded in ProB, launch the command from "Verify\|
Line 30:		Line 30:
	Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state). More details about assertions and goals can be found below.		Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state). More details about assertions and goals can be found below.

	The ~~temporal~~ model checker ~~(TMC)~~ is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.		The model checker is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. The user can interrupt the model checking at any time by pressing the "Cancel" button.

	=== Incremental Model Checking ===		=== Incremental Model Checking ===

	It is important to understand that the computation of and search in the state space is an incremental process. The model checking can be done by running the ~~TMC~~ several times; if the number of nodes specified in the entry "max nr. of nodes to check" is less that the size of the state space that remains to be checked. If the model checking is done in several steps, the end of the model checking step is indicated by the line No error so far, ... nodes visited at the bottom of the pop-up window, unless a violation of the properties (deadlockfreeness, invariant) are found. Between each model checking step, the user can execute the various commands of ProB, notably those of the "Analyse" menu to display information on the state space (see [[Animation#The Analyse menu\|The Analyse Menu]]) and the visualization features (see [[State Space Visualization]]).		It is important to understand that the computation of and search in the state space is an incremental process. The model checking can be done by running the model checker several times; if the number of nodes specified in the entry "max nr. of nodes to check" is less that the size of the state space that remains to be checked. If the model checking is done in several steps, the end of the model checking step is indicated by the line No error so far, ... nodes visited at the bottom of the pop-up window, unless a violation of the properties (deadlockfreeness, invariant) are found. Between each model checking step, the user can execute the various commands of ProB, notably those of the "Analyse" menu to display information on the state space (see [[Animation#The Analyse menu\|The Analyse Menu]]) and the visualization features (see [[State Space Visualization]]).

	By default, each model checking step starts from the open nodes of the last computed state space. This means that a change in the settings of the ~~TMC~~ between two steps does not affect the non-open nodes (those already computed), unless there is an alternative path to an already computed node. This behavior can be changed by toggling on the "Inspect Existing Nodes" setting. This forces ProB to reevaluate the properties set to be verified on the state space previously computed. Keep in mind that unless the "Inspect Existing Nodes" setting is on, the change of the ~~TMC~~ settings may not affect the state space already computed.		By default, each model checking step starts from the open nodes of the last computed state space. This means that a change in the settings of the model checker between two steps does not affect the non-open nodes (those already computed), unless there is an alternative path to an already computed node. This behavior can be changed by toggling on the "Inspect Existing Nodes" setting. This forces ProB to reevaluate the properties set to be verified on the state space previously computed. Keep in mind that unless the "Inspect Existing Nodes" setting is on, the change of the model checking settings may not affect the state space already computed.

	=== Results of the Model Checking ===		=== Results of the Model Checking ===
Line 51:		Line 51:
	When the two properties (invariant and deadlock-freeness) are checked and a state violates both , only the invariant violation is reported. In that situation, the deadlock can be observed either from the Enabled Operations (as only the backtrack virtual operation is enabled), or from the state space graph (as the current node has no successors).		When the two properties (invariant and deadlock-freeness) are checked and a state violates both , only the invariant violation is reported. In that situation, the deadlock can be observed either from the Enabled Operations (as only the backtrack virtual operation is enabled), or from the state space graph (as the current node has no successors).

	During the model checking of a specification which contains both of these errors, it is often useful to be able to focus exclusively upon the detection of one type of error. For example, since an invariant violation is only reported the first time it is encountered, subsequent invocations of the ~~TMC~~ may yield deadlocks whose cause is the invariant violation. This is done by toggling off the corresponding settings of the temporal model checker pop-up window.		During the model checking of a specification which contains both of these errors, it is often useful to be able to focus exclusively upon the detection of one type of error. For example, since an invariant violation is only reported the first time it is encountered, subsequent invocations of the model checker may yield deadlocks whose cause is the invariant violation. This is done by toggling off the corresponding settings of the temporal model checker pop-up window.

	'''HINT: Turning off invariant violation and deadlock detection will simply compute the entire state space until the user presses the Cancel button or until the specified number of nodes is reached.'''		'''HINT: Turning off invariant violation and deadlock detection will simply compute the entire state space until the user presses the Cancel button or until the specified number of nodes is reached.'''
Line 70:		Line 70:
	== Specifying Goals and Assertions ==		== Specifying Goals and Assertions ==

	The ASSERTIONS clause of a B machine enables the user to define predicates that are supposed to be deducible from the INVARIANT or PROPERTIES clauses. If the B specification opened in ProB contains an ASSERTIONS clause, the ~~TMC~~ pop-up window enables to check if the assertion can be violated. If enabled and a state corresponding to the violation of the assertion is found, a message "Error state was found for new node: assertion violation" is displayed, and then ProB displays this state in the animation panes		The ASSERTIONS clause of a B machine enables the user to define predicates that are supposed to be deducible from the INVARIANT or PROPERTIES clauses. If the B specification opened in ProB contains an ASSERTIONS clause, the model checking pop-up window enables to check if the assertion can be violated. If enabled and a state corresponding to the violation of the assertion is found, a message "Error state was found for new node: assertion violation" is displayed, and then ProB displays this state in the animation panes

	A feature that is similar to the assertions is the notion of a goal. A goal is a macro in the DEFINITIONS section whose name is GOAL and whose content is a predicate. If the B specification defines such a macro, the ~~TMC~~ pop-up window enables to check if a state satisfies this goal. If enabled and a state corresponding to the goal is found, a message "State satisfying GOAL predicate was found" is displayed, and then ProB displays this state in the animation panes.		A feature that is similar to the assertions is the notion of a goal. A goal is a macro in the DEFINITIONS section whose name is GOAL and whose content is a predicate. If the B specification defines such a macro, the model checking pop-up window enables to check if a state satisfies this goal. If enabled and a state corresponding to the goal is found, a message "State satisfying GOAL predicate was found" is displayed, and then ProB displays this state in the animation panes.

	It is also possible to find a state of the B machine that satisfies such a goal without defining it explicitly in the B specification. The "Verify\|Advanced Find..." command enables the user to type a predicate directly in a text field. ProB then searches for a state of the state space currently computed that satisfies this goal.		It is also possible to find a state of the B machine that satisfies such a goal without defining it explicitly in the B specification. The "Verify\|Advanced Find..." command enables the user to type a predicate directly in a text field. ProB then searches for a state of the state space currently computed that satisfies this goal.

← Older revision		Revision as of 11:44, 18 April 2011
Line 11:		Line 11:
	Since a graph of the visited states and the transformations (operations) between them is retained, it is therefore possible to produce traces (sequence of operations) of invariant violations when they are detected. Such a trace is called a “counter-example” and is useful in determining where and in what circumstances a specification contains errors.		Since a graph of the visited states and the transformations (operations) between them is retained, it is therefore possible to produce traces (sequence of operations) of invariant violations when they are detected. Such a trace is called a “counter-example” and is useful in determining where and in what circumstances a specification contains errors.

	Notice that if the model checker does not find any invariant violations or deadlocks when a traversal of the exhaustive state space has been performed, this does not imply that the specification is a correct specification. This should be understood as the fact that, given the initialization stated and the model checker preferences set at the time of the check, no errors were found. The main difference is that the ProB animation preferences (such as the number of initializations ~~and enablings~~ and the size of unspecified sets) may be set too low for the exhaustive state space to be covered by the model checking.		Notice that if the model checker does not find any invariant violations or deadlocks when a traversal of the exhaustive state space has been performed, this does not imply that the specification is a correct specification. This should be understood as the fact that, given the initialization stated and the model checker preferences set at the time of the check, no errors were found. The main difference is that the ProB animation preferences (such as the number of initializations, times that an operation may be enabled, and the size of unspecified sets) may be set too low for the exhaustive state space to be covered by the model checking.

	As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.		As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.
Line 17:		Line 17:
	== Using the Temporal Model Checker (TMC) ==		== Using the Temporal Model Checker (TMC) ==

	To model check a B machine loaded in ProB, launch the command from Verify\|Temporal		To model check a B machine loaded in ProB, launch the command from "Verify\|Temporal
	Model Check.		Model Check".

	[[File:Temporal_Model_Checker_settings.png]]		[[File:Temporal_Model_Checker_settings.png]]

	The entry Enter max nr. of nodes to check in the pop-up window indicates the number of states that ProB should compute. (This field has disappeared in version 1.3.1.) This computation is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting pure Depth or pure Breadth First is toggled on. The two toggles Find Deadlocks and Find Invariant Violations add to this computation a verification of the corresponding property each time a new node is computed. The temporal model checker is started by clicking on the Model Check button. When the TMC computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in ~~realtime~~ the number of nodes that have been computed, until the number of nodes indicated in the Enter max nr. of nodes to check entry is reached or a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the Cancel button.		The entry "Enter max nr. of nodes to check" in the pop-up window indicates the number of states that ProB should compute. (This field has disappeared in version 1.3.1.) This computation is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting "pure Depth" or "pure Breadth First" is toggled on. The two toggles "Find Deadlocks" and "Find Invariant Violations" add to this computation a verification of the corresponding property each time a new node is computed. The temporal model checker is started by clicking on the "Model Check" button. When the TMC computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until the number of nodes indicated in the "Enter max nr. of nodes to check" entry is reached or a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the "Cancel" button.

	=== Incremental Model Checking ===		=== Incremental Model Checking ===

	It is important to understand that the computation of and search in the state space is an incremental process. The model checking can be done by running the TMC several times; if the number of nodes specified in the entry max nr. of nodes to check is less that the size of the state space that remains to be checked. If the model checking is done in several steps, the end of the model checking step is indicated by the line No error so far, ... nodes visited at the bottom of the pop-up window, unless a violation of the properties (deadlockfreeness, invariant) are found. Between each model checking step, the user can execute the various commands of ProB, notably those of the Analyse menu to display information on the state space (see [[Animation#The Analyse menu\|The Analyse Menu]]) and the visualization features (see [[State Space Visualization]]).		It is important to understand that the computation of and search in the state space is an incremental process. The model checking can be done by running the TMC several times; if the number of nodes specified in the entry "max nr. of nodes to check" is less that the size of the state space that remains to be checked. If the model checking is done in several steps, the end of the model checking step is indicated by the line No error so far, ... nodes visited at the bottom of the pop-up window, unless a violation of the properties (deadlockfreeness, invariant) are found. Between each model checking step, the user can execute the various commands of ProB, notably those of the "Analyse" menu to display information on the state space (see [[Animation#The Analyse menu\|The Analyse Menu]]) and the visualization features (see [[State Space Visualization]]).

	By default, each model checking step starts from the open nodes of the last computed state space. This means that a change in the settings of the TMC between two steps does not affect the non-open nodes (those already computed), unless there is an alternative path to an already computed node. This behavior can be changed by toggling on the Inspect Existing Nodes setting. This forces ProB to reevaluate the properties set to be verified on the state space previously computed. Keep in mind that unless the Inspect Existing Nodes setting is on, the change of the TMC settings may not affect the state space already computed.		By default, each model checking step starts from the open nodes of the last computed state space. This means that a change in the settings of the TMC between two steps does not affect the non-open nodes (those already computed), unless there is an alternative path to an already computed node. This behavior can be changed by toggling on the "Inspect Existing Nodes" setting. This forces ProB to reevaluate the properties set to be verified on the state space previously computed. Keep in mind that unless the "Inspect Existing Nodes" setting is on, the change of the TMC settings may not affect the state space already computed.

	=== Results of the Model Checking ===		=== Results of the Model Checking ===
	When the state space has been computed by ProB, the pop-up window is replaced by a dialog window stating No error state found. All new nodes visited. If ProB finds a node where one of the property that was checked is not verified, it displays a similar pop-up window but with the text Error state was found for new node: invariant violation or Error state was found for new node: deadlock. Then, ProB displays in the animation panes the state of the B machine corresponding to the property violation. From there, the user can examine the state in the State Properties pane, the enabled operations (including the backtrack virtual operation to go back to the valid state that lead to the property violation) in the Enabled Operations pane, and the trace (sequence of operations) leading to the invalid state in the History pane.		When the state space has been computed by ProB, the pop-up window is replaced by a dialog window stating "No error state found". All new nodes visited. If ProB finds a node where one of the property that was checked is not verified, it displays a similar pop-up window but with the text Error state was found for new node: invariant violation or Error state was found for new node: deadlock. Then, ProB displays in the animation panes the state of the B machine corresponding to the property violation. From there, the user can examine the state in the "State Properties" pane, the enabled operations (including the backtrack virtual operation to go back to the valid state that lead to the property violation) in the "Enabled Operations" pane, and the trace (sequence of operations) leading to the invalid state in the "History" pane.
	=== Preferences of the Model Checking ===		=== Preferences of the Model Checking ===

	The preferences Nr of Initialisations shown and Max Number of Enablings shown (described in [[Animation#Animation Preferences\|Animation Preferences]]) affect the model checking in exactly the same way as they do for the animation. These preferences are particularly important for the model checking, as setting the number of initializations or the number ~~of enablings~~ too low will lead to computing and searching a state space that is too small. On the other hand, the user may have to set these preferences to a lower value if the exhaustive state space is too big to be covered by ProB.		The preferences "Nr of Initialisations shown" and "Max Number of Enablings shown" (described in [[Animation#Animation Preferences\|Animation Preferences]]) affect the model checking in exactly the same way as they do for the animation. These preferences are particularly important for the model checking, as setting the number of initializations or the number times than an operation may be enabled too low will lead to computing and searching a state space that is too small. On the other hand, the user may have to set these preferences to a lower value if the exhaustive state space is too big to be covered by ProB.

	Once the state space of the B specification has been computed by ProB, the commands from the Analyse menu (see [[Animation#The Analyse menu\|The Analyse menu]]) and the visualization features (see [[State Space Visualization]]) are then very useful to examine the state space. The features used to visualize a reduced state space are particularly useful as examining a huge state space may not yield to interesting observations due to excessive cluttering <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 http://www.stups.uni-duesseldorf.de/publications/prob_visualise.pdf[wiki:Visualisation#VisualizeStateSpace</ref>.		Once the state space of the B specification has been computed by ProB, the commands from the "Analyse" menu (see [[Animation#The Analyse menu\|The Analyse menu]]) and the visualization features (see [[State Space Visualization]]) are then very useful to examine the state space. The features used to visualize a reduced state space are particularly useful as examining a huge state space may not yield to interesting observations due to excessive cluttering <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 http://www.stups.uni-duesseldorf.de/publications/prob_visualise.pdf[wiki:Visualisation#VisualizeStateSpace</ref>.

	== Machines with Invariant Violations and Deadlocks ==		== Machines with Invariant Violations and Deadlocks ==
Line 48:		Line 48:
	=== Two Phase Verification ===		=== Two Phase Verification ===

	If the state space of the specification can be exhaustively searched, check for deadlocks and invariant violations in two phases. To do this, set Inspect Existing Nodes to off and ~~set one of~~ Check for Deadlocks or Check for Invariant Violations to on and the other to off. Perform the temporal model check until all the deadlocks (resp. invariant violations) are detected or shown to be absent. To recheck the whole state space, either turn on the option Inspect Existing Nodes or purge the state space already computed by reopening the machine. Now deselect		If the state space of the specification can be exhaustively searched, check for deadlocks and invariant violations in two phases. To do this, set "Inspect Existing Nodes" to off and turn either "Check for Deadlocks" or "Check for Invariant Violations" on and the other off. Perform the temporal model check until all the deadlocks (resp. invariant violations) are detected or shown to be absent. To recheck the whole state space, either turn on the option "Inspect Existing Nodes" or purge the state space already computed by reopening the machine. Now deselect
	the previous property checked, and select the alternative property for checking. Now perform a temporal model check again to search for a violation of the second property.		the previous property checked, and select the alternative property for checking. Now perform a temporal model check again to search for a violation of the second property.

Line 55:		Line 55:
	=== Interleaved deadlock and invariant violation checking ===		=== Interleaved deadlock and invariant violation checking ===

	If you wish to determine if an already encountered invariant violation is also a deadlocked node, turn the option Inspect Existing Nodes on, turn Detect Invariant Violations off, and ensure that Detect Deadlocks is on. Performing a temporal model check now will traverse the state space including the previously found node that violates the invariant.		If you wish to determine if an already encountered invariant violation is also a deadlocked node, turn the option "Inspect Existing Nodes" on, turn "Detect Invariant Violations" off, and ensure that "Detect Deadlocks" is on. Performing a temporal model check now will traverse the state space including the previously found node that violates the invariant.

	'''WARNING: Enabling Inspect Existing Nodes will continually report the first error it encounters until that error is corrected.'''		'''WARNING: Enabling "Inspect Existing Nodes" will continually report the first error it encounters until that error is corrected.'''

	== Specifying Goals and Assertions ==		== Specifying Goals and Assertions ==

	The ASSERTIONS clause of a B machine enables the user to define predicates that are supposed to be deducible from the INVARIANT or PROPERTIES clauses. If the B specification opened in ProB contains an ASSERTIONS clause, the TMC pop-up window enables to check if the assertion can be violated. If enabled and a state corresponding to the violation of the assertion is found, a message Error state was found for new node: assertion violation is displayed, and then ProB displays this state in the animation panes		The ASSERTIONS clause of a B machine enables the user to define predicates that are supposed to be deducible from the INVARIANT or PROPERTIES clauses. If the B specification opened in ProB contains an ASSERTIONS clause, the TMC pop-up window enables to check if the assertion can be violated. If enabled and a state corresponding to the violation of the assertion is found, a message "Error state was found for new node: assertion violation" is displayed, and then ProB displays this state in the animation panes

	A feature that is similar to the assertions is the notion of a goal. A goal is a macro in the DEFINITIONS section whose name is GOAL and whose content is a predicate. If the B specification defines such a macro, the TMC pop-up window enables to check if a state satisfies this goal. If enabled and a state corresponding to the goal is found, a message State satisfying GOAL predicate was found is displayed, and then ProB displays this state in the animation panes.		A feature that is similar to the assertions is the notion of a goal. A goal is a macro in the DEFINITIONS section whose name is GOAL and whose content is a predicate. If the B specification defines such a macro, the TMC pop-up window enables to check if a state satisfies this goal. If enabled and a state corresponding to the goal is found, a message "State satisfying GOAL predicate was found" is displayed, and then ProB displays this state in the animation panes.

	It is also possible to find a state of the B machine that satisfies such a goal without defining it explicitly in the B specification. The Verify\|Advanced Find... command enables the user to type a predicate directly in a text field. ProB then searches for a state of the state space currently computed that satisfies this goal.		It is also possible to find a state of the B machine that satisfies such a goal without defining it explicitly in the B specification. The "Verify\|Advanced Find..." command enables the user to type a predicate directly in a text field. ProB then searches for a state of the state space currently computed that satisfies this goal.

	== References ==		== References ==
	<references />		<references />