Event-based controllability check

The controllability check verifies whether a supervisor automaton does not disable edges with uncontrollable events of the (combined) plant automata. If the check fails, the tool reports where it fails. If the check succeeds, it reports the edges with controllable events that are disabled by the supervisor.

The tool takes a .cif file containing a supervisor automaton, and one or more plant automata. Besides the general event-based restrictions listed at Supported specifications, the current implementation does not support:

The controllability check tool produces a report text file with its findings. It states whether the controllability property holds (no edges with uncontrollable events of the plant are disabled) or fails (one or more edges with uncontrollable events in the plant are disabled by the supervisor).

If the controllability property holds, the tool lists the disabled controllable events, which can be useful in the design process. If the property fails, the tool lists the edges that are disabled by the supervisor.

Starting the controllability check 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 controllability check…​.

  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools  Event-based synthesis tools  Apply controllability check…​.

  • Use the cifctrlchk tool in a ToolDef script. See the scripting documentation and tools overview page for details.

  • Use the cifctrlchk 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.

  • Report file: The absolute or relative local file system path to the output report file with disabled events. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a _disableds.txt file extension is added.