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:
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).
Also, ProB will generate a warning when variable capture may occur.
See the page Using ProB with Atelier B for more details.
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.