Deferred Sets
A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.
MACHINE M0
SETS AA; BB={bb,cc,dd}
END
ProB in general requires all deferred sets to be given a finite cardinality before starting animation or model checking. If no cardinality is specified, a default size will be used (which is controlled by the DEFAULT_SETSIZE preference).
In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by
- making it an enumerated set, i.e., adding AA = {v1,v2,…} to the SETS clause
- adding a predicate card(AA) = constant to the PROPERTIES clause
- Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:
- card(AA) > 1
- aa:AA & bb:AA & aa/=bb
- AA = {aa,bb} & aa/=bb
- …
- you can add a DEFINITION scope_AA == constant to instruct ProB to set the cardinality of AA to the constant.
Using Refinement for Animation Preferences
Note: instead of adding AA = {aa,bb} to the SETS clause you can also add AA = {aa,bb} & aa/=bb to the PROPERTIES clause. This can also be done in a refinement. A good idea is then to generate a refinement for animation with ProB (which may contain other important settings for animation):
REFINEMENT M0_ProB REFINES M0
CONSTANTS aa,bb
PROPERTIES
AA = {aa,bb} & aa/=bb
END
Setting Deferred Set Cardinalities within probcli
From the command-line, using probcli you can use the command-line switch:
-card <GS> <VAL>
Example:
probcli my.mch -card PID 5