Event-based DFA minimization

Minimizing the number of locations of an automaton while preserving the language gives a canonical representation of the language, making it easier to compare automata. The DFA minimization tool computes such a minimal automaton.

The tool takes a .cif file containing one deterministic automaton with an initial location. In addition, the general event-based restrictions apply as well.

The DFA minimization tool produces an automaton with the same language, but with the minimal number of locations. If the original automaton already had the minimal number of locations, the result is the same as the input.

To minimize an NFA, first determinize it to a DFA.

Starting the DFA minimization 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 DFA minimization…​.

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

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

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

  • 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 _minimal.cif file extension is added. The minimal part of the default extension depends on the Result name option.

  • Result name: The name to use for the minimized automaton. If not specified, defaults to minimal. 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.