Tips: Writing Models for ProB: Difference between revisions

Revision as of 08:35, 2 March 2011

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.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 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.

@@ Line 1: / Line 1: @@
 [[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>)
+* 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.