CIF event-based language equivalence check output contradicts itself
Given the following input:
The CIF event-based language equivalence check tool produces the following output:
Automata have a different language!
From location "loc12" of automaton "statespace1", event "do1" can be performed, but from the equivalent location "loc12" of automaton "statespace2", the event cannot be performed.
It indicates the two automata statespace1 and statespace2 have different languages. As evidence it indicates that statespace1 can do a do1 event in loc12, while statespace2 can't (in that same location).
However, the following is from the CIF specification, for these locations in both automata:
...
location loc12:
edge enter goto loc20;
edge do1 goto loc21;
edge done2 goto loc17;
...
location loc12:
edge done2 goto loc15;
edge enter goto loc20;
edge do1 goto loc21;
...
Clearly both automata allow do1 in loc12. The evidence the tool produces is thus wrong.