-type t = {
- id : int;
- states : Ptset.t;
- init : Ptset.t;
- final : Ptset.t;
- universal : Ptset.t;
- phi : (TagSet.t * state, bool * formula) Hashtbl.t;
- delta : (TagSet.t, Ptset.t * bool * Ptset.t * Ptset.t) Hashtbl.t;
- properties : (state,property) Hashtbl.t;
+type dispatch = { first : Tree.t -> Tree.t;
+ flabel : string;
+ next : Tree.t -> Tree.t -> Tree.t;
+ nlabel : string;
+ }
+type t = {
+ id : int;
+ mutable states : Ptset.t;
+ init : Ptset.t;
+ mutable final : Ptset.t;
+ universal : Ptset.t;
+ (* Transitions of the Alternating automaton *)
+ phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t;
+ sigma : (dispatch*bool*formula) HTagSet.t;