On Fri, Apr 26, 2019 at 8:18 AM David Müller david.mueller2@tu-dresden.de wrote:

Hi Alexandre,

I run the experiments and found two formulas where ltl2tgba did not finish correctly. The formulas were

& | G F p0 F G p1 | G F ! p1 F G p2 & & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0

The according command-line was:

ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA} Output was: ltl2tgba: direct_simulation() requires separate Inf and Fin sets

Thanks. I'm looking into this.

You can somehow work around this problem by adding option -x ba-simul=0 to this line. For historical reason, the name of this option suggests that it is only for Büchi automata (and as a bonus bug, it's unfortunately still documented this way), but it's actually used for any state-based acceptance today.