# a formula to optimize

Here is a recurrence formula for which Spot (2.3.4) produces a non-deterministic automaton:

`% ltl2tgba -D 'G(F(a & X(a)))'`

Constructing the automaton by hand, it is natural to suggest the following deterministic automaton where each state remembers the last letter read:

Can we adapt the translation somehow to produce that?

I've checked a few translators, and most of them produce non-deterministic automata like Spot. The only exception I have found is `ltl2da`

from Owl, which produces the following deterministic automaton:

`% owl-1.1.0/bin/ltl2da 'G(F(a & X(a)))'`

This formula came in a discussion with @max about the translation of `GF(a&Xa) & GF(a&!Xa)`

which should also be translated to a 2-state automaton (but isn't, even by `ltl2da`

).