On Sat, Aug 24, 2019 at 8:22 AM M. H. Zibaeenejad <hadi_zbn(a)yahoo.com> wrote: 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. -- Alexandre Duret-Lutz