//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2025, 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

[[lang-ref-annotations-reachability-requirement]]
== Reachability requirement annotations

A reachability requirement <<lang-ref-annotations,annotation>> can be used to specify a form of liveness requirements.
A reachability requirement includes a reachability requirement predicate.
<<lang-tut-synthesis-intro,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 <<lang-tut-annotations-reachability-requirement,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 <<lang-ref-annotations-constraints,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:

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