Skip to content

translation to improve

The following was reported by Mikuláš Klokočka.

ltl2tgba translates G(a & XF(b & XF(c & XFd))) in an automaton with 5 states, while ltl2ldpa (from Owl 1.1.0) produces an automaton with 1 state.

I guess we could just make sure that this is simplified to G(a & Fb & Fc & Fd), but maybe we can also improve the already-special handling of G in the translation.

Also, this looks like a nice pattern to add to genltl.