//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-cif2cif-chapter-remove-reqs]]
== Remove requirements

indexterm:[CIF to CIF transformer,remove requirements]
indexterm:[remove requirements]
indexterm:[requirement,remove]
This CIF to CIF transformation removes <<lang-tut-synthesis-plant-req-sup,requirements>> from the specification.
By removing all requirements from a CIF specification with both <<lang-tut-synthesis-plant-req-sup,plants>> and requirements, only the plants remain.
The resulting plants can then be <<tools-chapter-mergecif,merged>> with a <<lang-tut-synthesis-plant-req-sup,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:

[source, cif]
----
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 <<tools-cif2cif-chapter-index,CIF to CIF transformations>> (in the given order):

* <<tools-cif2cif-chapter-elim-comp-def-inst>>

=== Implementation details

All types of requirements are removed:

* <<lang-tut-synthesis-autkind,Requirement automata>>
* <<lang-tut-synthesis-invkind,Requirement invariants>>
* <<lang-tut-annotations-reachability-requirement,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:

[source, cif]
----
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:

[source, cif]
----
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 <<lang-tut-annotations-controller,controller properties annotation>>, it is removed.
