Tutorial Understanding ProB's Constraint Solver - Revision history

Michael Leuschel: /* Complicating the Example */

2011-07-27T06:56:08Z

Complicating the Example

← Older revision		Revision as of 06:56, 27 July 2011
Line 145:		Line 145:
	[[file:ProB_PropagationAfterLoadDebug3.png\|500px\|center]]		[[file:ProB_PropagationAfterLoadDebug3.png\|500px\|center]]

	This will hopefully help us pinpoint the error in our properties. See [[Tutorial Troubleshooting the Setup]] for more ways to locate problems in the properties.		This will hopefully help us pinpoint the error in our properties. More recent versions of ProB also have a "Minimize" button in the lower left corner of the above dialog, in order to compute a minimal set of inconsistent properties. See [[Tutorial Troubleshooting the Setup]] for more ways to locate problems in the properties.
	After clicking "Done", we get the following; observe the orange timeout button in the "State Properties" pane:		After clicking "Done", we get the following; observe the orange timeout button in the "State Properties" pane:

Joy Clark: grammar and punctation

2011-04-18T12:37:07Z

grammar and punctation

← Older revision		Revision as of 12:37, 18 April 2011
Line 15:		Line 15:
	</pre>		</pre>

	* For limit=10,000 this takes 0.2 seconds (on a 2008 laptop); with the list representation this operation ran out of memory after 2 minutes in ProB 1.2.x.		* For limit=10,000, this takes 0.2 seconds (on a 2008 laptop); with the list representation this operation ran out of memory after 2 minutes in ProB 1.2.x.
	* For limit=100,000 this takes 2.1 seconds. (An encoding of this problem in Kodkod took 363 seconds on the same hardware.)		* For limit=100,000, this takes 2.1 seconds. (An encoding of this problem in Kodkod took 363 seconds on the same hardware.)
	* For limit=1,000,000 this takes about 21.9 seconds.		* For limit=1,000,000 this takes about 21.9 seconds.

Line 146:		Line 146:

	This will hopefully help us pinpoint the error in our properties. See [[Tutorial Troubleshooting the Setup]] for more ways to locate problems in the properties.		This will hopefully help us pinpoint the error in our properties. See [[Tutorial Troubleshooting the Setup]] for more ways to locate problems in the properties.
	After clicking Done, we get the following; observe the orange timeout button in the "State Properties" pane:		After clicking "Done", we get the following; observe the orange timeout button in the "State Properties" pane:

	[[file:ProB_PropagationAfterLoad3.png\|600px\|center]]		[[file:ProB_PropagationAfterLoad3.png\|600px\|center]]
Line 154:		Line 154:
	^CProlog interruption (h for help)?		^CProlog interruption (h for help)?
	</pre>		</pre>
	You can now type A followed by RETURN. This will typically raise an error message, which you can dismiss. Afterwards, you should be able to continue working.		You can now type A followed by RETURN. This will typically raise an error message which you can dismiss. Afterwards, you should be able to continue working.

	Finally, one can control the time after which a timeout will trigger using the preference "Time out for computing enabled transitions (in ms)" in the Animation Preferences. You can also control it using a definition for <tt>SET_PREF_TIME_OUT</tt> in the DEFINITIONS clause.		Finally, one can control the time after which a timeout will trigger using the preference "Time out for computing enabled transitions (in ms)" in the "Animation Preferences". You can also control it using a definition for <tt>SET_PREF_TIME_OUT</tt> in the DEFINITIONS clause.

	== Adding universally quantified formulas ==		== Adding universally quantified formulas ==
Line 169:		Line 169:

	ProB had no trouble finding a solution here. Indeed, it expanded the universally quantified formula before starting enumeration of <tt>f</tt>.		ProB had no trouble finding a solution here. Indeed, it expanded the universally quantified formula before starting enumeration of <tt>f</tt>.
	Here, it is important to understand ~~when~~ a universally quantified formula <tt>!x.(P=>Q)</tt> is expanded:		Here it is important to understand that a universally quantified formula <tt>!x.(P=>Q)</tt> is expanded:
	* either when it can fully determine all solutions to <tt>P</tt>; this involves knowing exactly all open variables appearing in <tt>P</tt>		* either when it can fully determine all solutions to <tt>P</tt>; this involves knowing exactly all open variables appearing in <tt>P</tt>
	* or when <tt>P</tt> is of the form <tt>x:S</tt> for some set S (the forall will be expanded for the known elements of S).		* or when <tt>P</tt> is of the form <tt>x:S</tt> for some set S (the forall will be expanded for the known elements of S).
Line 176:		Line 176:
	!x.(x:dom(f) => f(x)=x mod 2)		!x.(x:dom(f) => f(x)=x mod 2)
	</pre>		</pre>
	Here, the first case does not apply, as <tt>f</tt> is not yet fully known. Luckily, the formula is in of the second form and ProB will still be able to quickly find the single solution.		Here the first case does not apply as <tt>f</tt> is not yet fully known. Luckily, the formula is in of the second form and ProB will still be able to quickly find the single solution.

	However, if we use		However, if we use
Line 184:		Line 184:
	then none of the cases apply, and ProB will delay checking the formula until it knows <tt>f</tt>. As there are 2^101 possibilities, this will lead to a timeout.		then none of the cases apply, and ProB will delay checking the formula until it knows <tt>f</tt>. As there are 2^101 possibilities, this will lead to a timeout.

	Finally, in the current version of ProB (1.3) it is better to use <tt>!x.(x:low..up => f(x)=x mod 2)</tt> rather than the seemingly equivalent <tt>!x.(x>=low & x<=up => f(x)=x mod 2)</tt>. The former version is currently more efficient, especially for large values of MAXINT and MININT. (But we are planning to overcome this issue.)		Finally, in the current version of ProB (1.3) it is better to use <tt>!x.(x:low..up => f(x)=x mod 2)</tt> rather than the seemingly equivalent <tt>!x.(x>=low & x<=up => f(x)=x mod 2)</tt>. The former version is currently more efficient especially for large values of MAXINT and MININT. (But we are planning to overcome this issue.)

Joy Clark: /* Adding universally quantified formulas */ changed sentence structure

2011-04-12T14:02:29Z

Adding universally quantified formulas: changed sentence structure

← Older revision		Revision as of 14:02, 12 April 2011
Line 184:		Line 184:
	then none of the cases apply, and ProB will delay checking the formula until it knows <tt>f</tt>. As there are 2^101 possibilities, this will lead to a timeout.		then none of the cases apply, and ProB will delay checking the formula until it knows <tt>f</tt>. As there are 2^101 possibilities, this will lead to a timeout.

	Finally, in the current version of ProB (1.3) it is better to use <tt>!x.(x:low..up => f(x)=x mod 2)</tt> rather than the seemingly equivalent <tt>!x.(x>=low & x<=up => f(x)=x mod 2)</tt>. ~~Especially~~ for large values of MAXINT and MININT~~, the former version is currently more efficient~~. (But we are planning to overcome this issue.)		Finally, in the current version of ProB (1.3) it is better to use <tt>!x.(x:low..up => f(x)=x mod 2)</tt> rather than the seemingly equivalent <tt>!x.(x>=low & x<=up => f(x)=x mod 2)</tt>. The former version is currently more efficient, especially for large values of MAXINT and MININT. (But we are planning to overcome this issue.)

Joy Clark at 13:47, 12 April 2011

2011-04-12T13:47:23Z

← Older revision		Revision as of 13:47, 12 April 2011
Line 25:		Line 25:
	* a = 1 & b=2 & d = {a\|-b}		* a = 1 & b=2 & d = {a\|-b}
	then all values will be fully known and the new AVL-based representation will be used.		then all values will be fully known and the new AVL-based representation will be used.
	However, ~~for example~~ for		However, for
	* card(x) = 2 & dom(x) = {1,2}		* card(x) = 2 & dom(x) = {1,2}
	we would only have partial information about x (which the constraint solver will encode using the list <tt>[1\|->_, 2\|->_]</tt> where the underscore marks as of yet unknown bits.		we would only have partial information about x (which the constraint solver will encode using the list <tt>[1\|->_, 2\|->_]</tt> where the underscore marks as of yet unknown bits).

	Basically, the ProB constraint solver works as follows:		Basically, the ProB constraint solver works as follows:

Joy Clark: changed "grasped" to "have grasped"

2011-04-12T13:37:57Z

changed "grasped" to "have grasped"

← Older revision		Revision as of 13:37, 12 April 2011
Line 2:		Line 2:
	[[Category:User Manual]]		[[Category:User Manual]]

	We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].		We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].

	First, it is important to understand that as of version 1.3, ProB uses three representations for sets and relations:		First, it is important to understand that as of version 1.3, ProB uses three representations for sets and relations:

Michael Leuschel at 12:09, 24 March 2010

2010-03-24T12:09:41Z

← Older revision		Revision as of 12:09, 24 March 2010
Line 107:		Line 107:
	The arrow <tt>-->></tt> shows us when an AVL-representation was found for a constant. The <tt>====></tt> tells us when a predicate is interpreted.		The arrow <tt>-->></tt> shows us when an AVL-representation was found for a constant. The <tt>====></tt> tells us when a predicate is interpreted.
	You can also see that all constants have been valued '''before''' enumeration was started.		You can also see that all constants have been valued '''before''' enumeration was started.
	You can also see that ProB does '''not''' treat the predicates in the same order as you have typed them in the PROPERTIES clause: indeed, ProB sorts the properties (e.g., moving equalities earlier) before starting the interpretation.		You can also see that ProB does '''not''' treat the predicates in the same order as you have typed them in the PROPERTIES clause: indeed, ProB sorts the properties (e.g., moving equalities earlier) before starting the interpretation. As of version 1.3.2 the PROPERTIES are also partitioned, to improve performance and make it easier to locate inconsistencies.

	After selecting SETUP_CONSTANTS and INITIALISATION, we obtain the following state, and we can ensure ourselves that the values found for f and fi are correct (by looking at the "State Properties" pane):		After selecting SETUP_CONSTANTS and INITIALISATION, we obtain the following state, and we can ensure ourselves that the values found for f and fi are correct (by looking at the "State Properties" pane):

Michael Leuschel at 12:04, 24 March 2010

2010-03-24T12:04:58Z

← Older revision		Revision as of 12:04, 24 March 2010
Line 4:		Line 4:
	We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].		We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].

	First, it is important to understand that as of version 1.3, ProB uses ~~two~~ representations for sets and relations:		First, it is important to understand that as of version 1.3, ProB uses three representations for sets and relations:
	* a classical list representation		* a classical list representation
			* a symbolic representation (using what is called a closure)
	* a representation using AVL-trees.		* a representation using AVL-trees.
	The ~~second~~ representation allows ProB to deal with larger sets and relations (starting at around 100,000 elements performance will start to slow down). However, this representation can only be used if the constraint solver knows exactly '''all''' elements of a set or relation. The list representation will be used if only part of the set or relation is known.		The third representation allows ProB to deal with larger sets and relations (starting at around 100,000 elements performance will start to slow down). However, this representation can only be used if the constraint solver knows exactly '''all''' elements of a set or relation. The list representation will be used if only part of the set or relation is known. The symbolic representation can be used to represent certain sets (and set comprehensions) symbolically (such as large intervals, and to some very limited extent also infinite sets).

	To give an idea about the performance related to the new AVL-based representation, take the substitution		To give an idea about the performance related to the new AVL-based representation, take the substitution

Michael Leuschel: /* Adding universally quantified formulas */

2010-01-26T11:06:26Z

Adding universally quantified formulas

← Older revision		Revision as of 11:06, 26 January 2010
Line 170:		Line 170:
	Here, it is important to understand when a universally quantified formula <tt>!x.(P=>Q)</tt> is expanded:		Here, it is important to understand when a universally quantified formula <tt>!x.(P=>Q)</tt> is expanded:
	* either when it can fully determine all solutions to <tt>P</tt>; this involves knowing exactly all open variables appearing in <tt>P</tt>		* either when it can fully determine all solutions to <tt>P</tt>; this involves knowing exactly all open variables appearing in <tt>P</tt>
	* or when <tt>P</tt> is of the form <tt>x:S</tt> for some set S.		* or when <tt>P</tt> is of the form <tt>x:S</tt> for some set S (the forall will be expanded for the known elements of S).
	Take for example,		Take for example,
	<pre>		<pre>

Michael Leuschel: /* Complicating the Example */

2010-01-26T11:04:54Z

Complicating the Example

← Older revision		Revision as of 11:04, 26 January 2010
Line 126:		Line 126:
	[[file:ProB_PropagationAfterLoad2.png\|600px\|center]]		[[file:ProB_PropagationAfterLoad2.png\|600px\|center]]

	You can see that ProB had to problem with this machine. Still, one may wonder why it only proposes four solutions for the constants. Indeed, there should be 2^101 = 2.54e+30 different solutions (over 2 thousand billion billion billion solutions).		You can see that ProB had no problem with this machine. Still, one may wonder why it only proposes four solutions for the constants. Indeed, there should be 2^101 = 2.54e+30 different solutions (over 2 thousand billion billion billion solutions).
	In fact, as quite often there are a lot of solutions for the constants, ProB (luckily) does not compute all of them. Indeed, there is a cut-off point after which it will no longer search for more solutions. In this case, the orange button "max" appears in the "Enabled Operatoins" pane.		In fact, as quite often there are a lot of solutions for the constants, ProB (luckily) does not compute all of them. Indeed, there is a cut-off point after which it will no longer search for more solutions. In this case, the orange button "max" appears in the "Enabled Operatoins" pane.
	The cut-off itself is controlled by a preference. You can either		The cut-off itself is controlled by a preference. You can either

Michael Leuschel: /* Complicating the Example */

2010-01-22T15:04:28Z

Complicating the Example

← Older revision		Revision as of 15:04, 22 January 2010
Line 131:		Line 131:
	* change the preference "Max Number of Initialisations Computed" in the "Animation Preferences", or		* change the preference "Max Number of Initialisations Computed" in the "Animation Preferences", or
	* add a definition <tt>SET_PREF_MAX_INITIALISATIONS == xxx</tt>, where xxx is the maximum number of initialisations or possible ways to value the constants that ProB should compute.		* add a definition <tt>SET_PREF_MAX_INITIALISATIONS == xxx</tt>, where xxx is the maximum number of initialisations or possible ways to value the constants that ProB should compute.
	There is a similar preference to control how many solutions are found for ways to execute an operation (<tt>SET_PREF_MAX_OPERATIONS</tt>).		There is a similar preference to control how many solutions are found for ways to execute an operation (<tt>SET_PREF_MAX_OPERATIONS</tt>). (As a side note: these preferences can also be set to 0. This means that you will have to use "Execute an Operation..." in the Animate menu to add transitions one by one.)

	One may wonder what happens if there are no solutions. Will not ProB have to examine all of these solutions? The answer is: sometimes yes.		One may wonder what happens if there are no solutions. Will not ProB have to examine all of these solutions? The answer is: sometimes yes.