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
.