flabel : string;
next : Tree.t -> Tree.t -> Tree.t;
nlabel : string;
+ consres : Tree.t -> TS.t -> TS.t -> bool -> bool -> TS.t;
}
+
+type formlist = Nil | Cons of state*formula*int*formlist
+
type t = {
id : int;
mutable states : Ptset.t;
init : Ptset.t;
mutable final : Ptset.t;
universal : Ptset.t;
+ starstate : Ptset.t option;
(* Transitions of the Alternating automaton *)
phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t;
- sigma : (dispatch*bool*formula) HTagSet.t;
+ sigma : (dispatch*bool*formlist*Ptset.t*Ptset.t) HTagSet.t;
}
val dump : Format.formatter -> t -> unit