Tips: Writing Models for ProB: Difference between revisions

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 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 !s.(s<:S => P) will have to check P for all subsets of S (i.e., checking is exponential in the size of S)

• 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 set the symbolic preference of ProB to true (use -p SYMBOLIC TRUE 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 ABSTRACT_CONSTANT 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 #x.P 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 one 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 #x.(x=E & P). 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 #x.(x=E & P) 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 !x.(P=>Q) until all variables in P are known so as to be able to determine all values of x for which Q has to be checked.

There are a few optimisations:

• if ProB can determine that the domain of x is finite and small, then the universal quantifier will be expanded into a conjunction. E.g., !x.(x:1..3 & x<y => P(x) will be expanded into (1<y => P(1)) & (2<y => P(2)) & (3<y => P(3)) even if y is not yet known. Setting the preference SMT to true will increase the threshold for which this expansion occurs.
• if the quantifier is of the form !x.(x:S => P), then P will be gradually checked for every new value that is added to S; ProB does not wait for S 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 s is a subset of 1..10, then we can rewrite !x.(s(x)=5 => P(x) into !x.(x:1..10 => (s(x)=5 => P(x)). This will ensure that the quantifier is checked

Transitive Closure in Event-B

Classical B contains the transitive closure operator closure1. 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 tclos from relations to relations, ProB will try to find a value for tclos. The search space for this function is (2^n*n)^(2^n*n), where n is the size of the base set (see Tutorial Understanding the Complexity of B Animation). 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. See 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 dom({x,y|P}) rather than {x|#y.P}. This is generally more efficient.