-type t = {
- id : int;
- mutable states : Ptset.t;
- init : Ptset.t;
- mutable final : Ptset.t;
- universal : Ptset.t;
- phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
- delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
-(* delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
- sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.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;