projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
* Seal the representation of states
[tatoo.git]
/
src
/
ata.ml
diff --git
a/src/ata.ml
b/src/ata.ml
index
190c4c7
..
5f7a282
100644
(file)
--- a/
src/ata.ml
+++ b/
src/ata.ml
@@
-184,8
+184,8
@@
module Transition =
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
- let hash (
a, b, c
) =
- HASHINT4 (PRIME1,
a
, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
+ let hash (
(a, b, c) : t
) =
+ HASHINT4 (PRIME1,
((a) :> int)
, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
end)
let print ppf t =
let q, l, f = t.node in
end)
let print ppf t =
let q, l, f = t.node in
@@
-276,10
+276,10
@@
let print fmt a =
) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
- let prev_q = ref State.dummy in
+ let prev_q = ref State.dummy
_state
in
fprintf fmt "%s@\n" line;
List.iter (fun (q, s1, s2, s3) ->
fprintf fmt "%s@\n" line;
List.iter (fun (q, s1, s2, s3) ->
- if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line;
+ if !prev_q != q && !prev_q != State.dummy
_state
then fprintf fmt "%s@\n" line;
prev_q := q;
fprintf fmt "%s, %s" s1 s2;
fprintf fmt "%s"
prev_q := q;
fprintf fmt "%s, %s" s1 s2;
fprintf fmt "%s"
@@
-387,7
+387,7
@@
let normalize_negations auto =
with
Not_found ->
(* create a new state and add it to the todo queue *)
with
Not_found ->
(* create a new state and add it to the todo queue *)
- let nq = State.
make
() in
+ let nq = State.
next
() in
auto.states <- StateSet.add nq auto.states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
auto.states <- StateSet.add nq auto.states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
@@
-409,7
+409,7
@@
let normalize_negations auto =
with
Not_found ->
let nq = if b then q else
with
Not_found ->
let nq = if b then q else
- let nq = State.
make
() in
+ let nq = State.
next
() in
auto.states <- StateSet.add nq auto.states;
nq
in
auto.states <- StateSet.add nq auto.states;
nq
in
@@
-597,7
+597,7
@@
let rename_states mapper a =
let copy a =
let mapper = Hashtbl.create MED_H_SIZE in
let () =
let copy a =
let mapper = Hashtbl.create MED_H_SIZE in
let () =
- StateSet.iter (fun q -> Hashtbl.add mapper q (State.
make
())) a.states
+ StateSet.iter (fun q -> Hashtbl.add mapper q (State.
next
())) a.states
in
rename_states mapper a
in
rename_states mapper a
@@
-657,7
+657,7
@@
let link a1 a2 q link_phi =
let union a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
let union a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
@@
-669,7
+669,7
@@
let union a1 a2 =
let inter a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
let inter a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (stay q) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (stay q) phi))
@@
-680,7
+680,7
@@
let inter a1 a2 =
let neg a =
let a = copy a in
let neg a =
let a = copy a in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (not_(stay q)) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (not_(stay q)) phi))