Maintain the set of unsatisfiable states.

[tatoo.git] / src / ata.mli

diff --git a/src/ata.mli b/src/ata.mli
index bb94a7c..374beb2 100644 (file)
--- 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 =
 *)
 
 type predicate =


@@ -86,6 +86,19 @@ val eval_trans : t -> TransList.t
   -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
   -> TransList.t*StateSet.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
 val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
 val print : Format.formatter -> t -> unit
 val complete_transitions : t -> unit