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, J.
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