Current Limitations: Difference between revisions
No edit summary |
No edit summary |
||
| Line 6: | Line 6: | ||
Other general limitations are: | Other general limitations are: | ||
* closure The transitive and reflexive closure operator 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). | ||
| Line 14: | Line 14: | ||
* Trees and binary trees. These onstructs are specific to AtelierB tool and are not supported (the STRING type is now supported); | * Trees and binary trees. These onstructs are specific to AtelierB tool and are not supported (the STRING type is now supported); | ||
* Definitions Definitions (from the DEFINITIONS clause) with arguments are | * Definitions Definitions (from the DEFINITIONS clause) with arguments are supported, but in contrast to AtelierB they are type-checked and have to be either an expression, a predicate or a substitution; | ||
** There are also limitations wrt refinements. See below; | ** There are also limitations wrt refinements. See below; | ||
** VALUES This clause of IMPLEMENTATION machines is not yet supported; | ** VALUES This clause of IMPLEMENTATION machines is not yet supported; | ||
| Line 20: | Line 20: | ||
=== Multiple Machines and Refinements === | === Multiple Machines and Refinements === | ||
It is possible to use multiple machines with ProB. However, ProB may not enforce all of the 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. | 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 | 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. | ||
Note, however, that for Rodin Event-B models we now support multi-level animation and validation. | |||
Revision as of 12:58, 18 January 2010
|
Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
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.
Other general limitations are:
- 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).
- 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 are specific to 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 type-checked and have to be either an expression, a predicate or a substitution;
- There are also limitations wrt refinements. See below;
- VALUES This clause of IMPLEMENTATION machines is not yet supported;
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 reformulate them in terms of the variables of the refinement machine, if necessary). 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.