Tips: Writing Models for ProB: Difference between revisions

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

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.