weird non-determinism in the output of ltl2tgba
I would expect the following command to output nothing.
./randltl -n -1 2 | ./ltl2tgba --any --low -F - | ./autfilt --states=3 --stats=%M | ./ltl2tgba --any --low -F - | ./autfilt -v --states=3
But that is not the case: the are formulas for which the first call to
ltl2tgba outputs 3 states, and the second call in the pipe, outputs a different number of states.
I suspect it is related to LTL simplification.