This data type implements a representation of a Kripke structure by Bdds which is the basis for symbolic model checking with Bdds. It has the following components:

• nowAtoms : the list of atoms for the current state
• nxtAtoms : the corresponding list of atoms for the next state; i.e., where operator BoolNext was applied to the nowAtoms
• nowAtomsIdxBdd = BoolExpr2Bdd MkListConj nowAtoms
• nxtAtomsIdxBdd = BoolExpr2Bdd MkListConj nxtAtoms
• initCondBDD : Bdd index of the initial condition
• transRelBDD : Bdd index of the transition relation
• fairCnstBDDs : list of Bdd indices of the fairness constraints
• fairStatesBDD : Bdd index of the fair states (if already computed)

Note that nowAtomsIdxBdd and nxtAtomsIdxBdd are to be used for computing symbolic predecessor and successor state sets by Bdd function ExistAnd.