|
|
| 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^n*n)^(2^n*n)</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^n*n)^(2^n*n)</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. |
Revision as of 10:54, 21 November 2012
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.
- 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. For example, Event-B does not have a transitive closure operator (classical B has closure1). As such, the transitive closure is often axiomatised 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). 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.