CIF 3

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

For more information on applying these tools, and where these tools should be placed in the toolchain for the development of a supervisory controller, see the Supervisory controller development part of the documentation.

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.
  • Events that are not controllable or uncontrollable, if used (present in the alphabet or on an edge of at least one automaton), are not supported.
  • Any use of the tau event is not supported, as event tau is not controllable or uncontrollable. 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.

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.
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.
DFA minimization:
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.
Event-based observer check:
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.
Event-based trim check:
Verifies whether the automata are trim, that is, in each automaton, the locations must be both reachable and co-reachable.
Event-based trim:
Removes all locations that are not reachable or coreachable.