On Sat, Aug 24, 2019 at 8:22 AM M. H. Zibaeenejad hadi_zbn@yahoo.com wrote:

I have used the version 2.0 of your online tool for LTL to Buchi automata translation. At the time the tool did not return a deterministic Buchi automaton, but the new version does the transformation with ease.

I was wondering if something fundamental has changed in your code that made this possible. Do you have the Changelog from 2.0 to 2.8?

Hi Hadi

A list of user-visible changes in all versions is at https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-1/NEWS v2.0, is at line 2448

A lot of things have changed, and the translation pipeline is regularly improved by adding new tricks and simplifications. However your formula is quite simple in this regard. I don't have it around to verify, but I suspect that the command-line tool ltl2tgba was already able to output a deterministic automaton in Spot 2.0. However you said you used to online translator so I suspect that the main factor is just that this online tool was rewritten. In the past, the online translator would do very limited optimizations by default, and you had to enable those by hand: for instance simulation-based reductions, which I think is the only important step in your case, were off by default if I remember correctly. The online tool even had its own translation pipeline different from (and inferior to) the command-line tool. Today the online tool uses the very same logic as the ltl2tgba tool, and apply all simplifications by default.