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.