Line 25: | Line 25: | ||
=== Limitations === | === Limitations === | ||
ProB | * Parsing: ProB will require parentheses around the comma, the relational composition and parallel product operators. For example, you cannot write <tt>r2=rel;rel</tt>. You need to write <tt>r2=(rel;rel)</tt>. This allows ProB to distinguish the relational composition from sequential composition (or other uses of the semicolon). | ||
* Well-Definedness:ProB will try to check well-definedness of your predicates during animation or model checking. For this, ProB assumes (similar to Rodin) a stricter left-to-right definition of well-definedness than Atelier B. | |||
* closure The transitive and reflexive closure operator of classical B is not supported as defined in 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. | * closure The transitive and reflexive closure operator of classical B is not supported as defined in 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. | ||
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). | 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). | ||
* fnc, rel These operators are not supported. Also, succ and pred are only supported when applied to numbers (i.e., succ(x) is supported; dom(succ) is not). | * Unsupported Operators: | ||
** fnc, rel These operators are not supported. Also, succ and pred are only supported when applied to numbers (i.e., succ(x) is supported; dom(succ) is not). | |||
* Trees and binary trees. These onstructs | ** Trees and binary trees. These onstructs are not supported (the STRING type is now supported); | ||
** VALUES This clause of IMPLEMENTATION machines is not yet supported; | ** VALUES This clause of IMPLEMENTATION machines is not yet supported; | ||
See | * There are also limitations wrt refinements. See ... | ||
=== Multiple Machines and Refinements === | === Multiple Machines and Refinements === |
As of version 1.3, ProB contains a much improved parser which tries be compliant with Atelier B as much as possible.
There is also a plugin for Atelier B, in order to use the standalone Tcl/Tk Version on Atelier B projects.
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).
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 reformulate them in terms of the variables of the refinement machine, if necessary). Also, the refinement checker does yet check the gluing invariant.