## Reachability requirement annotations

A reachability requirement annotation can be used to specify a form of liveness requirements. A reachability requirement includes a reachability requirement predicate. Supervisory controller synthesis will ensure that in every state of the controlled system, either the predicate holds, or a state can be reached where the predicate holds. For basic information on reachability requirement annotations, see the language tutorial. Here we discuss further details.

### Constraints

Reachability requirement annotations (`@requirement:reachable`) can only be added to the following elements of the specification:

- To the root of the specification (using `@@requirement:reachable`).

- To components (automata and groups).

- To component definitions (automaton definitions and group definitions).

- To component instantiations (automaton instantiations and group instantiations).

The annotation has the following constraints, in addition to the general constraints that apply to all annotations:

- The annotation must have exactly one argument.

- The argument must not have a name.

- The value must be a predicate (a boolean-typed expression).

### Scoping

If a reachability requirement annotation is specified on a component or component definition, then references to named elements are resolved from within the body of the component or component definition. For example:

    input bool closed;

    @requirement:reachable(closed)
    plant bridge:
      controllable c_open, c_closed;

      location open:
        initial;
        marked;
        edge c_close goto closed;

      location closed:
        edge c_open goto open;
    end

In this case, the predicate refers to `closed`, and this is resolved to the location `closed` in the body of the `bridge` automaton (in the automaton’s scope), rather than to the input variable named `closed` (in the specification’s root scope).