Event-based synthesis toolset
Synthesis, 'supervisor synthesis', or 'supervisory controller synthesis', is a generative technique, where one derives a (supervisor) automaton from a collection of plants and requirements. Synthesis is an essential part of the synthesis-based engineering approach to develop supervisory controllers. The resulting supervisor is maximally permissive under the conditions of being free of deadlocks, and always having the option of reaching a marked state.
While there is only one true synthesis tool (the tool that actually derives a supervisor automaton from a collection of plant and requirement automata), other tools exist to support the process. These tools together form the event-based synthesis toolset.
These tools use and modify the sequences of events that can be performed. This in contrast to state-based tools, which operate primarily on the state of the system. Event sequences directly hook into language theory, which places these tools firmly in the language theory mathematical framework.
When employing synthesis, consider also the data-based synthesis tool. It is often much more efficient when synthesizing supervisors for large and complex systems. It also supports a larger subset of CIF concepts.
Supported specifications
The application supports a subset of CIF specifications. The following restrictions apply:
-
Channels (events with data types) are not supported.
-
Any use of the
tauevent is not supported. Note that both explicit use (keywordtau) and implicit use (no events on an edge) are unsupported. -
Automata with multiple initial locations are not supported.
-
Edges with updates are not supported.
-
Urgent locations and edges are not supported.
-
Initialization predicates in components are not supported.
-
Initialization predicates in locations that are not trivially true or false are not supported.
-
Marker predicates in components are not supported.
-
Marker predicates in locations that are not trivially true or false are not supported.
-
Invariants are not supported, unless they don’t impose any restrictions.
-
Guards of edges that are not trivially true or false are not supported.
To allow state/event exclusion invariants to be used in the input, manually eliminate them first using the Eliminate state/event exclusion invariants CIF to CIF transformation.
For meaningful results, it is recommended to have an initial location and at least one marked location, in each automaton.
I/O declarations are ignored. For tools that produce CIF models, those models will not contain any I/O declarations.
Annotations are ignored. For tools that produce CIF models, those models will not contain any annotations, except that they may contain state annotations.
Preprocessing
The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:
Automaton kinds
The event-based toolset recognizes the CIF automaton kinds plant, requirement, and supervisor, and interprets them using the corresponding concepts of the mathematical framework of supervisor synthesis. Kindless/regular automata (without a supervisory kind) are treated as unknown.
Location names in reports and errors
Several tools output reports or give errors with locations that are interesting in some way.
Tools that take a single automaton as input report locations by their name in the input specification, for example location "button.off" denotes the off location in the button automaton. The location of automata that have a single unnamed location use * as location name, for example location "req.*" denotes the single unnamed location in the req automaton.
Tools that take a number of automata together, like supervisor synthesis report interesting states as state followed by the names of the locations, for example state "button.on", "machine.idle". Such a state refers to a location that represents the combined locations of the automata, in the example, the combined locations button.off and machine.idle.
Tools that combine or merge locations, like projection, report such combined locations as a partition, for example partition "machine.down", "machine.off" represents a location that is a combination of the down and the off locations in the machine automaton.
Available tools
-
Event-based synchronous product
Computes the product of a number of deterministic or non-deterministic automata, where common events are synchronized. Essentially computes the state space.
-
Event-based supervisor synthesis
Derivation of a maximal permissive supervisor from a collection of deterministic plant and requirement automata.
-
Event-based synthesis analysis
Analysis of the removed parts of a synthesized supervisor.
-
Event-based nonconflicting check
Verifies whether automata are conflicting, that is together could lead to non-coreachable states.
-
Event-based controllability check
Verifies whether the supervisor does not disable uncontrollable events of the plant.
-
Event-based language equivalence check
Verifies whether two automata produce the same events at each point.
-
Event-based NFA to DFA automaton conversion
Converts a non-deterministic automaton to a deterministic automaton while preserving the event behavior.
-
Minimize the number of locations of an automaton while preserving the event behavior.
-
Event-based automaton projection
Computes a projection of an automaton, resulting in a deterministic and language equivalent automaton over a subset of its alphabet.
-
Verifies whether an automaton can act as an observer of occurrences of observable events.
-
Event-based automaton abstraction
Abstracts an automaton to a set of observable events.
-
Verifies whether the automata are trim, that is, in each automaton, the locations must be both reachable and co-reachable.
-
Removes all locations that are not reachable or coreachable.