Version:
v10.0
[release notes]

# Module 4.2: Requirement automata and invariants

As already mentioned in the previous sub-module, requirements can be specified in different ways. The two main forms are requirement automata and requirement invariants. And requirement invariants also come in two different forms: state requirement invariants and state/event exclusion requirements. These three forms of requirements all restrict the allowed behavior of the system, either by indicating what must never be allowed to happen, or by specifying that only certain things are allowed to happen, meaning that all other things are disallowed. Restrictions are thus specified in a positive or negative way, but they are always restrictions nonetheless.

## Example

To explain the difference between the different forms of requirements, we will consider an example of bridge deck and traffic light, similar to the one from the first module. The bridge deck can be closed, partially open or fully open. The traffic light can be red or green. The plants of this system can be modeled as follows:

Together, these two components define the following state space for the uncontrolled system:

For safety reasons, we do not want the bridge deck to be partially or fully open while the light is green, as then cars could drive off the bridge into the water. This phrases the safety requirement negatively, by describing what is not allowed. This same requirement can also be phrased positively, in terms of what is allowed: the bridge deck may only be partially or fully open while the light is red. Alternatively, we could say that the bridge must be closed when the light is green.

Next, we will model this requirement in each of the three different forms.

## Requirement automata

Requirements can be specified as requirement automata, similar to how plant automata can be specified. In fact, there is no difference in what can be modeled for plant and requirement automata, except that they are either indicated as being a plant or a requirement. Requirement automata thus have location and edges, and they can also have variables, guards, and updates. And it is possible to make requirement automaton definitions and instantiate them multiple times.

The purposes of plant and requirement automata are different. A plant automaton specifies what the system can do, while a requirement automaton specifies what it is allowed to do. As with all automata, they synchronize on shared events. This way, a requirement automaton may restrict the behavior of the system. That is, if a certain event in the alphabet of a requirement automaton is not possible in one of the locations of the requirement automaton, while it is allowed in the plant, then the requirement automaton imposes a restriction.

One way to make a requirement automaton is to take one or more plant automata, compute their state space, and remove some behavior from it. If we do that for the bridge deck and traffic light example above, we could make the following requirement automaton:

This is a copy of the combined state space of the bridge deck and traffic light plant components, with some behavior removed from it. The two states that are unsafe have been removed, as have all transitions to these states. What remains is the allowed behavior, described as a requirement automaton. Certain behavior is restricted. For instance, when the bridge deck is open and the traffic light is red, the traffic light is not allowed to be turned to green. Putting this requirement together with the plant, it restricts the behavior of the plant, ensuring that the controlled system can never get to the unsafe states.

## State requirement invariants

Requirements can be also be specified by state requirement invariants, which are also called state invariant requirements or requirement state invariants. This form of requirements allows you to specify a condition, in the form of a predicate, that must hold in all states of the controlled system. Any state that does not adhere to this condition is deemed a bad state, and synthesis will ensure it can never be reached.

For instance, for the bridge deck and traffic light example, we could specify a state requirement invariants, with the following condition:

1. `not ((BridgeDeck.PartiallyOpen or BridgeDeck.Open) and TrafficLight.Green)`

This specifies that it must not be the case, that the bridge deck is partially open or fully open and at the same the traffic light is green. This is phrased negatively. We could also phrase it positively:

2. `(BridgeDeck.Closed and TrafficLight.Green) or TrafficLight.Red`

This specifies that it must always be the case that, either the bridge deck is closed and the traffic light is green, or the traffic light is red. It does not indicate what the bridge deck must be when the traffic light is red, and thus it may have any state that is possible in the plant. That is, if the traffic light is red, the bridge deck may be closed, partially open or fully open.

The two requirements have the same effect, but are phrased differently. In this case, the negative phrasing more directly indicates the bad states, while the positive phrasing prevents the use of the negation (`not`). The choice of how to write a requirement invariant depends on the modeler's preference. But, in general, you should opt for what is the most direct, simple and readable.

## State/event exclusion requirement invariants

The third and final form of requirements is state/event exclusion requirement invariants, which are also called state/event exclusion invariant requirements or requirement state/event exclusion invariants. This form of requirements allow you to specify a condition, in the form of a predicate, that must hold for an event to be enabled or disabled in certain states. If the condition is for disabling an event, synthesis will ensure the event is disabled in all states where the predicate holds. If the condition is for enabling an event, synthesis will ensure the event is disabled in all states where the predicate doesn't hold, such that it is only enabled in states where the predicate holds.

For instance, for the bridge deck and traffic light example, we could specify the following state/event exclusion requirement invariants to disable certain events in certain states:

3. `BridgeDeck.Closed and TrafficLight.Green disables partially_opened`
4. `BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green`

The first requirement disables the `partially_opened` event in the state where the bridge deck is closed and the traffic light is green. This prevents transitioning from the `Closed/Green` state to the `PartiallyOpen/Green` state. Similarly, the second requirement disables the `to_green` event in states where the bridge deck is partially open or fully open. It prevents transitioning from the `PartiallyOpen/Red` state to the `PartiallyOpen/Green` state, and from the `Open/Red` state to the `Open/Green` state.

The requirements above restrict only the direct transitions to bad states. Synthesis will prevent reaching those bad states, and thus any transitions from the bad states are also not possible. We may exploit this in phrasing requirements, which can help to make requirements simpler. For instance, the above two requirements could also be written as:

5. `TrafficLight.Green disables partially_opened`
6. `BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green`

The first requirement is changed, by dropping the `BridgeDeck.Closed` part of the condition. It is fine to also disable the `partially_opened` event in the `Open/Green` state, as that is a bad state.

Besides that, predicates can often be written in different way by making use of the fact that only a limited number of locations are present in automata. The bridge deck being partially open or fully open is therefore the same as it not being closed. We may thus also write the above two requirements as:

7. `not TrafficLight.Red disables partially_opened`
8. `not BridgeDeck.Closed disables to_green`

Which of these forms is better, depends on the modeler's preference, and what is simpler and more readable.

Besides these different ways of writing the requirements in a negative form, indicating when the events are disabled, they can also be specified positively, indicating when the events are enabled/allowed:

9. `partially_opened needs TrafficLight.Red`
10. `to_green needs BridgeDeck.Closed`

This indicates that for the bridge deck to be partially opened, the traffic light needs to be red. If it is green, this event is thus not allowed. Similarly, for the traffic light to be turned to green, the bridge deck needs to be closed. If the bridge deck is partially or fully open, the light may thus not be turned to green.

As with state requirement invariants, which form to use, positive or negative, depends on preference and readability. A positively stated state/event exclusion requirement invariants `e needs p` (like 9 and 10 above) can always be phrased negatively as `not p disables e` (like 7 and 8 above), and vice versa.

## Choosing the best requirement form

For the example above, the requirement automaton is arguably the least suited form. It requires modeling a full automaton, with four locations and even more edges. Also, it indicates what is allowed, which means you mentally have to check what is disabled, and thus what is expressed as a requirement.

The invariants are more succinct. The different forms of requirement invariants (1, 2, 3+4, 5+6, 7+8, or 9+10) have their pros and cons as well. Variants 9+10 are the shortest, but require a mental step to invert the conditions to see what is disabled. Variants 7+8 use double negations (`not` and `disables`) and are thus best avoided. Variants 5+6 directly indicate what is disabled, and are not much longer than 9+10, and are thus a good choice. Variants 3+4 are needlessly longer than 5+6 and are thus best avoid as well.

Variant 2 also requires mentally inverting the condition to see what states are being forbidden. Variant 1 is in that sense the better option, even though it uses a negation.

In the end, it is up to you to decide which form you think is the most intuitive. But, variant 1 and variants 5+6 could be seen as the best options for this particular example.

## Requirement automata to specify order

In the previous example of a bridge deck and traffic light, the requirement automaton was not the best option. Let us now consider another example, of a railway crossing, where a requirement automaton could be a good option. A red light can be on, signaling that a train is coming, and is off otherwise. A barrier is closed if a train approaches, such that road traffic can't cross the tracks. Once the train has passed, the barrier opens again. The plant of this railway crossing can be modeled as follows:

The light is initially Off, but can be turned on. If it is On, it can be turned off again. And so on. The barrier is initially Open. It can be closed, opened, closed, opened, and so on.

Together, these two components have the following state space:

To prevents potential collisions of road traffic with trains, some of this behavior is to be prevented. That is, for safety reasons, we want the light to be turned on, before the barrier is opened. Then, only once the light is turned off again, should the barrier be opened again.

We could model this using the following requirement:

This is a simple requirement, that indicates the order in which the four controllable events are allowed to happen. State requirement invariants are not applicable here, as we do not wish to restrict the states of the plant, but only the transitions. State/event exclusion requirement invariants are an alternative, but it would require four of them, one per event. The requirement automaton could be seen as the best option here, as it most intuitively and directly specifies the allowed order of events.

Do note, that this particular example may be too restrictive in practice. It for instance does not allow turning off the light if it was turned on by mistake, at least not without first closing the barrier.

## Quiz

[ { type: 'multiple-choice', question: "Which of the following should be requirements, rather than being part of the plant?", answers: [ "An automaton that describes the behavior of a button.", "An automaton that describes that a motor should not be unnecessarily turned on and off.", "An automaton that describes how a product must be checked after it has been processed.", "An automaton that describes how products can enter the system.", "An automaton that describes that a gate must be open for a car to go through it.", "An automaton that describes the behavior of a motor.", ], correctAnswer: '2, 3, 5' }, { type: 'single-choice', question: "Is the alphabet of a requirement automaton always the same as the plant alphabet?", answers: [ "Yes.", "No.", ], correctAnswer: '2' }, { type: 'single-choice', question: ` Consider a `Button` that can be `Pushed` or `Released` and a `Lamp` that can be `On` or `Off`. The lamp can be turned on or off by the events `turn_on` and `turn_off`, respectively. Which of the following requirements impose the same restriction as requirement `Button.Pushed disables turn_off`? `, answers: [ "`Button.Pushed disables turn_on`", "`Button.Released disables turn_off`", "`Button.Released disables turn_on`", "`not Button.Pushed disables turn_off`", "`not Button.Pushed disables turn_on`", "`not Button.Released disables turn_off`", "`not Button.Released disables turn_on`", "None of the above." ], correctAnswer: '6' }, { type: 'multiple-choice', question: ` Consider again the same system as the previous question. Which of the following requirements impose the same restriction as requirement `Button.Pushed disables turn_off`? `, answers: [ "`turn_off needs Button.Pushed`", "`turn_on needs Button.Pushed`", "`turn_off needs Button.Released`", "`turn_on needs Button.Released`" ], correctAnswer: '3' }, { type: 'multiple-choice', question: ` Consider again the same system as the previous question. Which of the following requirements impose the same restriction as requirement `Button.Pushed disables turn_off`? `, answers: [ "`turn_off needs not Button.Pushed`", "`turn_on needs not Button.Pushed`", "`turn_off needs not Button.Released`", "`turn_on needs not Button.Released`" ], correctAnswer: '1' } ]