Specification phase

The first phase is the specification phase. During this phase, untimed plants and requirements are created, from which a supervisor is synthesized during the next phase, the supervisor synthesis phase.

Getting started

Make sure you installed the tooling, and made the 4K420 course files available (if applicable). If you already previously installed the tooling, make sure to update it. Also update the 4K420 course files, if you previously made them available in your workspace (if applicable).

You can either start from scratch, or work on designing a controller for one of the four workstations from the 4K420 course files.

To start from scratch, first start Eclipse. In Eclipse, create a project. In that project, you can optionally create some directories. Then you need to create a CIF file. For information on how to name the CIF file, see the Naming conventions section below.

Alternatively, you can also use the 4K420 course files, to work on the exercises, to work on your assignment for the 4K420 course, or just to play with them as examples. First obtain the course files, or update them, if you already previously obtained them. Then, you can directly create a CIF file. For information on how to name the CIF file, see the Naming conventions section below.

Naming conventions

While you are free to choose a name for you CIF file, you may want to follow the naming conventions. If you follow the naming conventions, name the CIF file that contains your plants and requirements #_plants_reqs1.cif, where # should be replaced by the name of your system.

If you use multiple plants/requirements files, name them #_plants_reqs1.eventbased.cif or #_plants_reqs1.databased.cif, #_plants_reqs2.eventbased.cif or #_plants_reqs2.databased.cif, #_plants_reqs3.eventbased.cif or #_plants_reqs3.databased.cif, etc. The scripts provided by the 4K420 course files allow up to five plants/requirements files. The numbers may not be that indicative of their content, but they allow arbitrary division of the system into parts, without having to modify the scripts.

For each plants/requirements file, you can choose whether to apply event-based synthesis or data-based synthesis by using the .eventbased.cif or .databased.cif file extension, respectively. For instance, for the first plants/requirements file, use either #_plants_reqs1.eventbased.cif or #_plants_reqs1.databased.cif. You must choose one or the other, you can’t have both a #_plants_reqs1.eventbased.cif and a #_plants_reqs1.databased.cif file. You can always rename the file later on, to change the synthesis algorithm that is applied.

Modeling the plants/requirements

In the plants/requirements file, you should model some plants and requirements in CIF 3 syntax. The plants specify the physical behavior of the (hardware) system. The requirements each limit a part of the system’s behavior. Together the requirements make sure that only the desired behavior is allowed.

To get started with modeling the plants and requirements for the first time, take a look at the first exercise, which guides you through the modeling of some plants and requirements, and explains the syntax that is used.

For the four workstations used in the 4K420 course, the event names are specified in the workstations documentation. Use the specified event names to avoid problems in using the scripts and coupling the synthesized supervisor to the actual hardware setup. The workstation pages also indicate the initial states of all their actuators and sensors.

Modeling the plants

Typically, for low-level controllers as developed during the 4K420 course, you should start with a plant automaton per sensor and actuator. For digital sensors and actuators, which are by far the most common, you should model the automata with two locations, one where the sensor or actuator is off, and one where it is on. Which location should be the initial location depends on the specific sensor or actuator. Digital sensors can go on and off, and as such have two associated uncontrollable events. Similarly, digital actuators can be turned on or off as well, and also have two associated controllable events.

Here are some examples of typical plants:

plant Button:
  uncontrollable u_pushed, u_released;

  location Released:
    initial; marked;
    edge u_pushed goto Pushed;

  location Pushed:
    edge u_released goto Released;

plant Lamp:
  controllable c_on, c_off;

  location Off:
    initial; marked;
    edge c_on goto On;

  location On:
    edge c_off goto Off;

Once you have the plants for the individual sensors and actuators, you can think about the relations between them. These relations should be physical relations, representing behavior present in the actual uncontrolled system. For instance, if a movement has two limit sensors, most likely they physically can’t both be on at the same time. The individual plants of the two digital sensors however, can both be in their ‘On’ state, as they are not in any way related.

In such a case, if plants are physically related, you may combine them to a single plant. Usually, this involves only two plants. In some very rare cases, it may be needed to combine three or more plants together into a single new plant. To merge some plants, manually compute/model the product of the plants, and remove the original plant automata. Then, to express the relationship, remove the behavior that is not physically possible.

An alternative physical relationship, is the relation between sensors and actuators. In such cases, the relationship with the sensor(s) can usually be added to the actuator plant(s).

By correctly incorporating all the physical restrictions present in the actual system, the tools can use this knowledge during synthesis. Essentially, by modeling the physical relations/restrictions, the uncontrollable events are enabled in much less (combinations of) locations of the plants. This means that the requirements are much less likely to block uncontrollable events.

In other words, the modeled relationships of the plants restrict the behavior of the plant automata. However, these restrictions are also present in the physical system. Hence, without modeling such relationships, the plant model has more behavior than the physical system. Once the plant relations are correctly modeled, you may assume this relationship in the requirements, meaning you may assume that certain uncontrollable events can physically not occur in certain locations. The tools will then have enough knowledge of the system to come to the same conclusions.

For instance, assume a certain sensor signal can only occur when the corresponding actuator is enabled. Modeling this relation ensures that ‘blocking’ such sensor signals in the requirements, when the actuator is off, is no longer ‘illegal’ behavior.

To practice modeling plants for a low-level controller, see the third exercise.

Modeling the requirements

The hardest thing about requirement automata, is that you have to think in restrictions, rather than in use cases. So, rather than ‘first do this, then do that, then do that or that other thing, etc’, you should think ‘this or that is only allowed if/after this or that other thing’.

Requirements should be as small and orthogonal as possible. The simplest event-based requirements, which are rather common when using event-based modeling, have only two locations, and form a loop of only two edges. Here is a typical example requirement that controls the plants from the previous section.

requirement LampOnWhileButtonPushed:
  location Released:
    initial; marked;
    edge Button.u_pushed goto Pushed;
    edge Lamp.c_off;

  location Pushed:
    edge Button.u_released goto Released;
    edge Lamp.c_on;

Event-based requirements can be used for both event-based and data-based synthesis. However, for data-based synthesis we can also model the requirements in a more state-based manner (referring to locations of automata) or data-based manner (referring to locations of automata, as well as using variables, guards, updates, and invariants), which is often shorter and simpler. The requirement above can be modeled in a state-based manner as follows:

// Lamp on only while button is pushed.
requirement Lamp1.c_off needs Button1.Released;
requirement Lamp1.c_on  needs Button1.Pushed;

The requirement is taken from the first exercise, where it is explained in more detail.

Requirements must never block uncontrollable events. As mentioned in the previous section, correctly modeling the plant relations makes this easier.


Every automaton, whether plant or requirement, must have at least one marked location. A marked location is a location that indicates a safe, stable, or resting state. In practice however, especially for the 4K420 course, the entire system can potentially be brought back to the initial state. As such, it is usually enough to make the initial locations marked.

An exception is automata that have some kind of initialization behavior/sequence. For such automata, make the first location that is part of the loop after the initialization sequence, a marked location. The locations from the initialization sequence can no longer be reached after initialization is finished. The first location after that initialization sequence is part of the ‘normal’ behavior and can be seen as the initial location of the behavior after initialization.

Incremental development

When developing a controller, it is often best to start with just a small part of the system. You first develop a controller for that small part, test it, and make sure it works properly. Then, you extend the controller to work for a larger part of the system, and you keep repeating this until the controller controls the entire system. That is, you go through the entire toolchain each time, increasing the part of the system covered by the plants and requirements for each iteration.

This incremental development approach makes it easier to figure out why your controller doesn’t behave as expected, or why it can’t be synthesized. More information on this is provided during the next phase.

Typically, for low-level controllers as developed during the 4K420 course, you should start with no more than a few sensors and actuators, with their corresponding events.

Using multiple plants/requirements files

For larger systems, monolithic supervisor synthesis becomes infeasible, as the resulting supervisor becomes very large. One solution is to split the system into several parts, and develop supervisory controllers for each of the parts. The toolchain for synthesis of multiple supervisors is explained in details during the next phase.

The CIF merger tool is used during that phase to merge the supervisors for the different parts into a single supervisor file. The tool puts the supervisors in parallel, and avoids having to compute the full product. That is, the tool puts the supervisor automata together in a single file, and does not expand the full state space. For more information, see the documentation of the CIF merger tool.

See the section on Naming conventions above, for information on how to name the plants/requirements files when using multiple such files.

When splitting the system into parts, strongly related components should be kept together. That is, create plants/requirements per sub-system. Under no circumstance should multiple controllers control the same controllable events, and thus the same actuator. In fact, only sensors should be shared between the different controllers. This ensures that the supervisors don’t conflict with each other, and together apply the same restrictions as would the monolithic supervisor.

Adding a plant with only two locations doubles the uncontrolled state space. As such, adding lamps or other visual feedback elements from a user interface, to indicate to the user that something interesting has occurred, quickly becomes expensive. In such cases, separating the ‘normal’ behavior from the user interface part of the system, can greatly reduce the size of the supervisors.

Another common division is if the system has naturally loosely coupled parts. For instance, if one part of the system processes a product and provides it to the second part of the system, a single sensor between them may be enough for the second part of the system to detect the product. In such cases, the first and second part could be modeled in separate plants/requirements files, only sharing a single plant automaton for the common sensor.

Splitting plants and requirements into multiple plants/requirements files can be practiced with the fourth exercise.