This data type implements a symbolic description of an automaton: States are identified with the set of variables that hold in that state, and in addition to the formulas that encode the initial states and transitions, there is also a set of fairness constraints (of type GF) to define fair computations (these are the only ones that are considered).