Expand description
Reachability specification for model checkers
This module defines the types for reachability specifications in threshold automata. On a high-level, a reachability specification asks whether an upwards closed set of locations can be reached.
In more detail, a reachability consists of two parts:
- A constraint that narrows down the set of initial locations (we will also
name this part of the specification
init). - A constraint specifying the set of configurations that should be
reached (we will also call this part of the constraint
target).
Such a constraint can be seen as an (E)LTL formula:
(init) => <>(target)
This module contains the logic to transform an arbitrary ELTL constraint
into a constraint of that form, assuming that it is a safety constraint
(i.e., it does not contain a []).
A reachability specification allows to specify a set of locations with a number of processes that must be at least in that location, as well as a set of locations that should not contain any processes. Additionally, one can specify a constraint on the valuations of the shared variables.
Structs§
- Disjunction
Target Config - Disjunction over multiple target configurations
- Reachability
- Formula of the form
(preconditions) => <>(target) - Reachability
Property - A named reachability Property
- Target
Config - Upward closed set of configurations representing a target set of configurations
Enums§
- Reachability
Transformation Error - Error that can occur during a transformation into a reachability specification
- Upwards
Closed SetExtraction Error - Errors that can occur when attempting to extract an upwards closed set of configurations
Traits§
Type Aliases§
- LocConstraint 🔒
- Alias for unconverted constraints over locations simplifying the definitions in the remainder of the file