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
statespace2 have different languages. As evidence it indicates that
statespace1 can do a
do1 event in
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
loc12. The evidence the tool produces is thus wrong.