A sample of the equivalence test.
The test reports that the language of the current automaton is
equivalent to that of the automaton translated from [](p --> <> q).
You have to choose a target automaton after the function is triggered. This function checks if the language of the current automaton equals that of the chosen automaton. If the equivalence does not hold, similar to the containment test, one counterexample (an infinite word) will be shown. The equivalence test of two automata is built on top of the language containment test.