## 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, the tool does not support:

- Having more than one `supervisor` automaton.

- Having no `plant` or `supervisor` automaton.

- Having an automaton with a different kind than `plant` or `supervisor`.

- Having a non-deterministic automaton.

- Events that are not controllable or uncontrollable.

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` or `.cifx` 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` or `.cifx` 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.