## 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.