Model: [model.cif](/uploads/fba788469e31f6ddf8f5520b227fe0a8/model.cif) The CIF language equivalence check indicates the two automata are language equivalent. However: * `aut1` can do `c_evt1` from its initial location to `loc2` that is marked. * `aut2` can do `c_evt1` from its initial location to `loc8` that is not marked. * One automaton accepts `c_evt1` as trace, and the other doesn't. They are not language equivalent.