Specifications supported by data-based synthesis

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

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:

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:

Only limited forms of assignments are supported:

What exactly is supported for assignments, expressions and predicates can be subtle:

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:

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.