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