Tutorial Understanding the Complexity of B Animation - Revision history

Michael Leuschel: /* Complexity of Animation */

2013-03-26T09:42:40Z

Complexity of Animation

← Older revision		Revision as of 09:42, 26 March 2013
Line 83:		Line 83:
	\| 64		\| 64
	\|512		\|512
	\| overflow		\| overflow (1.40e+1387)
	\|-		\|-
	\|4		\|4
Line 89:		Line 89:
	\| 624		\| 624
	\| 65,536		\| 65,536
	\| overflow		\| overflow (6.74e+315652)
	\|-		\|-
	\|5		\|5
Line 130:		Line 130:
	tclos is actually the type of a function that does appear in some models (often Event-B models): namely, the transitive closure which gets a relation as argument and computes its transitive closure. As you can see, we already run into problems with a <tt>card(S)=2</tt>.		tclos is actually the type of a function that does appear in some models (often Event-B models): namely, the transitive closure which gets a relation as argument and computes its transitive closure. As you can see, we already run into problems with a <tt>card(S)=2</tt>.
	(Note that the age of the universe is about 4e+17 seconds and 4e+26 nanoseconds.)		(Note that the age of the universe is about 4e+17 seconds and 4e+26 nanoseconds.)
	For <tt>card(S)=3</tt> the number of possible solutions (512^512) can no longer be represented as a standard floating point number.		For <tt>card(S)=3</tt> the number of possible solutions (512^512) can no longer be represented as a standard floating point number (it is roughly 1.40e1387 and is a number with 1388 digits).

Joy Clark: grammar and punctuation

2011-04-18T12:30:14Z

grammar and punctuation

← Older revision		Revision as of 12:30, 18 April 2011
Line 4:		Line 4:
	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]].		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]].

	In this lesson, we examine the complexity of animation of B models in general, how ProB solves this problem and what the ramification for users are.		In this lesson, we examine the complexity of animation of B models in general, how ProB solves this problem, and what the ramification for users are.


Line 42:		Line 42:
	We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.		We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.

	Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB, so as to highlight predicates over mathematical integers which are potentially problematic.		Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB so as to highlight predicates over mathematical integers which are potentially problematic.

	The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets can be unknown, and they may even be infinite.		The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets can be unknown, and they may even be infinite.
Line 49:		Line 49:
	== Complexity of Animation ==		== Complexity of Animation ==

	However, ~~having addressed~~ the undecidability issue still ~~leaves open~~ the problem of complexity. The animation task can be arbitrarily complex even for finite sets and implementable integers.		However, after addressing the undecidability issue, there is still the problem of complexity. The animation task can be arbitrarily complex even for finite sets and implementable integers.
	Take for example the following predicate, which declares <tt>rr</tt> to be a binary relation over -3..3:		Take for example the following predicate, which declares <tt>rr</tt> to be a binary relation over -3..3:
	<pre>		<pre>

Joy Clark: /* Complexity of Animation */ fixed grammatical errors, changed word order, changed "possible enablings of the operation" to "possible ways to enable the operation"

2011-04-12T14:44:21Z

Complexity of Animation: fixed grammatical errors, changed word order, changed "possible enablings of the operation" to "possible ways to enable the operation"

← Older revision		Revision as of 14:44, 12 April 2011
Line 49:		Line 49:
	== Complexity of Animation ==		== Complexity of Animation ==

	However, having addressed the undecidability issue still leaves open the problem of complexity. ~~Indeed,~~ even for finite sets and implementable integers~~, the animation task can be arbitrarily complex~~.		However, having addressed the undecidability issue still leaves open the problem of complexity. The animation task can be arbitrarily complex even for finite sets and implementable integers.
	Take for example the following predicate, ~~declaring~~ <tt>rr</tt> to be a binary relation over -3..3:		Take for example the following predicate, which declares <tt>rr</tt> to be a binary relation over -3..3:
	<pre>		<pre>
	rr : (-3..3) <-> (-3..3)		rr : (-3..3) <-> (-3..3)
	</pre>		</pre>
	This predicate could be part of a precondition of an operation. In order to find possible ~~enablings of~~ the operation the possible values for <tt>rr</tt> need to be examined.		This predicate could be part of a precondition of an operation. In order to find possible ways to enable the operation, the possible values for <tt>rr</tt> need to be examined.
	Even if ProB did enumerate 100,000 candidate solutions for <tt>rr</tt> per second, it would take over 178 years to check all solutions for <tt>rr</tt>. Indeed, there are 49 possible pairs of values between -3 and 3 and hence 2^49 = 562,949,953,421,312 binary relations over -3..3.		Even if ProB did enumerate 100,000 candidate solutions for <tt>rr</tt> per second, it would take over 178 years to check all solutions for <tt>rr</tt>. Indeed, there are 49 possible pairs of values between -3 and 3 and hence 2^49 = 562,949,953,421,312 binary relations over -3..3.

Line 138:		Line 138:
	* hope that the constraint solver of ProB will be able to find a solution.		* hope that the constraint solver of ProB will be able to find a solution.

	In the next part of the tutorial we will explain in more detail how the constraint solver of ProB works, so that you will be in a better position to write specifications which can be successfully animated or validated.		In the next part of the tutorial, we will explain in more detail how the constraint solver of ProB works, so that you will be in a better position to write specifications which can be successfully animated or validated.

Joy Clark: /* Complexity of Animation */ changed sentence order

2011-04-12T13:36:17Z

Complexity of Animation: changed sentence order

← Older revision		Revision as of 13:36, 12 April 2011
Line 128:		Line 128:
	\|}		\|}

	tclos is actually the type of a function that does appear in some models (often Event-B models): namely, the transitive closure which gets a relation as argument and computes its transitive closure. As you can see, already ~~for~~ a <tt>card(S)=2</tt> ~~we run into problems~~.		tclos is actually the type of a function that does appear in some models (often Event-B models): namely, the transitive closure which gets a relation as argument and computes its transitive closure. As you can see, we already run into problems with a <tt>card(S)=2</tt>.
	(Note that the age of the universe is about 4e+17 seconds and 4e+26 nanoseconds.)		(Note that the age of the universe is about 4e+17 seconds and 4e+26 nanoseconds.)
	For <tt>card(S)=3</tt> the number of possible solutions (512^512) can no longer be represented as a standard floating point number.		For <tt>card(S)=3</tt> the number of possible solutions (512^512) can no longer be represented as a standard floating point number.

Joy Clark: /* Undecidability */ edited commas, changed "requires" to "is required"

2011-04-12T13:32:14Z

Undecidability: edited commas, changed "requires" to "is required"

← Older revision		Revision as of 13:32, 12 April 2011
Line 42:		Line 42:
	We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.		We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.

	Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend, using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB, so as to highlight predicates over mathematical integers which are potentially problematic.		Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB, so as to highlight predicates over mathematical integers which are potentially problematic.

	The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets can be unknown and they may even be infinite.		The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets can be unknown, and they may even be infinite.
	To overcome this issue, ProB ~~requires~~ to fix the cardinality of every deferred set to a finite number before animation (see also [[Tutorial Setup Phases\|Understanding the ProB Setup Phases]] on how you can control the cardinality of the deferred sets).		To overcome this issue, ProB is required to fix the cardinality of every deferred set to a finite number before animation (see also [[Tutorial Setup Phases\|Understanding the ProB Setup Phases]] on how you can control the cardinality of the deferred sets).

	== Complexity of Animation ==		== Complexity of Animation ==

Joy Clark: grasped to have grasped

2011-04-12T13:25:57Z

grasped to have grasped

← Older revision		Revision as of 13:25, 12 April 2011
Line 2:		Line 2:


	We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]].		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]].

	In this lesson, we examine the complexity of animation of B models in general, how ProB solves this problem and what the ramification for users are.		In this lesson, we examine the complexity of animation of B models in general, how ProB solves this problem and what the ramification for users are.

Michael Leuschel: /* Complexity of Animation */

2010-07-26T20:13:08Z

Complexity of Animation

← Older revision		Revision as of 20:13, 26 July 2010
Line 135:		Line 135:
	In order to make a B model amenable to animation, we have three options:		In order to make a B model amenable to animation, we have three options:
	* use small cardinalities for the deferred sets and avoid using overly complicated datastructures (e.g., relations over relations or total functions over relations)		* use small cardinalities for the deferred sets and avoid using overly complicated datastructures (e.g., relations over relations or total functions over relations)
	* ensure that ProB does not have to enumerate variables with complicated types, by providing concrete values (e.g., in the form of an equality <tt>rel = {1\|->2, 2\|->3, 3\|->1}</tt>		* ensure that ProB does not have to enumerate variables with complicated types, by providing concrete values (e.g., in the form of an equality such as <tt>rel = {1\|->2, 2\|->3, 3\|->1}</tt>)
	* hope that the constraint solver of ProB will be able to find a solution.		* hope that the constraint solver of ProB will be able to find a solution.

	In the next part of the tutorial we will explain in more detail how the constraint solver of ProB works, so that you will be in a better position to write specifications which can be successfully animated or validated.		In the next part of the tutorial we will explain in more detail how the constraint solver of ProB works, so that you will be in a better position to write specifications which can be successfully animated or validated.

Michael Leuschel: /* Undecidability */

2010-07-26T20:11:58Z

Undecidability

← Older revision		Revision as of 20:11, 26 July 2010
Line 9:		Line 9:
	== Undecidability ==		== Undecidability ==

	In general, animation of a B model is undecidable. ~~I.e.~~, it is undecidable		In general, animation of a B model is undecidable. More precisely, it is undecidable to find out
	* whether a solution to the PROPERTIES can be found,		* whether a solution to the PROPERTIES can be found,
	* whether a valid INITIALISATION exists and		* whether a valid INITIALISATION exists and

Michael Leuschel: /* Undecidability */

2010-03-24T11:56:54Z

Undecidability

← Older revision		Revision as of 11:56, 24 March 2010
Line 9:		Line 9:
	== Undecidability ==		== Undecidability ==

	In general, animation of a B model is undecidable. I.e., it is undecidable whether a solution to the PROPERTIES can be found, whether a valid INITIALISATION exists and whether an operation can be applied.		In general, animation of a B model is undecidable. I.e., it is undecidable
			* whether a solution to the PROPERTIES can be found,
			* whether a valid INITIALISATION exists and
			* whether any given operation can be applied.

	For example, the following B machine encodes Goldbach's conjecture (that every even number greater than 2 is a Goldbach number, i.e., it can be expressed as the sum of two primes):		For example, the following B machine encodes Goldbach's conjecture (that every even number greater than 2 is a Goldbach number, i.e., it can be expressed as the sum of two primes):
Line 31:		Line 34:


	How does ProB overcome undecidability. First, it will enumerate integer variables only between MININT and MAXINT (unless the machine itself fixes the value to be outside of that range).		How does ProB overcome undecidability? First, it will enumerate integer variables only between MININT and MAXINT (unless the machine itself fixes the value to be outside of that range).
	Hence, ProB will look for solutions to the parameter <tt>x</tt> of NotGoldbachNumber only until MAXINT. Hence, if we set MAXINT to 16 (adding a definiton <tt>SET_PREF_MAXINT == 16</tt>) we get the following picture after executing the INITIALISATION:		Hence, ProB will look for solutions to the parameter <tt>x</tt> of NotGoldbachNumber only until MAXINT. Hence, if we set MAXINT to 16 (adding a definiton <tt>SET_PREF_MAXINT == 16</tt>) we get the following picture after executing the INITIALISATION:

Line 39:		Line 42:
	We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.		We can see that 10 can be expressed as the sum 5+5 or 3+7. At least until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is disabled.

	Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend, using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB ~~which~~ to highlight predicates over mathematical integers which are potentially problematic.		Note, that this restriction (of enumerating only between MININT and MAXINT) means that ProB is in general incomplete and sometimes unsound when using mathematical integers. We recommend, using the implementable integers only (INT, NAT, NAT1). In future, we plan to integrate an interval analysis into ProB, so as to highlight predicates over mathematical integers which are potentially problematic.

	The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets ~~maybe~~ unknown and they may even be infinite.		The mathematical integers are, however, not the only source of undecidability. Another source stems from the deferred sets. Indeed, the size of those sets can be unknown and they may even be infinite.
	To overcome this issue, ProB requires to fix the cardinality of every deferred set to a finite number before animation (see also [[Tutorial Setup Phases\|Understanding the ProB Setup Phases]] on how you can control the cardinality of the deferred sets).		To overcome this issue, ProB requires to fix the cardinality of every deferred set to a finite number before animation (see also [[Tutorial Setup Phases\|Understanding the ProB Setup Phases]] on how you can control the cardinality of the deferred sets).

Michael Leuschel: /* Complexity of Animation */

2010-01-19T13:36:44Z

Complexity of Animation

← Older revision		Revision as of 13:36, 19 January 2010
Line 134:		Line 134:
	* ensure that ProB does not have to enumerate variables with complicated types, by providing concrete values (e.g., in the form of an equality <tt>rel = {1\|->2, 2\|->3, 3\|->1}</tt>		* ensure that ProB does not have to enumerate variables with complicated types, by providing concrete values (e.g., in the form of an equality <tt>rel = {1\|->2, 2\|->3, 3\|->1}</tt>
	* hope that the constraint solver of ProB will be able to find a solution.		* hope that the constraint solver of ProB will be able to find a solution.

			In the next part of the tutorial we will explain in more detail how the constraint solver of ProB works, so that you will be in a better position to write specifications which can be successfully animated or validated.