Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
ProB requires all constants and variables to be typed. As of version 1.3, ProB uses a new unification-based type inference and checking algorithm. As such, you should be able to use most Atelier B models without problem. On the other hand, certain models that ProB accepts will have to be rewritten to be type checked by Atelier B (e.g., by adding additional typing predicates). Also note that, in contrast to Atelier B, ProB will type check macro DEFINITIONS.
Generally speaking, any constant or variable. More precisely:
ProB will warn you if a variable has not been given a type.
HINT: The Analyse|Show Typing command reveals the typing that ProB has inferred for your constants and global variables.
Animating and verifying a B specification is in principle undecidable. ProB overcomes this by requiring that the domain of the variables is finite (i.e., with finitely many values) or integer. This ensures that the state space has finite size. Typing of the B specification ensures this restriction.
In the B specification, a set is either defined explicitely, thus being a finite domain, or its definition is deferred. In the later case, the user can indicate the size of the set mySET (without defining its elements) by creating a macro in the DEFINITIONS clause with the name scope_mySET and an integer value (e.g. scope_mySET==2) or a value specified as a range (e.g. scope_mySET == 1..12). The macros with the prefix "scope_" will be used by ProB and do not modify the B specification. If the size of the set is unspecified, ProB considers the set to have a default size. The value for the default size is defined in the Preferences|Animation Preferences... preference window by the preference Size of unspecified sets in SETS section.
The B method enables to specify the size of a set with the card operator in the PROPERTIES clause; this form of constraint is now supported by ProB, provided it is of a simple form card(S)=Nr, where S is a deferred set and Nr a natural number.
The typing information is used by ProB to enumerate the possible values of a constant or a variable whenever a specification does not narrow down that value to a single value.
For example, if you write xx:NAT & xx=1 ProB does not have to resort to enumeration as the xx=1 constraint imposes a single possible value for xx. However, if you write xx:NAT & xx<3 ProB will enumerate the possible values of xx in order to find those that satisfy the constraints imposed by the machine (here 0,1,2).
ProB will use the constraints to try to cut down the enumeration space, and will resort to enumeration usually only as a last resort. So something like xx:NAT & xx<10 & x>2 & x=5 will not result in enumeration.
The enumeration range for integers is controlled by two preferences in the Preferences|Animation Preferences... preference window: !MinInt, used for expressions such as xx::INT, and !MaxInt, used for expressions such as xx::NAT preferences. Nevertheless, writing xx: NAT & xx = 55 puts the value 55 in x no matter what !MaxInt is set to, as no enumeration is required.
Note that these preferences also apply to the mathematical integers (INTEGER) and natural numbers (NATURAL). In case a mathematical integer or natural number is enumerated (using !MinInt and !MaxInt) a warning is printed on the console.