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