Hi Ruijie, Meng Ruijie <ruijie_meng(a)u.nus.edu> writes: "deterministic" only expresses a *preference*: in case the translator can make a choice between a smaller non-deterministic or a larger automata, it will honor your preference. But for Büchi/Generalized Büchi output this option does ensure that a deterministic automaton will be output when one exists. If you use the "study" tab of the online application, you can see that this formula belongs to the "Persistence" class, which means that no deterministic Büchi automaton exist for this particular formula. See https://spot.lrde.epita.fr/hierarchy.html for more documentation about the classes. In particular, the section about the Recurrence class (where deterministic Büchi automata always exist) shows a case where the translator produce a non-deterministic Büchi automaton even with -D, and how to work around that.