## 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 supported type:

  - Boolean type.

  - Ranged integer type (e.g. `int[0..5]`). Ranges that allow more than 2,147,483,647 (2^31 - 1) possible values are not supported.

  - Enumeration type.

  - Tuple type, with supported types for the tuple’s fields.

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

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

- Annotations are ignored, except for reachability requirement annotations.

The following restrictions apply to user-defined functions:

- External user-defined functions are not supported.

- Internal user-defined functions with recursive calls are not supported.

- Internal user-defined functions with `while` statements are not supported.

- Internal user-defined functions with assignments that may result in runtime out-of-range errors are not supported.

- Internal user-defined functions may only be used in function calls. All other uses are not supported, including using them as data, such as storing them in variables, returning them from functions, and so on.

- Internal user-defined functions may only use supported data types (same as discrete and input variables) as their return and parameter types, and as the types of their local variables.

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, on two supported integer or enumeration expressions, or on two supported tuple expressions.

- The binary inequality comparison (`!=`) on two supported predicates, on two supported integer or enumeration expressions, or on two supported tuple 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.

- Function calls to internal user-defined functions with supported arguments that return a boolean value.

- Projections on tuples that result in a boolean value.

- Received values (`?`) with a boolean type.

- 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` and `-i` for `i` a supported integer expression.

- `i + j`, `i - j`, and `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.

- `abs(i)` and `sign(i)` for `i` a supported integer expression.

- `max(i, j)` and `min(i, j)` for `i` and `j` supported integer expressions.

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

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

- Function calls to internal user-defined functions with supported arguments that return an integer or enumeration value.

- Projections on tuples that result in an integer or enumeration value.

- Received values (`?`) with an integer or enumeration type.

- 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 tuple expressions (for binary comparisons, initial values of variables, right hand sides of assignments, etc) are supported. The supported expressions are:

- A tuple literal/value.

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

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

- Tuple-typed constants (`x`, for `x` a constant with a tuple type).

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

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

- Function calls to internal user-defined functions with supported arguments that return a tuple value.

- Projections on tuples that result in a tuple value.

- Received values (`?`) with a tuple type.

- Any other valid CIF expression (computation) that results in a tuple 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.

### 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 with merge' variant) to the edges. Predicates are represented internally using Binary Decision Diagrams (BDDs).

### Supported requirements

Four types of requirements are supported: state invariants, state/event exclusion invariants, requirement automata and reachability requirements. 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

Reachability requirements can be used to specify liveness conditions, in addition to marker predicates.

Besides the explicit requirements, synthesis also prevents runtime errors. This includes enforcing that integer (parts of) 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 (parts of) variables being assigned values outside their domain (integer value range) occur.