projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Hash-conses each node configuration.
[tatoo.git]
/
src
/
ata.mli
diff --git
a/src/ata.mli
b/src/ata.mli
index
374beb2
..
0b52462
100644
(file)
--- a/
src/ata.mli
+++ b/
src/ata.mli
@@
-14,7
+14,7
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-18 1
6:25:35
CEST by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-18 1
8:36:06
CEST by Kim Nguyen>
*)
type predicate =
*)
type predicate =
@@
-81,22
+81,17
@@
val create : StateSet.t -> StateSet.t -> t
val reset : t -> unit
val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
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
- -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
- -> TransList.t*StateSet.t
-
type config = {
sat : StateSet.t;
unsat : StateSet.t;
todo : TransList.t;
}
type config = {
sat : StateSet.t;
unsat : StateSet.t;
todo : TransList.t;
}
-val eq_config : config -> config -> bool
+module Config : Hcons.S with type data = config
-val eval_trans
2 : t -> config -> config -> config -> config
+val eval_trans
: t -> Config.t -> Config.t -> Config.t -> Config.t
-> bool -> bool -> bool -> bool -> Tree.NodeKind.t
-> bool -> bool -> bool -> bool -> Tree.NodeKind.t
- ->
config
+ ->
Config.t
val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit