projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Actually fix the problems with negation.
[tatoo.git]
/
src
/
auto
/
ata.ml
diff --git
a/src/auto/ata.ml
b/src/auto/ata.ml
index
275d657
..
13c4854
100644
(file)
--- a/
src/auto/ata.ml
+++ b/
src/auto/ata.ml
@@
-14,7
+14,7
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-0
5 18:25:03
CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-0
8 16:24:41
CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
*)
INCLUDE "utils.ml"
@@
-272,10
+272,10
@@
let normalize_negations auto =
(* create a new state and add it to the todo queue *)
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
(* create a new state and add it to the todo queue *)
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
-
(*
if not (StateSet.mem q auto.bottom_states) then
+ if not (StateSet.mem q auto.bottom_states) then
auto.bottom_states <- StateSet.add nq auto.bottom_states;
if not (StateSet.mem q auto.top_states) then
auto.bottom_states <- StateSet.add nq auto.bottom_states;
if not (StateSet.mem q auto.top_states) then
- auto.top_states <- StateSet.add nq auto.top_states;
*)
+ auto.top_states <- StateSet.add nq auto.top_states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
in
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
in
@@
-296,10
+296,10
@@
let normalize_negations auto =
let nq = if b then q else
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
let nq = if b then q else
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
-
(*
if not (StateSet.mem q auto.bottom_states) then
+ if not (StateSet.mem q auto.bottom_states) then
auto.bottom_states <- StateSet.add nq auto.bottom_states;
if not (StateSet.mem q auto.top_states) then
auto.bottom_states <- StateSet.add nq auto.bottom_states;
if not (StateSet.mem q auto.top_states) then
- auto.top_states <- StateSet.add nq auto.top_states;
*)
+ auto.top_states <- StateSet.add nq auto.top_states;
nq
in
Hashtbl.add memo_state key nq; nq
nq
in
Hashtbl.add memo_state key nq; nq