alternative techniques for when autcross fails to complement an automaton
Currently autcross
needs to complement automata in order to test equivalence. If the complementation is not possible (for instance maybe the automaton is too big for determinization to be reasonable, see #541 (closed)) it would be nice to have alternate techniques we could use to test equivalence or even just approximate it.
For instance if I compute A*B and find that there is an accepting SCC of A that is never synchronized with any accepting SCC of B, than I can exhibit a word of A rejected by B, and I have a proved that A isn't included in B. This is only an implication, but surely this is better than nothing.