Given the following input: [test.cif](/uploads/dedb6f4bf51669aa70fc3f1909b4dbe9/test.cif) 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.