Event-based automaton abstraction

The event-based automaton abstraction takes an automaton, and a subset of the events of its alphabet that are observable. The abstraction produces a non-deterministic abstracted automaton with the observable events as its alphabet, that is weakly bisimilar to the original automaton.

The tool takes a .cif file containing a single automaton, and the names of the events that are observable. Besides the general event-based restrictions, the tool does not support:

The output is a .cif file with the abstracted automaton. The resulting automaton has the same kind as the input automaton.

Starting the automaton abstraction tool

The tool can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools  Event-based synthesis tools  Apply automaton abstraction…​.

  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools  Event-based synthesis tools  Apply automaton abstraction…​.

  • Use the cifabstr tool in a ToolDef script. See the scripting documentation and tools overview page for details.

  • Use the cifabstr 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.

  • Output file: The absolute or relative local file system path to the output CIF file. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a _abstracted.cif file extension is added. The abstracted part of the default extension depends on the Result name option.

  • Result name: The name to use for the abstracted automaton. If not specified, defaults to abstracted. Also affects the Output file option.

  • Add state annotations: Add state annotations to the locations of the automaton in the output CIF file. This option is enabled by default.