Deferred Sets: Difference between revisions

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

See manual page for probcli.