31 Oct
2022
31 Oct
'22
9:36 p.m.
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(a)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