## 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):

- Eliminate component definition/instantiation

### Implementation details

All types of requirements are removed:

- Requirement automata

- Requirement invariants

- Reachability requirement annotations

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

Similarly, reachability requirement annotations are removed from the top-level scope of the specification as well as from all components (automata and groups).

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

All reachability requirement annotations are removed. Furthermore, 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.