X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.mli;h=4ec2f59224c570773264b9ebe7989c2b0532d950;hb=6131f2f9e380543197c9fa253325bbc84749e6e8;hp=cd6610b37873ca945894467ee1b5105a87a772d4;hpb=2f157824afcbbc0852e2ff32ccb3e4dc2100a3b0;p=SXSI%2Fxpathcomp.git

diff --git a/ata.mli b/ata.mli
index cd6610b..4ec2f59 100644
--- a/ata.mli
+++ b/ata.mli
@@ -34,16 +34,21 @@ type dispatch = { first : Tree.t -> Tree.t;
 		  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