//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

indexterm:[invariant,supervisory kind]
indexterm:[invariant,regular]
indexterm:[invariant,kindless]
indexterm:[invariant,plant]
indexterm:[invariant,requirement]
indexterm:[invariant,supervisor]

:leveloffset: -2

[[lang-tut-synthesis-invkind]]
== Invariant kinds

<<lang-tut-synthesis-autkind,Similar to automata>>, different kinds of invariants are treated in different ways for <<lang-tut-synthesis-intro,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:

[source, cif]
----
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:
<<lang-tut-data-chapter-stat-invariants,state invariants>> and <<lang-tut-data-chapter-stat-evt-excl-invariants,state/event exclusion invariants>>.
Both forms can be used for synthesis.
For instance, consider the following example of two counters:

[source, cif]
----
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 <<tools-chapter-datasynth,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.
