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.
The general event-based restrictions apply.
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
.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
ciftrimchktool in a ToolDef script. See the scripting documentation and tools overview page for details. -
Use the
ciftrimchkcommand 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_trimcheck.txtfile extension is added.