Event-based language equivalence check
The language equivalence check verifies whether two automata produce the same language, that is, at every point they are marked in the same way and can produce the same events. Note that even automata with a different number of locations or edges can be language equivalent.
All reachable locations of the automata are checked. In particular, it also checks locations that are outside the marked behavior (that is, reachable locations that are not marked and are not on a path to a marked location). To avoid false positives, you may want to ensure that both automata are trim.
One practical application is to verify whether a manually created supervisor is equivalent to an automatically generated one. If they are not, a counter example is produced.
The tool takes a .cif file containing exactly two automata, that must be deterministic, have the same alphabet, and have an initial location. In addition, the general event-based restrictions listed at Supported specifications apply as well.
The language equivalence check tool produces output stating Automata have the same language, or it produces a counter example where an event can be performed in a location in one automaton, while from the equivalent location in the other automaton the same event cannot be performed. The equivalent location is derived by walking from the initial location to the location of interest in both automata, using the same sequence of events.
Starting the language equivalence check tool
The tool can be started in the following ways:
-
In Eclipse, right click a
.ciffile in the Project Explorer tab or Package Explorer tab and choose . -
In Eclipse, right click an open text editor for a
.ciffile and choose . -
Use the
ciflngeqvtool in a ToolDef script. See the scripting documentation and tools overview page for details. -
Use the
ciflngeqvcommand line tool.