Blocks World (Directed Model Checking) - Revision history

David Geleßus: Fix PDF link in reference

2021-02-03T13:29:09Z

Fix PDF link in reference

← Older revision		Revision as of 13:29, 3 February 2021
Line 1:		Line 1:
	In this example we want to highlight the new [[Tutorial_Directed_Model_Checking \|directed model checking]] features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, choosing states with minimal weights for processing. The user can influence how the weights for the unprocessed states are to be computed.		In this example we want to highlight the new [[Tutorial_Directed_Model_Checking \|directed model checking]] features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, choosing states with minimal weights for processing. The user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
	<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 ~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/w/~~Special:Publication~~/LeBe2010</ref>.		<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 https://www3.hhu.de/stups/downloads/pdf/LeBe2010.pdf</ref>.

	To illustrate the directed model checking feature, we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).		To illustrate the directed model checking feature, we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).

Michael Leuschel at 07:36, 23 April 2016

2016-04-23T07:36:33Z

← Older revision		Revision as of 07:36, 23 April 2016
Line 1:		Line 1:
	In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, choosing states with minimal weights for processing. The user can influence how the weights for the unprocessed states are to be computed.		In this example we want to highlight the new [[Tutorial_Directed_Model_Checking \|directed model checking]] features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, choosing states with minimal weights for processing. The user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
	<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.		<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.

Michael Leuschel at 07:29, 5 April 2016

2016-04-05T07:29:10Z

← Older revision		Revision as of 07:29, 5 April 2016
Line 1:		Line 1:
	In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, ~~and the~~ user can influence how the weights for the unprocessed states are to be computed.		In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, choosing states with minimal weights for processing. The user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
	<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.		<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.
Line 104:		Line 104:
	[[File:ProB_BlockGoal_Screenshot.png\|600px\|center]]		[[File:ProB_BlockGoal_Screenshot.png\|600px\|center]]

			When writing your own heuristic functions, keep in mind that internally the weights are stored as 64-bit integers on 64-bit systems, and 32-bit integers on 32-bit systems; currently no overflow checking is performed and larger values for the <tt>HEURISTIC_FUNCTION</tt> expression are silently converted to the respective integer size.

	<h3> The complete model for reference </h3>		<h3> The complete model for reference </h3>

Michael Leuschel at 10:45, 17 April 2015

2015-04-17T10:45:20Z

← Older revision		Revision as of 10:45, 17 April 2015
Line 52:		Line 52:
	You can use the <tt>-bf</tt> flag to force breadth-first search, thus obtaining shortest counter-examples (of length 7; model checking time about 3.3 seconds).		You can use the <tt>-bf</tt> flag to force breadth-first search, thus obtaining shortest counter-examples (of length 7; model checking time about 3.3 seconds).

	As of version 1.5.1 you can use the [[Using_the_Command-Line_Version_of_ProB#-mc_mode_.3CM.3E\|<tt>-mc_mode</tt> ~~flag~~]] to provide other options to control the model checking (see also [[Tutorial_Directed_Model_Checking]]).		As of version 1.5.1 you can use the [[Using_the_Command-Line_Version_of_ProB#-mc_mode_.3CM.3E\|<tt>-mc_mode</tt>]] flag to provide other options to control the model checking (see also [[Tutorial_Directed_Model_Checking\|the tutorial page on directed model checking options]]).

	One option is <tt>random</tt>, which gives every node (aka unprocesses state) a random weight. The difference over the mixed depth-first/breadth-first mode is that it completely disregards when nodes where generated. The mixed depth-first/breadth-first mode will try to do a mixture of depth-first and breadth-first traversal; the random mode here is ``just'' random:		One option is <tt>random</tt>, which gives every node (aka unprocesses state) a random weight. The difference over the mixed depth-first/breadth-first mode is that it completely disregards when nodes where generated. The mixed depth-first/breadth-first mode will try to do a mixture of depth-first and breadth-first traversal; the random mode here is ``just'' random:

Michael Leuschel at 10:43, 17 April 2015

2015-04-17T10:43:53Z

← Older revision		Revision as of 10:43, 17 April 2015
Line 52:		Line 52:
	You can use the <tt>-bf</tt> flag to force breadth-first search, thus obtaining shortest counter-examples (of length 7; model checking time about 3.3 seconds).		You can use the <tt>-bf</tt> flag to force breadth-first search, thus obtaining shortest counter-examples (of length 7; model checking time about 3.3 seconds).

	As of version 1.5.1 you can use the <tt>-mc_mode</tt> flag to provide other options to control the model checking.		As of version 1.5.1 you can use the [[Using_the_Command-Line_Version_of_ProB#-mc_mode_.3CM.3E\|<tt>-mc_mode</tt> flag]] to provide other options to control the model checking (see also [[Tutorial_Directed_Model_Checking]]).

	One option is <tt>random</tt>, which gives every node (aka unprocesses state) a random weight. The difference over the mixed depth-first/breadth-first mode is that it completely disregards when nodes where generated. The mixed depth-first/breadth-first mode will try to do a mixture of depth-first and breadth-first traversal; the random mode here is ``just'' random:		One option is <tt>random</tt>, which gives every node (aka unprocesses state) a random weight. The difference over the mixed depth-first/breadth-first mode is that it completely disregards when nodes where generated. The mixed depth-first/breadth-first mode will try to do a mixture of depth-first and breadth-first traversal; the random mode here is ``just'' random:

Michael Leuschel at 10:41, 17 April 2015

2015-04-17T10:41:14Z

← Older revision		Revision as of 10:41, 17 April 2015
Line 5:		Line 5:
	To illustrate the directed model checking feature, we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).		To illustrate the directed model checking feature, we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).
	The goal is, given a starting position, to find a plan for the robot to achieve a certain goal (here: block a is on top of b, which is on top of c, ...).		The goal is, given a starting position, to find a plan for the robot to achieve a certain goal (here: block a is on top of b, which is on top of c, ...).
			We want to use the model checker to find such a plan, i.e., a <em>counter-example</em> found by the model checker is actually a <em>solution</em> to our planning problem.

	In B we can model this task as follows.		In B we can model this task as follows.

Jens Bendisposto: Undo revision 2812 by Jens Bendisposto (Talk)

2015-04-17T08:23:19Z

Undo revision 2812 by Jens Bendisposto (Talk)

← Older revision		Revision as of 08:23, 17 April 2015
Line 1:		Line 1:
	~~__NOTOC__~~
	In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, and the user can influence how the weights for the unprocessed states are to be computed.		In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, and the user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
Line 45:		Line 44:
	$ probcli BlocksWorldGeneric6.mch -model_check		$ probcli BlocksWorldGeneric6.mch -model_check

	As it has a random component, runtimes vary (typically 0.5 to 3.5 seconds on a Mac Book Air 1.7 GHz). It finds reasonably short ~~sequences of operations to reach a state where the goal holds~~.		As it has a random component, runtimes vary (typically 0.5 to 3.5 seconds on a Mac Book Air 1.7 GHz). It finds reasonably short counter examples.

	You can use depth-first search using the -df flag:		You can use depth-first search using the -df flag:

Jens Bendisposto at 08:22, 17 April 2015

2015-04-17T08:22:03Z

← Older revision		Revision as of 08:22, 17 April 2015
Line 1:		Line 1:
			__NOTOC__
	In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, and the user can influence how the weights for the unprocessed states are to be computed.		In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, and the user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
Line 44:		Line 45:
	$ probcli BlocksWorldGeneric6.mch -model_check		$ probcli BlocksWorldGeneric6.mch -model_check

	As it has a random component, runtimes vary (typically 0.5 to 3.5 seconds on a Mac Book Air 1.7 GHz). It finds reasonably short ~~counter examples~~.		As it has a random component, runtimes vary (typically 0.5 to 3.5 seconds on a Mac Book Air 1.7 GHz). It finds reasonably short sequences of operations to reach a state where the goal holds.

	You can use depth-first search using the -df flag:		You can use depth-first search using the -df flag:

Michael Leuschel at 14:57, 16 April 2015

2015-04-16T14:57:53Z

← Older revision		Revision as of 14:57, 16 April 2015
Line 1:		Line 1:
	In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1).		In this example we want to highlight the new directed model checking features of ProB (available as of version 1.5.1), which allow one to <em>direct</em> the model checker towards a desired goal. Technically speaking, the model checker now maintains a weighted priority queue of unprocessed states, and the user can influence how the weights for the unprocessed states are to be computed.
	The techniques are also explained and evaluated in a scientific paper		The techniques are also explained and evaluated in a scientific paper
	<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.		<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.

Michael Leuschel at 14:55, 16 April 2015

2015-04-16T14:55:31Z

← Older revision		Revision as of 14:55, 16 April 2015
Line 3:		Line 3:
	<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.		<ref name="vispaper">M. Leuschel and J. Bendisposto: Directed Model Checking for B: An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527. Springer-Verlag, 2010 http://www.stups.uni-duesseldorf.de/w/Special:Publication/LeBe2010</ref>.

	~~For this~~ we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).		To illustrate the directed model checking feature, we use the following model of Blocks-World, where we manipulate a given set of blocks (a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block is on top of it) and either move it onto a table or onto another block (provided this block has no other block on top of it).
	The goal is, given a starting position, to find a plan for the robot to achieve a certain goal (here: block a is on top of b, which is on top of c, ...).		The goal is, given a starting position, to find a plan for the robot to achieve a certain goal (here: block a is on top of b, which is on top of c, ...).