Eliminate state invariants

This CIF to CIF transformation eliminates state invariants. It replaces them with extra guards on edges of automata, and with extra initialization predicates in components.

Note that eliminating state invariants using this transformation is not the same as performing supervisory controller synthesis. It is not recommended to eliminate requirement state invariants using this transformation.

This transformation comes in multiple variants:

Eliminate state invariants (elim-state-invs)

  • Eliminates all state invariants from the specification.

Eliminate plant state invariants (elim-plant-state-invs)

  • Eliminates only the plant state invariants from the specification.

Eliminate supervisor state invariants (elim-supervisor-state-invs)

  • Eliminates only the supervisor state invariants from the specification.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

  • Component definitions and component instantiations are not supported.

  • SVG input mappings with updates are not supported.

  • Multi-assignments are not supported, e.g. (x, y) := (y, x) is not supported. Multiple assignments on an edge are supported.

  • Partial-variable assignments are not supported.

  • Time-dependent state invariants are not supported.

  • State invariants that directly or indirectly depend on the values of input variables are not supported.

  • State invariants that directly or indirectly contain an automaton ('self') reference are not supported.

Preprocessing

No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):

Implementation details

Depending on the variant of the transformation that is used, all invariants or only some of them are eliminated.

For each invariant that is eliminated, an extra initialization predicate and extra guards may be added to the specification. The state invariant itself is removed from the specification. If a removed state invariant has a name, it is lost.

Invariants in locations are adapted first, before they are eliminated. If the invariant is in a location of an automaton with two or more locations, its predicate is made conditional on being in the location. For instance, for a state invariant invariant x < 3 in a location loc, the state invariant becomes invariant loc => (x < 3). Regardless of the number of locations of the automaton, the state invariant is moved out of the location, and into the automaton.

For each state invariant, the predicate of the state invariant is added as an initialization predicate to the component where the state invariant is located. In order to not unnecessarily add initialization predicates to components, some steps are taken to simplify the added initialization predicate. The initial values of discrete variables and continuous variables are filled in, if it can be statically determined what their single initial value is. Similarly, a location reference is replaced by true or false as appropriate, if it can be statically determined which location is the single initial location of its automaton. If discrete variables, continuous variable, or locations are referred to via algebraic variables or derivatives of continuous variables, these algebraic variables and derivatives are inlined before the initial values are filled in. If the predicate, after filling in initial values of state objects, is trivially true (as can be statically determined), then no initialization predicate is added to the component. In all other cases, the predicate is simplified as much as possible before it is added to the component.

For each state invariant, a single extra guard is added to each edge of each automaton. The added guard consists of the state invariant’s predicate, where each updated variable is replaced by its new value expressions, according to the updates of the edge. Furthermore, references to the locations of that same automaton are replaced by true (for the target location of the edge) and false (for all other locations of the automaton). For instance, for an edge with update x := x + 1 and state invariant x < 5, the added guard is x + 1 < 5. Similarly as for the added initialization predicates, algebraic variables and derivatives of continuous variables may be inlined, no extra guard is added if it is trivially true, and the added guards are simplified as much as possible. Additionally, no extra guard is added to an edge if the state invariant’s predicate is not affected by the updates of the edge.

As an example, consider the following CIF specification:

automaton aut:
  disc int[1..10] x in any;
  invariant x >= 3;
  location:
    initial;
    edge do x := x - 1;
    edge do x := x + 1;
end

invariant aut.x <= 6;

Using the variant of this transformation that transforms all state invariants, it is transformed to the following CIF specification:

automaton aut:
  disc int[1..10] x in any;
  initial x >= 3;
  location:
    initial;
    edge when x - 1 <= 6, x - 1 >= 3 do x := x - 1;
    edge when x + 1 <= 6, x + 1 >= 3 do x := x + 1;
end
initial aut.x <= 6;

There are two state invariants. For each of them, an initialization predicate is added, in the same place as where the state invariant was originally located. Since x can has ten different possible initial values, the initialization predicates can’t be simplified further. The edges get extra guards, one per state invariant.

In some cases, no extra initialization predicates or guards are needed, or the predicates get simplified. For instance, consider the following example:

automaton aut:
  disc int[1..10] x = 3;
  invariant x >= 3;
  location:
    initial;
    edge do x := 3;
    edge do x := 7;
end

invariant aut.x <= 6;

Using the variant of this transformation that transforms all state invariants, it is transformed to the following CIF specification:

automaton aut:
  disc int[1..10] x = 3;
  location:
    initial;
    edge do x := 3;
    edge when false do x := 7;
end

Both invariants are true in the initial state, and thus no initialization predicates are added. For the first edge, both 3 >= 3 and 3 <= 6 are trivially true, and thus no extra guards are added. For the second edge, 7 >= 3 is trivially true and thus no extra guard is added for it, while 7 <= 6 is simplified to false and added as extra guard.

Renaming

n/a

Size considerations

The specification get larger or smaller:

  • A single state invariant may lead to both an initialization predicate being added and multiple extra guards being added.

  • Invariants may be simplified, reducing their size. However, invariants may also get references to algebraic variables and derivatives of continuous variables inlined, increasing their size.

Optimality

For state invariants that are defined in locations of automata with more than one location, this transformation makes their predicates conditional on those locations. To eliminate such location references, apply the CIF to CIF transformation to eliminate the use of locations in expressions.

Some effort is spent to simplify the added initialization predicates and guards. However, this simplification is not necessarily optimal; the predicates could potentially be simplified further.

Annotations

This transformation does not process or add any specific annotations. The annotations of eliminated state invariants are removed.