Skip to content

`ltl2tgba` side effect with stream of formulae

When ltl2tgba is fed a stream of formulae, it does not find the same automata as if given the same formulae one by one.

The attached file provides such a sequence. On the last formula of the file, ltl2tgba -D -G finds an automaton with 5 states if the formula is given alone, and finds an automaton with 4 states all 36 formulae of the file are given.

262.txt