[Spot] Re: [bug] ltl2tgba gets stuck with this formula

Hi Jacopo, Thank you for the feedback.

ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl

I ran this with gdb just to see where Spot was spending its time, and discovered it was doing automata-based implication checks to try to reduce the LTL formula before actually translating it. I'll have to dig into this a bit more later to see what can be improved [1]. In the meantime I think you can safely disable those checks, as they are mostly useful when translating random formulas. Try adding option -x tls-impl=1: ltl2tgba -S -D --dot=s -o output.txt -x tls-impl=1 -F gb_formula.ltl This took 0.21s on my laptop. Best regards, Alexandre [1] https://gitlab.lrde.epita.fr/spot/spot/-/issues/521