View source for Tips: Writing Models for ProB

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