## 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:

- Having no automata at all, or more than one automaton.

- Automata with only marked locations, or with only non-marked locations.

- Observable events that are not in the alphabet of the automaton.

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.