Event-based trim check

This check verifies that the automata in the given file are trim, that is, in each automaton, all the locations must be both reachable and coreachable. If the check fails for one or more automata, the tool reports for each automaton, whether all its locations are reachable and coreachable. It also lists the locations where the property fails.

Starting the trim check tool

The tool can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools  Event-based synthesis tools  Apply trim check…​.

  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools  Event-based synthesis tools  Apply trim check…​.

  • Use the ciftrimchk tool in a ToolDef script. See the scripting documentation and tools overview page for details.

  • Use the ciftrimchk 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 _trimcheck.txt file extension is added.