Current Limitations: Difference between revisions

No edit summary
No edit summary
Line 1: Line 1:
[[Category:User Manual]]
[[Category:User Manual]]


ProB requires all deferred sets to be given a finite cardinality. If no cardinality is specified, a default size will be used. Also, mathematical integers will only be enumerated within MININT to MAXINT (there is now some support for checking whether such an enumeration did occur, in particular when using the commands in the "Analyse Predicate" sub-menu).
ProB requires all deferred sets to be given a finite cardinality. If no cardinality is specified, a default size will be used. Also, mathematical integers will only be enumerated within <tt>MININT</tt> to <tt>MAXINT</tt> (there is now some support for checking whether such an enumeration did occur, in particular when using the commands in the "Analyse Predicate" sub-menu).


Other general limitations are:
Other general limitations are:
* <tt>closure</tt>. The transitive and reflexive closure operator of classical B, named <tt>closure</tt>, does not follow exactly the definition from the B-Book by Abrial. AtelierB also does not support the operator as defined in the B-Book (as this version cannot be applied in practice). For the reflexive component of <tt>closure</tt>, ProB will compute the elements in the domain and range of the relation (i.e., for ProB we have closure(r) = closure1(r) \/ id(dom(r) \/ ran(r))). As an example, <tt>closure({1|->2})</tt> equals <tt>{1|->1,2|->2,1|->2}</tt> in ProB, but is infinite according to the B-Book : <tt>{1|->2, 0|->0, 1|->1, -1|->-1, 2|->2,...}</tt>.
* <tt>closure</tt>. The transitive and reflexive closure operator of classical B, named <tt>closure</tt>, does not follow exactly the definition from the B-Book by Abrial. AtelierB also does not support the operator as defined in the B-Book (as this version cannot be applied in practice). For the reflexive component of <tt>closure</tt>, ProB will compute the elements in the domain and range of the relation (i.e., for ProB we have <tt>closure(r) = closure1(r) \/ id(dom(r) \/ ran(r)))</tt>. As an example, <tt>closure({1|->2})</tt> equals <tt>{1|->1,2|->2,1|->2}</tt> in ProB, but is infinite according to the B-Book : <tt>{1|->2, 0|->0, 1|->1, -1|->-1, 2|->2,...}</tt>.


Note however, that the transitive closure operator <tt>closure1</tt> is fully supported, and hence one can translate an expression closure(e), where e is a binary relation over some domain d, into the expression closure1(e) \/ id(d).
Note however, that the transitive closure operator <tt>closure1</tt> is fully supported, and hence one can translate an expression closure(e), where e is a binary relation over some domain d, into the expression <tt>closure1(e) \/ id(d).


* Trees and binary trees. These constructs are specific to the AtelierB tool and are not supported (the STRING type is now supported);  
* Trees and binary trees. These constructs are specific to the AtelierB tool and are not supported (the STRING type is now supported);  


* Definitions. Definitions (from the DEFINITIONS clause) with arguments are supported, but in contrast to AtelierB they are parsed independently and have to be either an expression, a predicate, or a substitution; Also: the arguments of DEFINITIONS have to be expressions.
* Definitions. Definitions (from the <tt>DEFINITIONS</tt> clause) with arguments are supported, but in contrast to AtelierB they are parsed independently and have to be either an expression, a predicate, or a substitution; Also: the arguments of <tt>DEFINITIONS</tt> have to be expressions.


* There are also limitations with refinements. See below;  
* There are also limitations with refinements. See below;  
* VALUES This clause of IMPLEMENTATION machines is not yet supported;
* <tt>VALUES</tt> This clause of <tt>IMPLEMENTATION</tt> machines is not yet supported;


See the page [[Using ProB with Atelier B]] for more details.
See the page [[Using ProB with Atelier B]] for more details.

Revision as of 16:03, 27 February 2012


ProB requires all deferred sets to be given a finite cardinality. If no cardinality is specified, a default size will be used. Also, mathematical integers will only be enumerated within MININT to MAXINT (there is now some support for checking whether such an enumeration did occur, in particular when using the commands in the "Analyse Predicate" sub-menu).

Other general limitations are:

  • closure. The transitive and reflexive closure operator of classical B, named closure, does not follow exactly the definition from the B-Book by Abrial. AtelierB also does not support the operator as defined in the B-Book (as this version cannot be applied in practice). For the reflexive component of closure, ProB will compute the elements in the domain and range of the relation (i.e., for ProB we have closure(r) = closure1(r) \/ id(dom(r) \/ ran(r))). As an example, closure({1|->2}) equals {1|->1,2|->2,1|->2} in ProB, but is infinite according to the B-Book : {1|->2, 0|->0, 1|->1, -1|->-1, 2|->2,...}.

Note however, that the transitive closure operator closure1 is fully supported, and hence one can translate an expression closure(e), where e is a binary relation over some domain d, into the expression closure1(e) \/ id(d).

  • Trees and binary trees. These constructs are specific to the AtelierB tool and are not supported (the STRING type is now supported);
  • Definitions. Definitions (from the DEFINITIONS clause) with arguments are supported, but in contrast to AtelierB they are parsed independently and have to be either an expression, a predicate, or a substitution; Also: the arguments of DEFINITIONS have to be expressions.
  • There are also limitations with refinements. See below;
  • VALUES This clause of IMPLEMENTATION machines is not yet supported;

See the page Using ProB with Atelier B for more details.

Multiple Machines and Refinements

It is possible to use multiple B machines with ProB. However, ProB may not enforce all of the classical B visibility rules (although we try to). As far as the visibility rules are concerned, it is thus a good idea to check the machines in another B tool, such as Atelier B or the B-Toolkit.

While refinements are supported, the preconditions of operations are not propagated down to refinement machines. This means that you should rewrite the preconditions of operations (and, if necessary, reformulate them in terms of the variables of the refinement machine). Also, the refinement checker does yet check the gluing invariant.

Note however, that for Rodin Event-B models we now support multi-level animation and validation.