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 a single automaton, and the names of the events that are observable. The output is a report file that indicates whether the observer check property holds. If it fails, the events causing failure are also listed.
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 .
cifobschkcommand line tool.
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.