Current Limitations: Difference between revisions

No edit summary
No edit summary
 
(5 intermediate revisions by the same user not shown)
Line 6: Line 6:
Other general limitations are:
Other general limitations are:


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)</tt>.
* Trees and binary trees. These constructs are specific to the AtelierB tool and are only partially supported;  
 
* Trees and binary trees. These constructs are specific to the AtelierB tool and are not supported (the <tt>STRING</tt> type is now supported);  


* 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; definitions which are predicates or substitutions must be declared before first use. Also: the arguments of <tt>DEFINITIONS</tt> have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B).
* 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; definitions which are predicates or substitutions must be declared before first use. Also: the arguments of <tt>DEFINITIONS</tt> have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B).
 
Also, ProB will generate a warning when variable capture may occur.


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


* 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 the sequential composition (or other uses of the semicolon).
* 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 the sequential composition (or other uses of the semicolon). You also generally need to put BEGIN and END around the sequential composition operator, e.g., <tt>Op = BEGIN x:=1;y:=2 END</tt>.


See the page [[Using ProB with Atelier B]] for more details.
See the page [[Using ProB with Atelier B]] for more details.
Line 22: Line 20:
=== Multiple Machines and Refinements ===
=== 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.
It is possible to use multiple classical 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.
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 not yet check the gluing invariant.


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

Latest revision as of 12:53, 11 May 2023


ProB in general requires all deferred sets to be given a finite cardinality. If no cardinality is specified, a default size will be used. Also, unless finite bounds can be inferred by the ProB constraint solver, mathematical integers will only be enumerated within MININT to MAXINT (and ProB will generate enumeration warnings in case no solution is found).

Other general limitations are:

  • Trees and binary trees. These constructs are specific to the AtelierB tool and are only partially 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; definitions which are predicates or substitutions must be declared before first use. Also: the arguments of DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with PLUS(x,y) == x+y, the expression PLUS(2,3)*10 will evaluate to 50 (and not to 32 as with Atelier-B).

Also, ProB will generate a warning when variable capture may occur.

  • There are also limitations with refinements. See below;
  • VALUES This clause of IMPLEMENTATION machines is not yet fully supported;
  • Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write r2=rel;rel. You need to write r2=(rel;rel). This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon). You also generally need to put BEGIN and END around the sequential composition operator, e.g., Op = BEGIN x:=1;y:=2 END.

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

Multiple Machines and Refinements

It is possible to use multiple classical 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 not yet check the gluing invariant.

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