CIF 3

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. Besides those restrictions, the general event-based restrictions listed at Supported specifications 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 .cif file in the Project Explorer or Package Explorer and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply nonconflicting check....
  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply nonconflicting check....
  • Use the cif3ncchk tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3ncchk 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 conflicts. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a _conflicts.txt file extension is added.