Tutorial Directed Model Checking - Revision history

Michael Leuschel at 12:27, 24 March 2025

2025-03-24T12:27:43Z

← Older revision		Revision as of 12:27, 24 March 2025
Line 136:		Line 136:

	A further illustration of directed model checking can be found in our [[Blocks_World_(Directed_Model_Checking)\|"Blocks World" example]].		A further illustration of directed model checking can be found in our [[Blocks_World_(Directed_Model_Checking)\|"Blocks World" example]].


			== Article ==

			Michael Leuschel, Jens Bendisposto:
			[https://doi.org/10.1007/978-3-642-19829-8_1 Directed Model Checking for B: An Evaluation and New Techniques]. SBMF 2010: 1-16

Michael Leuschel: /* More examples */

2016-04-23T07:35:56Z

More examples

← Older revision		Revision as of 07:35, 23 April 2016
Line 135:		Line 135:
	== More examples ==		== More examples ==

	A further illustration of directed model checking can be found in our [[Blocks_World_(Directed_Model_Checking)\|"Blocks World" example].		A further illustration of directed model checking can be found in our [[Blocks_World_(Directed_Model_Checking)\|"Blocks World" example]].

Michael Leuschel at 07:35, 23 April 2016

2016-04-23T07:35:44Z

← Older revision		Revision as of 07:35, 23 April 2016
Line 132:		Line 132:

	One can notice that ProB here has a tendency to go into depth, as the number of enabled operations decreases: if we add a name to the phonebook, four enabled operations disappear and only two appear (lookup and delete). Note: here it is important to set the <tt>MAX_OPERATIONS</tt> high enough, otherwise the resulting state space could be different.		One can notice that ProB here has a tendency to go into depth, as the number of enabled operations decreases: if we add a name to the phonebook, four enabled operations disappear and only two appear (lookup and delete). Note: here it is important to set the <tt>MAX_OPERATIONS</tt> high enough, otherwise the resulting state space could be different.

			== More examples ==

			A further illustration of directed model checking can be found in our [[Blocks_World_(Directed_Model_Checking)\|"Blocks World" example].

Michael Leuschel at 07:30, 5 April 2016

2016-04-05T07:30:16Z

← Older revision		Revision as of 07:30, 5 April 2016
Line 16:		Line 16:
	As of version 1.5.1, the following options are also available:		As of version 1.5.1, the following options are also available:
	<ul>		<ul>
	<li>Heuristic Function / Random (<tt>heuristic</tt> for <tt>mc_mode</tt>) : try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause. Some explanations can be found [[Blocks_World_(Directed_Model_Checking)\|in an example about directed model checking]].</li>		<li>Heuristic Function / Random (<tt>heuristic</tt> for <tt>mc_mode</tt>) : try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause; states with the smallest value for the heuristic function are treated first by the model checker. Some explanations can be found [[Blocks_World_(Directed_Model_Checking)\|in an example about directed model checking]].</li>
	<li>Random (<tt>random</tt>) : choosing next node to process completely at random,</li>		<li>Random (<tt>random</tt>) : choosing next node to process completely at random,</li>
	<li>Hash-Random (<tt>hash</tt>) :similar to random, but uses the Prolog hash function of a node instead of a random number generator,</li>		<li>Hash-Random (<tt>hash</tt>) :similar to random, but uses the Prolog hash function of a node instead of a random number generator,</li>

Michael Leuschel: /* Mixed DF/BF */

2015-04-17T12:21:56Z

Mixed DF/BF

← Older revision		Revision as of 12:21, 17 April 2015
Line 90:		Line 90:

	=== Mixed DF/BF ===		=== Mixed DF/BF ===

			The mixed search strategy, tries to combine the advantages of breadth-first and depth-first search.
			It is the default setting for ProB.
			It has the advantage of ensuring the exploration of some branches in depth, to find errors which require long counter examples (e.g., starvation, resource exhaustion kind of bugs). But it also ensures that we examine the specification more systematically in breadth, and is thus also good at finding counter examples which require exhaustively to test all operations (e.g., many errors simply require a particular faulty B operation to be executed).

	$ probcli phonebook7.mch -p MAX_OPERATIONS 200 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode mixed		$ probcli phonebook7.mch -p MAX_OPERATIONS 200 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode mixed

Michael Leuschel: /* Depth-First */

2015-04-17T12:18:07Z

Depth-First

← Older revision		Revision as of 12:18, 17 April 2015
Line 83:		Line 83:

	[[file:ProB_Phonebook7_spdot_df.png\|160px\|center]]		[[file:ProB_Phonebook7_spdot_df.png\|160px\|center]]

			The depth-first traversal has the advantage of lower memory requirements (concerning storing the unprocessed nodes) and can find very deep counter examples.
			While it is typically the best choice for exhaustive model checking, it can be a poor choice for models with errors. Indeed, if the state space is infinite, then depth-first may progress infinitely in one direction, and never find existing counter examples.
			Also, when depth-first search finds a counter example, it is typically very long and possibly hard to understand for the user.
			The next search strategy, tries to combine the advantages of breadth-first and depth-first search.

	=== Mixed DF/BF ===		=== Mixed DF/BF ===

Michael Leuschel: /* Breadth-First */

2015-04-17T12:14:56Z

Breadth-First

← Older revision		Revision as of 12:14, 17 April 2015
Line 73:		Line 73:

	[[file:ProB_Phonebook7_spdot_bf.png\|1000px\|center]]		[[file:ProB_Phonebook7_spdot_bf.png\|1000px\|center]]

			This mode has the advantage of finding shortest counter examples first.
			We also have a guarantee that, provided a counter example exists, a counter example will sooner or later be found.
			However, the memory requirements can be very large and it can take very long to find long counter examples.

	=== Depth-First ===		=== Depth-First ===

Michael Leuschel at 12:12, 17 April 2015

2015-04-17T12:12:35Z

Michael Leuschel: /* Breadth-First */

2015-04-17T10:50:46Z

Breadth-First

← Older revision		Revision as of 10:50, 17 April 2015
Line 69:		Line 69:
	$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf		$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf

	[[file:ProB_Phonebook7_spdot_bf.png\|~~900px~~\|center]]		[[file:ProB_Phonebook7_spdot_bf.png\|1000px\|center]]

	=== Depth-First ===		=== Depth-First ===

Michael Leuschel: /* Out-Degree */

2015-04-17T10:36:56Z

Out-Degree

← Older revision		Revision as of 10:36, 17 April 2015
Line 114:		Line 114:

	[[file:ProB_Phonebook7_spdot_dlk.png\|600px\|center]]		[[file:ProB_Phonebook7_spdot_dlk.png\|600px\|center]]

			One can notice that ProB here has a tendency to go into depth, as the number of enabled operations decreases: if we add a name to the phonebook, four enabled operations disappear and only two appear (lookup and delete). Note: here it is important to set the <tt>MAX_OPERATIONS</tt> high enough, otherwise the resulting state space could be different.

← Older revision		Revision as of 12:12, 17 April 2015
Line 5:		Line 5:

	Here we will look a bit closer at the search strategy options of the ProB model checker.		Here we will look a bit closer at the search strategy options of the ProB model checker.
	You can set the mode using the <tt>-mc_mode ~~<M>~~</tt> command-line switch of [[Using_the_Command-Line_Version_of_ProB\|probcli]].		You can set the mode using the <tt>-mc_mode</tt> command-line switch of [[Using_the_Command-Line_Version_of_ProB\|probcli]].
	In the Tcl/Tk version you can select the strategy in the model checking dialog box (which you obtain via the"Model Check..." command in the "Verify" menu):		In the Tcl/Tk version you can select the strategy in the model checking dialog box (which you obtain via the"Model Check..." command in the "Verify" menu):
	[[file:ProBWinModelCheckDialog.png\|center]]		[[file:ProBWinModelCheckDialog.png\|center]]
Line 16:		Line 16:
	As of version 1.5.1, the following options are also available:		As of version 1.5.1, the following options are also available:
	<ul>		<ul>
	<li>Heuristic Function / Random (<tt>heuristic</tt>) : try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause. Some explanations can be found [[Blocks_World_(Directed_Model_Checking)\|in an example about directed model checking]].</li>		<li>Heuristic Function / Random (<tt>heuristic</tt> for <tt>mc_mode</tt>) : try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause. Some explanations can be found [[Blocks_World_(Directed_Model_Checking)\|in an example about directed model checking]].</li>
	<li>Random (<tt>random</tt>) : choosing next node to process completely at random,</li>		<li>Random (<tt>random</tt>) : choosing next node to process completely at random,</li>
	<li>Hash-Random (<tt>hash</tt>) :similar to random, but uses the Prolog hash function of a node instead of a random number generator,</li>		<li>Hash-Random (<tt>hash</tt>) :similar to random, but uses the Prolog hash function of a node instead of a random number generator,</li>
	<li>Out-Degree for Deadlock Checking (<tt>out_degree_hash</tt>): prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking.		<li>Out-Degree for Deadlock Checking (<tt>out_degree_hash</tt>): prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking.
	</ul>		</ul>

			Note that for exhaustive model checking, where you have to look at the entire state space and no error state is found, the search strategy has little nor no influence: it does not really matter in which order we process the states, when we have to examine all of them anyway. In this case, the depth-first search is probably the most adequate choice: its memory requirement is smaller.
			However, when you expect an error (or goal state) to be found and when the state space is very large (or even infinite), then the search strategy can make a big difference: the difference between finding an error state very quickly, or only after a very long time or possibly never at all.

	To illustrate the effect of the search strategy we use the following simple example:		To illustrate the effect of the search strategy we use the following simple example: