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), if used (present on an edge of at least one automaton), are not supported.

  • Any use of the tau event is not supported. Note that both explicit use (keyword tau) 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.

  • Invariants in components are not supported.

  • Marker predicates in components are not supported.

  • Initialization predicates in locations that are not trivially true or false are not supported.

  • State invariants in locations that are not trivially true are not supported.

  • Marker predicates in locations that are not trivially true or false are not supported.

  • State/event exclusion invariants are not supported.

  • Guards of edges that are not trivially true or false are not supported.

  • Multiple initialization predicates in a single location are not supported.

  • Multiple state invariant predicates in a single location are not supported.

  • Multiple marker predicates in a single location are not supported.

  • Multiple guards on a single edge 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 and annotations are ignored. For tools that produce CIF models, those models will not contain any I/O declarations. The produced CIF models may however 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