Type declarations

Each component (natural, role or compartment) in an RBL model has a component type. This allows us to instantiate multiple components of the same type and to specify constraints on the level of types (see system instantiation).

Natural types

The simplest type is the natural type, which only has a name:

natural type Worker;

The keyword natural is optional, but can be added to clearly state that instances of this type are meant to be role players. In case the type is only needed for technical reasons, e.g., to define a counter, omitting the natural keyword is more appropriate.

Role types

A role type is declared similarly. However, a role type declaration must also specify the possible player types. Note that players are not necessarily only naturals, but other roles and compartments are allowed as well. In the following example, the role type Consumer is defined. Instances of this role type can be played by components of type Worker.

role type Consumer(Worker);

Compartment types

A compartment type declaration must include a list of role types that comprise the compartment:

compartment type ConsumerProducerProtocol(Producer, Consumer);

This type declaration states that an instance of ConsumerProducerProtocol must contain exactly one role instance of type Producer and one role instance of type Consumer.

It is also possible to define alternatives for the set of roles in a compartment. The following declaration specifies that either a Producer or a Consumer, or both must be contained in the compartment:

compartment type ConsumerProducerProtocol(Producer | Consumer | Producer, Consumer);

Furthermore, lower and upper bounds on the occurrence of roles can be specified:

compartment type ConsumerProducerProtocol(Producer, Consumer[1..3]);

Here, the compartment must contain at least one and at most three instances with role type Consumer. If lower and upper bounds are identical, the shorthand notation Consumer[3] can be used.

Type set definitions

If a certain set of component types is often used together, e.g., in function parameter types or in quantification over components, it can be useful to define an alias for the set of types. For instance, if there are component types SlowWorker and FastWorker, a type name comprising both of them can be defined as follows:

typedef Worker = { SlowWorker, FastWorker };

Then, this type can be used, e.g., in a forall quantifier:

forall w : Worker. w.work = 0