## Specifications supported by data-based synthesis

The data-based supervisory controller synthesis tool supports a subset of CIF specifications. The following restrictions apply:

- Only `plant` and `requirement` automata are supported. Automata with a `supervisor` kind, as well as kindless/regular automata (without a supervisory kind) are not supported.

- Specifications without plant automata are not supported.

- Events not declared as controllable or uncontrollable are not supported. This includes the `tau` event, both explicitly used on edges, as well as implicitly for edges without explicitly mentioned events.

- The use of channels (events with data types) in requirements is not supported. That is, requirements that send or receive (with or without data) are not supported.

- Only `plant` and `requirement` invariants are supported. Invariants with a `supervisor` kind, as well as kindless/regular invariants (without a supervisory kind) are not supported.

- Continuous variables are not supported.

- Discrete and input variables are supported, but only if they have a boolean type, ranged integer type (e.g. `int[0..5]`), or enumeration type. For integer types, ranges that include negative integer values are not supported, and neither are ranges that include value 2,147,483,647.

- Discrete variables must have supported initial values. If explicit initial values are given, they must be supported predicates (for boolean variables) or supported expressions as described below (for all other variables).

- Constants, algebraic variables and algebraic parameters of components are supported as long as their values are supported in the context where they are used (as described below).

- Automata with non-determinism for controllable events are not supported. That is, automata that have locations with multiple outgoing edges for the same controllable event, with overlapping guards (e.g. `x > 1` and `x < 4`), are not supported. Note that this check is performed on the linearized guards, and may therefore lead to false positives, as the check is an over-approximation and guard overlap may be detected for unreachable states.

- Conditional updates (`if` updates), multi-assignments, and partial variable assignments are not supported.

- I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.

- Annotations are ignored.

Only limited forms of predicates (for markers, invariants, initialization, guards, initial values of boolean variables, right hand sides of assignments, etc) are supported. The supported predicates are:

- Boolean literals (`true`, `false`).

- Discrete and input boolean variables (`x`, for `x` a discrete or input variable with a boolean type).

- Algebraic boolean variables with supported predicates as their values (`x`, for `x` an algebraic variable with a boolean type).

- Boolean constants (`x`, for `x` a constant with a boolean type).

- Locations (`aut.loc`, for `aut` and automaton and `loc` a location of that automaton).

- The unary inverse operator (`not`) on a supported predicate.

- The binary logical conjunction (`and`) on two supported predicates.

- The binary logical disjunction (`or`) on two supported predicates.

- The binary logical implication (`=>`) on two supported predicates.

- The binary logical bi-conditional (`<=>`) on two supported predicates.

- The binary equality comparison (`=`) on two supported predicates, or on two supported integer or enumeration expressions.

- The binary inequality comparison (`!=`) on two supported predicates, or on two supported integer or enumeration expressions.

- The binary less than comparison (`<`) on two supported integer expressions.

- The binary less than or equal comparison (`<=`) on two supported integer expressions.

- The binary greater than comparison (`>`) on two supported integer expressions.

- The binary greater than or equal comparison (`>=`) on two supported integer expressions.

- Conditional expressions (`if` expressions) with supported guard and resulting value predicates.

- `Switch` expressions with supported control value and resulting value predicates.

- Any other valid CIF predicate (computation) that results in a boolean value, as long as the computation is not too complex to be performed statically. That is, the computation must essentially represent a fixed/constant value.

  Here are some examples of computations that can be statically evaluated:

  - `{1} in {1, 2}` (result is `true`)

  - `[false, true][0]` (result is `false`)

  - `c - 1`, for a constant `c` with value `4` (result is `3`)

  Here are some examples of computations that can not be statically evaluated:

  - `v = true` for `v` a discrete variable. The computation results in different values for different values of `v`.

  - `{v} in {1, 2}` for `v` a discrete variable. The computation results in different values for different values of `v`.

Only limited forms of integer and enumeration expressions (for binary comparisons, initial values of variables, right hand sides of assignments, etc) are supported. The supported expressions are:

- An integer literal/value.

- An enumeration literal/value.

- Discrete and input integer/enumeration variables (`x`, for `x` a discrete or input variable with an integer or enumeration type).

- Algebraic integer/enumeration variables with supported expressions as their values (`x`, for `x` an algebraic variable with an integer or enumeration type).

- Integer/enumeration constants (`x`, for `x` a constant with an integer or enumeration type).

- `+i` for `i` a supported integer expression.

- `-i` for `i` a supported integer expression.

- `i + j` for `i` and `j` supported integer expressions.

- `i - j` for `i` and `j` supported integer expressions.

- `i div j` and `i mod j` for `i` a supported integer expressions, and `j` a positive integer value, or a computation that results in a positive integer value, as long as the computation is not too complex to be performed statically. That is, `j` must essentially be constant.

- Conditional expressions (`if` expressions) with supported guard predicates and supported resulting values.

- `Switch` expressions with supported control values and supported resulting values.

- Any other valid CIF expression (computation) that results in an integer value or an enumeration value, as long as the computation is not too complex to be performed statically. That is, the computation must essentially represent a fixed/constant value.

  Here are some examples of computations that can be statically evaluated:

  - `2 * 5` (result is `10`)

  - `floor(3.14)` (result is `3`)

  - `c + 1`, for a constant `c` with value `2` (result is `3`)

  Here are some examples of computations that can not be statically evaluated:

  - `v - 1`, for `v` a discrete variable. The computation results in different values for different values of `v`.

  - `ceil(sqrt(-1.0))`, since `sqrt` of a negative number results in a runtime error upon evaluation.

Only limited forms of assignments are supported. The supported forms are:

- `xb := p` (with `xb` a boolean variable, and `p` a supported predicate, as described above)

- `xi := ie` (with `xi` a supported integer variable, and `ie` a supported integer expression, as described above)

- `xe := ee` (with `xi` an enumeration variable, and `ee` a supported enumeration expression, as described above)

### Preprocessing

The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be synthesized:

- Remove I/O declarations

- Eliminate component definition/instantiation

Additionally, the CIF specification is converted to an internal representation on which the synthesis is performed. This conversion also applies linearization (product variant) to the edges. Predicates are represented internally using Binary Decision Diagrams (BDDs).

### Supported requirements

Three types of requirements are supported: state invariants, state/event exclusion invariants, and requirement automata. For state invariants and state/event exclusion invariants, both named and nameless variants are supported.

State invariants are global conditions over the values of variables (and locations of automata) that must always hold. Such requirements are sometimes also called mutual state exclusions. Here are some examples:

    requirement invariant x != 0 and not p.b;
    requirement invariant x > 5;
    requirement R1: invariant not(x = 1 and y = 1) or q.x = a;

    requirement (x = 1 and y = 1) or (x = 2 and y = 2);
    requirement (3 <= x and x < = 5) or (2 <= y and y <= 7);
    requirement x = 1 => y > 2;

State/event exclusion invariants or simply state/event exclusions are additional conditions under which transitions may take place for certain events. Here are some examples:

    requirement invariant buffer.c_add    needs buffer.count < 5;
    requirement invariant buffer.c_remove needs buffer.count > 0;
    requirement invariant button.on = 1 disables lamp.c_turn_on;
    requirement invariant R3: buffer.c_remove needs buffer.count > 0;

    requirement {lamp.c_turn_on, motor.c_turn_on} needs button.Off;
    requirement p.x = 3 and p.y > 7 disables p.u_something;

Requirement automata are simply automata marked as `requirement`. They usually introduce additional state by using multiple locations or a variable. The additional state is used to be able to express the requirement. One common example is a counter. For instance, consider the following requirement, which prevents more than three products being added to a buffer:

    requirement automaton counter:
      disc int[0..5] count = 0;

      requirement invariant count <= 3;

      location:
        initial;
        marked;

        edge buffer.c_add do count := count + 1;
    end

Another common example is a requirement that introduces ordering. For instance, consider the following requirement, which states that `motor1` must always be turned on before `motor2` is turned on, and they must always be turned off in the opposite order:

    requirement automaton order:
      location on1:
        initial;
        marked;
        edge motor1.c_on goto on2;

      location on2:
        edge motor2.c_on goto off2;

      location off2:
        edge motor2.c_off goto off1;

      location off1:
        edge motor1.c_off goto on1;
    end

Besides the explicit requirements, synthesis also prevents runtime errors. This includes enforcing that integer variables stay within their range of allowed values. This is essentially an implicit requirement. For instance, for a CIF specification with a variable `x` of type `int[0..5]` and a variable `y` of type `int[1..3]`, requirement invariant `0 <= x and x <= 5 and 1 <= y and y <= 3` is implicitly added and enforced by the synthesis algorithm. In the resulting controlled system, no runtime errors due to variables being assigned values outside their domain (integer value range) occur.