CIF 3

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 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.

Starting the observer check tool

The tool can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer or Package Explorer and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply observer check....
  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply observer check....
  • Use the cif3obschk tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3obschk 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.