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