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:

In addition, it warns about common mistakes:

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:

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