Remove requirements

This CIF to CIF transformation removes requirements from the specification. By removing all requirements from a CIF specification with both plants and requirements, only the plants remain. The resulting plants can then be merged with a supervisor or other controller.

Supported specifications

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

  • Component definitions and component instantiations are not supported.

  • Using (referring to) requirement automata or declarations from requirement automata from outside requirement automata is not supported.

  • Kindless, plant, or supervisor invariants in locations of a requirement automaton are not supported.

Specifications where requirement automata or declarations declared in requirement automata are used (referred to) from outside requirement automata are not supported. By removing the requirement automata, those uses (references) become invalid, as the automata or declarations that are referenced no longer exist. For instance, consider:

alg int x = switch req: case l1: 1 else 2 end;

requirement automaton req:
  location l1:
    initial;
    edge tau goto l2;

  location l2;
end

When requirement automaton req is removed, the switch expression can no longer refer to that automaton, or to its locations. Removing the requirements from this CIF specification is 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

Both requirement automata and requirement invariants are removed. Requirement invariants are removed from the top level scope of the specification, all groups and automata, and all locations of automata. For instance, consider the following CIF specification:

controllable add;

plant automaton buffer:
  disc int x;

  plant invariant 0 <= x and x <= 5;
  requirement invariant x < 5;

  location:
    initial;
    plant invariant x >= 0;
    edge add do x := x + 1;
end

requirement automaton not2:
  location:
    initial;
    requirement invariant buffer.x >= 0;
    edge add when buffer.x != 2;
end

The result after this transformation is:

controllable add;

plant automaton buffer:
  disc int x;

  plant invariant 0 <= x and x <= 5;

  location:
    initial;
    plant invariant x >= 0;
    edge add do x := x + 1;
end

Renaming

n/a

Size considerations

Since information is removed from the specification, the specification can only become smaller as a result of this transformation.

Optimality

n/a

Annotations

This transformation does not process or add any annotations.

If requirement automata have annotations, or if elements in requirement automata have annotations, removing these requirement automata removes those annotations as well. Similarly, if requirement invariants are removed, then so are their annotations.

If the specification has a controller properties annotation, it is removed.