25 Oct
2022
25 Oct
'22
4:45 p.m.
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>gt;.
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
--
Jacopo Binchi
jbinchi(a)developair.es
Paseo de Miramón 170
20014 San Sebastián – Donostia
Gipuzkoa (Spain)
www.developair.es
28 Oct
28 Oct
5:06 p.m.
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
31 Oct
31 Oct
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
828
days inactive
834
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Jacopo Binchi