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

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

- Eliminate component definition/instantiation

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

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