Reachability requirement annotations
A reachability requirement annotation can be used to specify a form of liveness requirements. A reachability requirement includes a goal predicate and may further restrict the source states, the states allowed on the path, and the maximum number of transitions to the goal. For the basic form without such restrictions, supervisory controller synthesis will ensure that in every state of the controlled system, either the goal predicate holds, or a state can be reached where it 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 unnamed argument.
-
The unnamed argument’s value must be a predicate (a boolean-typed expression).
-
Named and unnamed arguments may be specified in any order.
-
Optional named arguments must be named
from,avoid,stayorbound. -
The
from,avoidandstayargument values must be predicates (boolean-typed expressions). -
The
boundargument value must be a non-negative integer literal. -
The
avoidandstayarguments may not both be specified.
Goal
The unnamed argument is the goal predicate, and it specifies the set of states that must remain reachable. Without further arguments, the goal must remain reachable from every state in the controlled system.
Conditional reachability with from
The from argument turns the requirement into a conditional reachability requirement and restricts the states for which it applies. If from is specified, only states that satisfy the source predicate must be able to reach the goal. States that do not satisfy the source predicate are not affected by the conditional reachability requirement.
Restricted reachability with avoid or stay
The avoid and stay arguments turn the requirement into a restricted reachability requirement. They restrict both the states for which the requirement applies and the states that may occur on the path to the goal.
With avoid, the path may only use states that do not satisfy the restriction predicate. The starting and goal states may not satisfy the restriction predicate either. States that already satisfy the restriction predicate are not affected by this reachability requirement.
With stay, the path may only use states that satisfy the restriction predicate. For states to which the requirement applies, this includes the starting state, every intermediate state, and the goal state. States that already do not satisfy the restriction predicate are not affected by this reachability requirement.
The avoid and stay arguments express the same path restriction in inverse forms: avoid: pred is equivalent to stay: not pred, and stay: pred is equivalent to avoid: not pred. The arguments may not both be specified, so use the form that best describes the intended behavior and avoids unnecessary logical negations.
The from argument can be combined with avoid or stay to further restrict the source states of a restricted reachability requirement. Then only source states inside the allowed path region must be able to reach the goal along a path in that region.
Bounded reachability with bound
The bound argument turns the annotation into a bounded reachability requirement. The goal must then be reachable using at most the specified number of transitions. For bound: 0, a state satisfies the requirement only if it already satisfies the goal predicate, unless it is not affected by the requirement due to a from, avoid or stay argument.
The from argument can also restrict bounded reachability to source states. This results in a conditional and bounded reachability requirement. If from is specified, only states that satisfy the source predicate must be able to reach the goal within the bound. States that already do not satisfy the source predicate are not affected by this conditional and bounded reachability requirement. If bound is specified without from, the source predicate is true, so there is no additional source-state restriction. The avoid and stay arguments can similarly be combined with bound, resulting in restricted and bounded reachability requirements. Conditional, restricted and bounded reachability can all be combined in a single requirement.
For bounded reachability requirements, data-based synthesis debug output reports the configured bound, the minimum-bound status and the reason that the bounded computation stopped.
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_close;
location open:
initial;
marked;
edge c_close goto closed;
location closed:
edge c_open goto open;
endIn 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).