Dear Spot support team, I am a researcher at Developair Technologies. I write you looking for help with a formula that ltl2tgba cannot handle, possibly a bug. Here at Developair we have been using Spot for the past few months with great satisfaction. However, it seems that *ltl2tgba *cannot process the formula in attached file gb_formula.ltl . We let it run for quite some time (like hours) and it didn't terminate. On the other hand, Owl can process the same formula in a matter of a few milliseconds. We don't have any problem using ltl2tgba with other, similar formulas.
It seems strange to us that Spot gets stuck with such a relatively simple formula, especially since in our experience Spot worked reliably well with other, way more complex formulas. Is it maybe a bug or something that we are doing wrong? Could you please help us? Please find some more details (version and command) below.
Thank you. Best regards, J.
Spot version: ltl2tgba --version
ltl2tgba (spot) 2.10.6
Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita. License GPLv3+: GNU GPL version 3 or later < http://gnu.org/licenses/gpl.html%3E. This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.
Command: ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl
Using the "simplest" command "ltl2tgba -F gb_formula.ltl" produces the same result (that is, no result).
For comparison, with Owl we used command: owl ltl2ldgba --state-acceptance -i gb_formula.ltl -o owl_gb.txt
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
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
-
Alexandre Duret-Lutz -
Jacopo Binchi