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
supervisorautomaton.Having no
plantorsupervisorautomaton.Having an automaton with a different kind than
plantorsupervisor.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
.ciffile in the Project Explorer tab or Package Explorer tab and choose .In Eclipse, right click an open text editor for a
.ciffile and choose .Use the
cifctrlchktool in a ToolDef script. See the scripting documentation and tools overview page for details.Use the
cifctrlchkcommand 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
.ciffile extension is removed (if present), and a_disableds.txtfile extension is added.