Event-based observer check
The event-based observer check takes an automaton, and a subset of the events of its alphabet that are observable. The check verifies whether the automaton after projection (see Event-based automaton projection) can derive the (abstracted) state of another component by synchronizing only on the observable events.
The tool takes a .cif file containing one automaton, and the names of the events that are observable. In addition, the general event-based restrictions apply as well.
The output is a report file that indicates whether the observer check property holds. If it fails, the events causing failure are also listed.
Starting the observer 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
cifobschktool in a ToolDef script. See the scripting documentation and tools overview page for details. -
Use the
cifobschkcommand 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.
-
Observable events: Comma and/or whitespace separated absolute names of events that are observable.
-
Report file: The absolute or relative local file system path to the output report file. If not specified, defaults to the input file path, where the
.ciffile extension is removed (if present), and a_observation.txtfile extension is added.