Hi Akshay, On Mon, Jun 18, 2012 at 10:10 PM, Agrawal, Akshay <akshay.agrawal(a)vanderbilt.edu> wrote: No, all transitions are not accepting by definition of TGBA. If you got this impression while reading Spot's web pages or Spot's source code, it would help if you could tell me what gave you this impression, so that I can clarify the wording. A TGBA may have several acceptance sets of transitions. A transition may be in several acceptance set. An infinite run of a TGBA is accepted if it visits at least one transition from each acceptance set infinitely often. If course this definition implies that if no acceptance set is defined, or if all acceptance set all include all transitions, then all transitions are accepting. But these are special cases. Acc[r] is the name of an acceptance set. The transitions marked with Acc[r] are the transitions that belong to this acceptance set. On the automaton for this particular formula, this set ensures that a run that stays in state "Fr" continuously is rejected. No acceptance set are needed to express Xr as a TGBA. That means that all infinite runs are accepting (but in this case, the automaton has only one possible run anyway). Best regards, -- Alexandre Duret-Lutz