Dear Alexandre,

Thank you for your answer and for your help: your advice worked very well. Moreover, adding option "-x tls-impl=1" to our benchmark cut Spot's execution times by 60% on average.

Best regards,

On Fri, Oct 28, 2022 at 5:07 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:

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