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.

Keeping required behavior possible

Requirements that rule out unwanted behavior do not by themselves ensure that useful behavior remains possible. Even with marking, synthesis only needs to preserve the possibility of reaching some marked state. Add a reachability requirement when a particular capability must remain available and is not already ensured by marking. For example, a bridge may need to remain able to open for ships to pass, and able to close for road traffic to pass. Separate reachability requirements for the open and closed states ensure that neither capability can be lost merely because the other one suffices to reach a marked state. Other useful goals include returning a machine to its idle state after an operation or recovering to an operational state after a fault. These requirements keep paths to the goals available; they do not force the system to take those paths.

Use from when a capability is needed only in certain source states, and avoid or stay when the path to the goal must respect an additional restriction. For example, it may be necessary to keep an operational state reachable without passing through maintenance. A conditional requirement can be satisfied by removing all its source states from the controlled system. If those states must remain reachable as well, add a basic reachability requirement with the source predicate as its goal. For a bridge, @requirement:reachable(closed, from: open) keeps closing possible from the remaining open states, while an additional @requirement:reachable(open) ensures that opening itself remains possible. This requires some state satisfying the source predicate to remain reachable from every controlled state, rather than retaining every individual source state of the uncontrolled system.

Use bound when the number of model transitions needed to reach the goal matters. Choose the bound with the modeled operation and its possible starting states in mind: different states may need different numbers of transitions, and every state to which the requirement applies needs a permitted path within the bound. For example, some starting states may require preparatory actions before the operation itself can begin. Count those actions as well if they are separate transitions in the model. A bound limits the length of a path that must remain available; it does not impose a time deadline or require every execution to reach the goal within that many transitions. Changing the level of detail of the plant model may change the appropriate bound.

If no meaningful limit on the number of transitions is known, first model the requirement without a bound. When adding a bound, check that the resulting supervisor still permits the intended operations and source states: a smaller bound can remove behavior or lead to an empty supervisor. The data-based synthesis tool’s debug output can help explain the effect of a bound, but it is important to always interpret a reported minimum bound together with its stopping reason and the current controlled behavior. A fixed point reached before all source states are covered does not demonstrate that those source states can reach the goal within the reported minimum bound.

A bound can also be used for regression checking: a model update that unintentionally adds required steps may make the goal unreachable within the expected bound. Successful synthesis alone is not sufficient for this check, since synthesis may satisfy the bound by removing behavior or source states. As part of the regression check, you should therefore also verify that both the intended behavior and the intended source states remain reachable.

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