m (→Complexity of Animation: changed sentence order) |
m (→Complexity of Animation: fixed grammatical errors, changed word order, changed "possible enablings of the operation" to "possible ways to enable the operation") |
||
Line 49: | Line 49: | ||
== Complexity of Animation == | == Complexity of Animation == | ||
However, having addressed the undecidability issue still leaves open the problem of complexity. | 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, | 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 | 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. |
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 general, animation of a B model is undecidable. More precisely, it is undecidable to find out
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):
MACHINE Goldbach DEFINITIONS prime(x) == x>1 & !y.(y:NATURAL & y>1 & y<x => x mod y /= 0) OPERATIONS GoldbachNumber(x,p1,p2) = SELECT x:NATURAL & x mod 2 = 0 & x>2 & p1<x & p2<x & p1<=p2 & prime(p1) & prime(p2) & x = p1+p2 THEN skip END; NotGoldbachNumber(x) = SELECT x:NATURAL & x mod 2 = 0 & x>2 & !(p1,p2).(p1<x & p2<x & p1<=p2 & prime(p1) & prime(p2) => x /= p1+p2) THEN skip END END
If the conjecture is true, then the operation NotGoldbachNumber is disabled; if the conjecture is false then it is enabled.
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 x of NotGoldbachNumber only until MAXINT. Hence, if we set MAXINT to 16 (adding a definiton SET_PREF_MAXINT == 16) we get the following picture after executing the INITIALISATION:
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.
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 is required to fix the cardinality of every deferred set to a finite number before animation (see also Understanding the ProB Setup Phases on how you can control the cardinality of the deferred sets).
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, which declares rr to be a binary relation over -3..3:
rr : (-3..3) <-> (-3..3)
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 rr need to be examined. Even if ProB did enumerate 100,000 candidate solutions for rr per second, it would take over 178 years to check all solutions for rr. 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.
The following table shows how the size of a deferred set S influences the number of subsets, partial functions, relations over S, and a total function over relations of S:
card(S) | sub:POW(S) | pf:S+->S | rl: S<->S | tclos: (S<->S) --> (S<->S) |
---|---|---|---|---|
1 | 2 | 2 | 2 | 4 |
2 | 4 | 9 | 16 | 1.84e+19 |
3 | 8 | 64 | 512 | overflow |
4 | 16 | 624 | 65,536 | overflow |
5 | 32 | 7,776 | 33,554,432 | overflow |
6 | 64 | 117,649 | 6.87e+10 | overflow |
7 | 128 | 2,097,152 | 5.63e+14 | overflow |
8 | 256 | 43,046,721 | 1.85e+19 | overflow |
9 | 512 | 1,000,000,000 | 2.42e+24 | overflow |
n | 2^n | (n+1)^n | 2^n*n | (2^n*n)^(2^n*n) |
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 card(S)=2. (Note that the age of the universe is about 4e+17 seconds and 4e+26 nanoseconds.) For card(S)=3 the number of possible solutions (512^512) can no longer be represented as a standard floating point number.
In order to make a B model amenable to animation, we have three options:
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.