• Special Pages
• User

Help

# 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
```