Tips: Writing Models for ProB - Revision history

Michael Leuschel: /* Existential Quantifiers */

2016-09-16T09:06:27Z

Existential Quantifiers

← Older revision		Revision as of 09:06, 16 September 2016
Line 29:		Line 29:
	One exception to the above treatment are existential quantifiers of the form <tt>#x.(x=E & P)</tt>. They are recognised by ProB as LET-PREDICATES. This is a good use of the existential quantifier. This quantifier will never "block".		One exception to the above treatment are existential quantifiers of the form <tt>#x.(x=E & P)</tt>. They are recognised by ProB as LET-PREDICATES. This is a good use of the existential quantifier. This quantifier will never "block".

	* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-~~subexpresion~~ elimination) and to make your predicates more readable		* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations ([[Common_Subexpression_Elimination\|common-subexpression elimination]]) and to make your predicates more readable

	== Universal Quantifiers ==		== Universal Quantifiers ==

Michael Leuschel: /* Existential Quantifiers */

2016-02-08T12:45:07Z

Existential Quantifiers

← Older revision		Revision as of 12:45, 8 February 2016
Line 30:		Line 30:

	* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable		* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable

			== Universal Quantifiers ==
			The situation is very similar to the existential quantifier.
			In the worst case ProB may delay evaluating a universal quantifier <tt>!x.(P=>Q)</tt> until all variables in <tt>P</tt> are known so as to be able to determine all values of <tt>x</tt> for which <tt>Q</tt> has to be checked.

			There are a few optimisations:
			* if ProB can determine that the domain of <tt>x</tt> is finite and small, then the universal quantifier will be expanded into a conjunction. E.g., <tt>!x.(x:1..3 & x<y => P(x)</tt> will be expanded into <tt>(1<y => P(1)) & (2<y => P(2)) & (3<y => P(3))</tt> even if <tt>y</tt> is not yet known. Setting the preference <tt>SMT</tt> to true will increase the threshold for which this expansion occurs.
			* if the quantifier is of the form <tt>!x.(x:S => P)</tt>, then P will be gradually checked for every new value that is added to <tt>S</tt>; ProB does not wait for <tt>S</tt> to be completely known before checking the quantifier.

			Tip: sometimes one can force expansion of a quantifier by using two implications.
			E.g., suppose we know that the domain of <tt>s</tt> is a subset of <tt>1..10</tt>, then we can rewrite <tt>!x.(s(x)=5 => P(x)</tt> into <tt>!x.(x:1..10 => (s(x)=5 => P(x))</tt>. This will ensure that the quantifier is checked

	== Transitive Closure in Event-B ==		== Transitive Closure in Event-B ==

Michael Leuschel: /* Transitive Closure in Event-B */

2016-02-03T15:14:57Z

Transitive Closure in Event-B

← Older revision		Revision as of 15:14, 3 February 2016
Line 35:		Line 35:
	It is not available by default in Event-B, and axiomatisations of it may be very difficult to treat by ProB.		It is not available by default in Event-B, and axiomatisations of it may be very difficult to treat by ProB.
	Indeed, if you define the transitive closure in Event-B as a function <tt>tclos</tt> from relations to relations, ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]).		Indeed, if you define the transitive closure in Event-B as a function <tt>tclos</tt> from relations to relations, ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]).
	For n>2 this is already way too big too handle.		For n=3 this is already way too big too handle (the search space has 1.40e+1387 relations).

	Hence, in Event-B, you should use a theory of the transitive closure which contains a special mapping file which instructs ProB to use the classical B operator.		Hence, in Event-B, you should use a theory of the transitive closure which contains a special mapping file which instructs ProB to use the classical B operator.

Michael Leuschel at 15:12, 3 February 2016

2016-02-03T15:12:18Z

← Older revision		Revision as of 15:12, 3 February 2016
Line 10:		Line 10:
	* You may wish to give explicit values to certain constants. For example, in Event-B, this can be done by refining a context.		* You may wish to give explicit values to certain constants. For example, in Event-B, this can be done by refining a context.

	* ~~Set~~ the symbolic preference of ProB to true (use <tt>-p SYMBOLIC TRUE</tt> for probcli or set the Animation preference "Lazy expansion ... (SYMBOLIC)" to true) if you have large or infinite functions~~. For example, Event-B does not have a transitive closure operator~~ (~~classical B has <tt>closure1</tt>). As such, the transitive~~ closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. In classical B, any <tt>ABSTRACT_CONSTANT</tt> will also at first be kept symbolic. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.		* Try to set the symbolic preference of ProB to true (use <tt>-p SYMBOLIC TRUE</tt> for probcli or set the Animation preference "Lazy expansion ... (SYMBOLIC)" to true) if you have large or infinite functions (see discussion about closure below). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. In classical B, any <tt>ABSTRACT_CONSTANT</tt> will also at first be kept symbolic. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.

	== Effective Constraint Solving with ProB ==		== Effective Constraint Solving with ProB ==
Line 31:		Line 31:
	* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable		* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable

			== Transitive Closure in Event-B ==
			Classical B contains the transitive closure operator <tt>closure1</tt>.
			It is not available by default in Event-B, and axiomatisations of it may be very difficult to treat by ProB.
			Indeed, if you define the transitive closure in Event-B as a function <tt>tclos</tt> from relations to relations, ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]).
			For n>2 this is already way too big too handle.

			Hence, in Event-B, you should use a theory of the transitive closure which contains a special mapping file which instructs ProB to use the classical B operator.
			See [[Event-B_Theories\|the page on supporting Event-B theories]] along with the links to theories that can be used efficiently with ProB.

	* Tip: within set comprehensions use the form <tt>dom({x,y\|P})</tt> rather than <tt>{x\|#y.P}</tt>. This is generally more efficient.		* Tip: within set comprehensions use the form <tt>dom({x,y\|P})</tt> rather than <tt>{x\|#y.P}</tt>. This is generally more efficient.

Michael Leuschel: /* Existential Quantifiers */

2015-10-31T07:07:16Z

Existential Quantifiers

← Older revision		Revision as of 07:07, 31 October 2015
Line 30:		Line 30:

	* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable		* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable


			* Tip: within set comprehensions use the form <tt>dom({x,y\|P})</tt> rather than <tt>{x\|#y.P}</tt>. This is generally more efficient.

Michael Leuschel at 07:06, 31 October 2015

2015-10-31T07:06:02Z

← Older revision		Revision as of 07:06, 31 October 2015
Line 11:		Line 11:

	* Set the symbolic preference of ProB to true (use <tt>-p SYMBOLIC TRUE</tt> for probcli or set the Animation preference "Lazy expansion ... (SYMBOLIC)" to true) if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. In classical B, any <tt>ABSTRACT_CONSTANT</tt> will also at first be kept symbolic. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.		* Set the symbolic preference of ProB to true (use <tt>-p SYMBOLIC TRUE</tt> for probcli or set the Animation preference "Lazy expansion ... (SYMBOLIC)" to true) if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. In classical B, any <tt>ABSTRACT_CONSTANT</tt> will also at first be kept symbolic. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.

			== Effective Constraint Solving with ProB ==

			=== Existential Quantifiers ===
			Existential quantifiers can pose subtle problems when solving constraint problems.

			For an existential quantifier <tt>#x.P</tt> ProB will often wait until all variables in P apart from x are known to evaluate the quantifier. Indeed, if all variables apart from x are known, ProB can stop when it finds <b>one</b> solution for x. Take for example:
			#x.(x:0..1000 & x=p) & p:101..104
			Here, ProB will wait until p is known (e.g., 101) before enumerating possible values for x.
			However, it could be that the predicate P is required to instantiate the outside variable, as in this example:
			#x.(x:100..101 & x=p) & p:NATURAL
			Here, the existential quantifier is required to narrow down the possible values of p. Thus, before enumerating an unbounded variable, ProB will start enumerating the existential variable x.
			Note, however, that the priority with which it will be enumerated is much lower than if it was a regular variable!
			Hence:
			* Tip: Beware of putting important domain variables into existential quantifiers.

			One exception to the above treatment are existential quantifiers of the form <tt>#x.(x=E & P)</tt>. They are recognised by ProB as LET-PREDICATES. This is a good use of the existential quantifier. This quantifier will never "block".

			* Tip: use existential quantifiers as LET-PREDICATES <tt>#x.(x=E & P)</tt> to avoid repeated computations (common-subexpresion elimination) and to make your predicates more readable

Michael Leuschel at 10:54, 21 November 2012

2012-11-21T10:54:43Z

← Older revision		Revision as of 10:54, 21 November 2012
Line 10:		Line 10:
	* You may wish to give explicit values to certain constants. For example, in Event-B, this can be done by refining a context.		* You may wish to give explicit values to certain constants. For example, in Event-B, this can be done by refining a context.

	* ~~Try to use~~ the symbolic ~~mode~~ of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.		* Set the symbolic preference of ProB to true (use <tt>-p SYMBOLIC TRUE</tt> for probcli or set the Animation preference "Lazy expansion ... (SYMBOLIC)" to true) if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. In classical B, any <tt>ABSTRACT_CONSTANT</tt> will also at first be kept symbolic. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.

Joy Clark: added a space, changed sentence order, added "the"

2011-04-12T14:22:32Z

added a space, changed sentence order, added "the"

← Older revision		Revision as of 14:22, 12 April 2011
Line 8:		Line 8:
	* Try to put complicated properties into ASSERTIONS rather than PROPERTIES. Something like <tt>!s.(s<:S => P)</tt> will have to check <tt>P</tt> for all subsets of <tt>S</tt> (i.e., checking is exponential in the size of <tt>S</tt>)		* Try to put complicated properties into ASSERTIONS rather than PROPERTIES. Something like <tt>!s.(s<:S => P)</tt> will have to check <tt>P</tt> for all subsets of <tt>S</tt> (i.e., checking is exponential in the size of <tt>S</tt>)

	* You may wish to give explicit values to certain constants.In Event-B, this can be done by refining a context~~, for example~~.		* You may wish to give explicit values to certain constants. For example, in Event-B, this can be done by refining a context.

	* Try to use symbolic mode of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.		* Try to use the symbolic mode of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.

Michael Leuschel at 08:36, 2 March 2011

2011-03-02T08:36:45Z

← Older revision		Revision as of 08:36, 2 March 2011
Line 10:		Line 10:
	* You may wish to give explicit values to certain constants.In Event-B, this can be done by refining a context, for example.		* You may wish to give explicit values to certain constants.In Event-B, this can be done by refining a context, for example.

	* Try to use symbolic mode of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible.		* Try to use symbolic mode of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible. However, there are only limited things you can do with a "symbolic" function without forcing an expansion: taking the value of a function is fine, computing the image over a set is also possible as is taking the union with another symbolic function.

Michael Leuschel at 08:35, 2 March 2011

2011-03-02T08:35:01Z

← Older revision		Revision as of 08:35, 2 March 2011
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]


			The most common issue is that ProB needs to find values for the constants which satisfy the properties (aka axioms in Event-B). You should read the tutorial pages on this (in particular [[Tutorial Setup Phases\|Understanding the ProB Setup Phases]] and [[Tutorial Troubleshooting the Setup]])

			* Try to use ProB as early as possible in the modeling process; this will make it easier to identify the cause of problems (and also will hopefully give you valuable feedback on your model as well).

	* Try to put complicated properties into ASSERTIONS rather than PROPERTIES. Something like <tt>!s.(s<:S => P)</tt> will have to check <tt>P</tt> for all subsets of <tt>S</tt> (i.e., checking is exponential in the size of <tt>S</tt>)		* Try to put complicated properties into ASSERTIONS rather than PROPERTIES. Something like <tt>!s.(s<:S => P)</tt> will have to check <tt>P</tt> for all subsets of <tt>S</tt> (i.e., checking is exponential in the size of <tt>S</tt>)

			* You may wish to give explicit values to certain constants.In Event-B, this can be done by refining a context, for example.

			* Try to use symbolic mode of ProB if you have large or infinite functions. For example, Event-B does not have a transitive closure operator (classical B has <tt>closure1</tt>). As such, the transitive closure is often axiomatised in Event-B as a function <tt>tclos</tt> from relations to relations. ProB will try to find a value for <tt>tclos</tt>. The search space for this function is <tt>(2^nn)^(2^nn)</tt>, where <tt>n</tt> is the size of the base set (see [[Tutorial Understanding the Complexity of B Animation]]). In symbolic mode, ProB will keep lambda expressions and set comprehensions symbolic as much as possible.