Event-based nonconflicting check
The nonconflicting check verifies whether two or more automata are conflicting, that is, whether they together could result in non-coreachable states.
One practical application is to check a supervisor, either synthesized or manually created, against a plant. That is, when the supervisor is used to control the plant, will it always stay in the safe coreachable area? If not, at what point does it fail to do so?
Another practical application is to check several supervisors synthesized for parts of a system. That is, when the supervisors are used together to control a system, could that result in non-coreachable states? If so, which states are conflicting?
The tool takes a .cif file containing two or more automata, that must be both deterministic and trim. In addition, the general event-based restrictions apply as well.
The nonconflicting check tool produces a text file, listing the traces that lead to a conflicting state. If no such traces are found, the automata are nonconflicting.
Starting the nonconflicting 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
cifncchktool in a ToolDef script. See the scripting documentation and tools overview page for details. -
Use the
cifncchkcommand 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 conflicts. If not specified, defaults to the input file path, where the
.ciffile extension is removed (if present), and a_conflicts.txtfile extension is added.