[Spot] [bug] ltl2tgba gets stuck with this formula

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