Skip to content

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.