(Created page with 'Category:User Manual * 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…') |
No edit summary |
||
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^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. |
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)