CIF 3

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:

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

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 or Package Explorer 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 cif3ctrlchk tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3ctrlchk 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.