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.
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.
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):
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
Since information is removed from the specification, the specification can only become smaller as a result of this transformation.