//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-eventbased-chapter-language-equivalence-check]]
== Event-based language equivalence check

indexterm:[event-based language equivalence check]
indexterm:[tools,event-based language equivalence check]
indexterm:[event-based synthesis toolset,event-based language equivalence check]
indexterm:[event-based language equivalence check,event-based synthesis toolset]
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 <<tools-eventbased-chapter-trim,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 <<tools-eventbased-supported-specifications,general event-based restrictions>> apply as well.

The language equivalence check tool can produce three different results:

* The output stating `Automata have the same language` when the two automata are language equivalent.

* The output stating `Automata have a different language` when 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 output stating `Automata have a different language` when a location in one automaton is marked, while the equivalent location in the other automaton is not marked.

In the last two cases, 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.
When two automata are not language equivalent, a counter example is produced that shows the sequence of events to reach the equivalent locations.

indexterm:[event-based language equivalence check,start]

=== Starting the language equivalence check tool

The tool can be started in the following ways:

* In Eclipse, right click a `.cif` or `.cifx` file in the _Project Explorer_ tab or _Package Explorer_ tab and choose menu:CIF synthesis tools[Event-based synthesis tools > Apply language equivalence check...].

* In Eclipse, right click an open text editor for a `.cif` or `.cifx` file and choose menu:CIF synthesis tools[Event-based synthesis tools > Apply language equivalence check...].

* Use the `ciflngeqv` tool in a ToolDef script.
See the <<tools-scripting-chapter-intro,scripting documentation>> and <<tools-scripting-chapter-tools,tools overview>> page for details.

* Use the `ciflngeqv` command line tool.

indexterm:[event-based language equivalence check,options]

=== 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.
