(***********************************************************************)
(*
- 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 =
-> 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