X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.mli;h=374beb271372e8f1225c76cd19b9057ed863bfa6;hp=bb94a7c67ab7c2d32e073cf47686745630530e12;hb=3c87bbf00b98bcf40dab913cd334846b26cdb71d;hpb=8aee3aeab119fc323d0c15b2134b22cdcc130063

diff --git a/src/ata.mli b/src/ata.mli
index bb94a7c..374beb2 100644
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-04 18:42:38 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-18 16:25:35 CEST by Kim Nguyen>
 *)
 
 type predicate =
@@ -86,6 +86,19 @@ val eval_trans : t -> TransList.t
   -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
   -> TransList.t*StateSet.t
 
+type config = {
+  sat : StateSet.t;
+  unsat : StateSet.t;
+  todo : TransList.t;
+}
+
+val eq_config : config -> config -> bool
+
+val eval_trans2 : t -> config -> config -> config -> config
+  -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
+  -> config
+
+
 val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
 val print : Format.formatter -> t -> unit
 val complete_transitions : t -> unit