Modeling the requirements

After modeling the plant and plant relations, the requirements should be modeled as well.

The hardest thing about modeling the requirements, 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.

Event-based requirements are modeled as requirement automata. The simplest event-based requirements have only two locations, and form a loop of only two edges. Here is a typical example requirement that controls the plants from the section on modeling the plant. It ensures that the lamp is on while the button is pushed, and off while it is released:

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;
end

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 using state/event exclusion requirements as follows:

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

Having requirements block uncontrollable events can easily lead to unnecessarily restricting too much of the system behavior. As mentioned in the section on modeling plant relations, correctly modeling such relations makes this easier.

Generally, it is better to as much as possible use requirements that are pure restrictions. That is, use state-based requirements (mutual state exclusion and state/event exclusion requirements) instead of event-based requirements (requirement automata), where applicable. Requirement automata may introduce additional state, which can lead to reduced performance. Using pure restriction requirements you are also less likely to unnecessarily restrict too much of the system behavior.

The CIF language tutorial has lessons on using variables, guards and updates.

The next step in the process to apply synthesis-based engineering in practice is to deal with marking.