## 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 `.cif` or `.cifx` file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools Event-based synthesis tools Apply observer check…​.

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

- Use the `cifobschk` tool in a ToolDef script. See the scripting documentation and tools overview page for details.

- Use the `cifobschk` 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.

- 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 `.cif` file extension is removed (if present), and a `_observation.txt` file extension is added.