## Event-based supervisor synthesis

The supervisor synthesis procedure takes one or more deterministic plant automata, zero or more deterministic requirement automata, and combines them to a maximal permissive supervisor.

The tool takes a CIF file containing `plant` and (optionally) `requirement` automata. Besides the general event-based restrictions, the tool does not support:

- Having no `plant` automata at all.

- Having a `supervisor` or kindless automaton in the file. See Automaton kinds for a list of all automaton kinds.

- Having any non-deterministic automata.

- Events in the alphabet of the requirements that are not in the alphabet of the plants.

- Events that are not controllable or uncontrollable.

In addition, it warns about common mistakes:

- Automata without a marked location.

- Non-trim automata.

- Specifications without any `requirement` automata.

Finally, it can also perform checks about correct constructs that may not be the intention of its author. Each of these checks has to be enabled with an option:

- Automata with a marked deadlock location. In a system with infinite behavior, you should probably never enter a deadlock location.

- Automata with an empty alphabet. Such automata never participate in an event, and can be removed.

- Controllable events that are used in exactly one automaton. Not always wrong, but creating a controllable event, and not using it for control may be a mistake.

- Groups of automata that share events only within the group (and not with any automaton outside the group). Such a group is completely independent, and can be synthesized separately.

The synthesis tool produces a new CIF file with the supervisor automaton (of kind `supervisor`) if the resulting automaton has at least an initial location. Otherwise, synthesis fails with a `Supervisor is empty` error, and no CIF file is written.

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.

### Starting the supervisor synthesis tool

The tool can be started in the following ways:

- In Eclipse, right click a `.cif` or `.cifx` file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools Event-based synthesis tools Apply supervisor synthesis…​.

- In Eclipse, right click an open text editor for a `.cif` or `.cifx` file and choose CIF synthesis tools Event-based synthesis tools Apply supervisor synthesis…​.

- Use the `cifsupsynth` tool in a ToolDef script. See the scripting documentation and tools overview page for details.

- Use the `cifsupsynth` command line tool.

### Options

Besides the general application options, this application has the following options:

- Input file: The absolute or relative local file system path to the input CIF specification.

- Output file: The absolute or relative local file system path to the output CIF specification. If not specified, defaults to the input file path, where the `.cif` file extension is removed (if present), and a `_sup.cif` file extension is added. The `sup` part of the default extension depends on the Result name option.

- Result name: The name to use for the supervisor automaton. If not specified, defaults to `sup`. Also affects the Output file option.

- Add state annotations: Add state annotations to the locations of the automaton in the output CIF file. This option is enabled by default.

- Enable Synthesis dump: If enabled, the synthesis algorithm writes a dump file containing the actions performed by the algorithm, for later analysis. The name of the file is decided by the Dump file option.

- Synthesis dump file: The name of the dump file. Setting this option will enable dumping of the synthesis algorithm actions. The options contains the absolute or relative local file system path to the synthesis dump file. If not specified, defaults to the input file path, where the `.cif` file extension is removed (if present), and a `.synth_dump` file extension is added.

- Disjunct groups check: If enabled, the tool will report about groups of automata that share events in the group only.

- Empty alphabet check: If enabled, the tool will report about automata without events in their alphabet.

- Marked deadlock location check: If enabled, the tool will report about marked locations without outgoing edges.

- Single use controllable check: If enabled, the tool will report about controllable events that are used in exactly one automaton.