Invariant kinds

Similar to automata, different kinds of invariants are treated in different ways for supervisory controller synthesis. Invariants can be declared as plant, requirement, or supervisor invariants, by preceding or replacing the invariant keyword with a plant, requirement, or supervisor keyword respectively.

For instance, consider the following CIF specification:

invariant inv1: lamp.on or lamp.off;      // Regular/kindless invariant.

plant lamp:
  event turn_on, turn_off;

  requirement invariant req1: not off;    // Requirement invariant. Long form.
  requirement req2: not off;              // Requirement invariant. Short form.

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end

The inv1 invariant does not specify an additional supervisory kind keyword. It is therefore a regular invariant, also called a kindless invariant. The req1 invariant, in the lamp automaton, explicitly specifies a requirement kind and is therefore a requirement invariant. The req2 invariant is identical to the req1 invariant, except that the invariant keyword has been omitted. It is also a requirement invariant, but written in a shorter form.

There are two forms of invariants: state invariants and state/event exclusion invariants. Both forms can be used for synthesis. For instance, consider the following example of two counters:

plant def counter():
  controllable c_increment, c_decrement;
  disc int[0..10] count = 0;

  location:
    initial;
    marked;
    edge c_increment do count := count + 1;
    edge c_decrement do count := count - 1;
end

C1: counter();
C2: counter();

plant invariant C1.count + C2.count <= 15;
requirement C2.c_increment needs C1.count > 0;

Each counter can be incremented and decremented. The plant invariant specifies that the counts of both counters summed together can never exceed 15. The requirement invariant specifies that counter C2 may only be incremented if the count of C1 is non-zero. Note that data-based synthesis automatically ensures that all integer-typed variables are kept within range. Therefore, it is not strictly necessary to add requirements or guards to do so.