CIF 3

Event-based automaton projection

The event-based automaton projection takes an automaton and a subset of the events of its alphabet that should be preserved. The other events of the alphabet are considered to be internal steps and get replaced by epsilon at the edges. The algorithm produces a deterministic automaton with the subset as its alphabet that has the same language.

The tool takes a .cif file containing a single automaton, and the names of the events that should be preserved. The output is a .cif file containing a deterministic automaton that is language equivalent with the input automaton with respect to the set of preserved events. The resulting automaton has the same kind as the input automaton.

Starting the automaton projection 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 automaton projection....
  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply automaton projection....
  • Use the cif3proj tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3proj 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.
  • Preserved events: Comma and/or whitespace separated absolute names of events that should be preserved.
  • Output file: The absolute or relative local file system path to the output CIF specification. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a _projected.cif file extension is added. The projected part of the default extension depends on the Result name option.
  • Result name: The name to use for the projected automaton. If not specified, defaults to projected. Also affects the Output file option.