incorrect ltlcross diagnostic
This was reported by Salomon Sickert.
$ ltlcross-2.9 --csv=/dev/null ltl2tgba ./ltl2da -f '(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'
G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a)))))))
Running [P0]: ltl2tgba -H 'G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a)))))))'>'lcr-o0-xfhILB'
Running [P1]: ./ltl2da 'G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a)))))))'>'lcr-o1-JWdJGD'
Running [N0]: ltl2tgba -H '!(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'>'lcr-o0-v4gGyF'
Running [N1]: ./ltl2da '!(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'>'lcr-o1-Emh2LD'
Performing sanity checks and gathering statistics...
error: {N0} disagree with {N1} when evaluating the state-space
the following word(s) are not accepted by {N1}:
N0 accepts: cycle{a; !a; !a; a}
error: some error was detected during the above runs,
please search for 'error:' messages in the above trace.
This fails with ltlcross
2.9 and 2.9.1, but not 2.8.7.
Also the output of ltl2da '!(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'
is the following automaton and it does accept the word cycle{a; !a; !a; a}
.
$ ./ltl2da '!(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))' | autfilt -c --accept-word='cycle{a; !a; !a; a}'
1
Also, because the automata are quite easy to complement, the "state-space products" tests are only run because --csv
is passed, and they are not expected to fail, because at this point ltlcross has already established automata equivalence.