24 Aug
2019
24 Aug
'19
5:28 p.m.
On Sat, Aug 24, 2019 at 8:22 AM M. H. Zibaeenejad <hadi_zbn(a)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.
--
Alexandre Duret-Lutz