(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-04 18:42:38 CEST by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-18 18:36:06 CEST by Kim Nguyen>
*)
type predicate =
val reset : t -> unit
val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
-val eval_trans : t -> TransList.t
- -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
+type config = {
+ sat : StateSet.t;
+ unsat : StateSet.t;
+ todo : TransList.t;
+}
+
+module Config : Hcons.S with type data = config
+
+val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t
-> bool -> bool -> bool -> bool -> Tree.NodeKind.t
- -> TransList.t*StateSet.t
+ -> Config.t
+
val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
val print : Format.formatter -> t -> unit