X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fata.ml;fp=src%2Fauto%2Fata.ml;h=aa4fb385a2d80c3244b180f42ad99f5753a9e3d8;hp=ca641b498d16aa85a42f91e7d18399ecca7dc720;hb=f49a93deba13602e16a3923695281e9a20215ac8;hpb=e13f5deae217f945b44fa345ef4f0008e1780787

diff --git a/src/auto/ata.ml b/src/auto/ata.ml
index ca641b4..aa4fb38 100644
--- a/src/auto/ata.ml
+++ b/src/auto/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-02-08 18:43:08 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-04 16:36:40 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -84,11 +84,11 @@ struct
 end
 
 module SFormula = Formula.Make(Move)
-type 'a t = {
+type t = {
   id : Uid.t;
   mutable states : StateSet.t;
-  mutable top_states : StateSet.t;
-  mutable bottom_states: StateSet.t;
+(*  mutable top_states : StateSet.t;
+  mutable bottom_states: StateSet.t; *)
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
 }
@@ -97,8 +97,8 @@ let next = Uid.make_maker ()
 
 let create () = { id = next ();
                   states = StateSet.empty;
-                  top_states = StateSet.empty;
-                  bottom_states = StateSet.empty;
+(*                  top_states = StateSet.empty;
+                  bottom_states = StateSet.empty; *)
                   selection_states = StateSet.empty;
                   transitions = Hashtbl.create 17;
  }
@@ -137,14 +137,12 @@ let print fmt a =
   fprintf fmt
     "Unique ID: %i@\n\
      States %a@\n\
-     Top states: %a@\n\
-     Bottom states: %a@\n\
      Selection states: %a@\n\
      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states
-    StateSet.print a.top_states
-    StateSet.print a.bottom_states
+(*    StateSet.print a.top_states
+    StateSet.print a.bottom_states *)
     StateSet.print a.selection_states;
   let trs =
     Hashtbl.fold
@@ -233,7 +231,7 @@ let normalize_negations a =
       end
     end
   in
-  StateSet.iter (fun q -> Queue.add (q, true) todo) a.top_states;
+  StateSet.iter (fun q -> Queue.add (q, true) todo) a.selection_states;
   while not (Queue.is_empty todo) do
     let (q, b) as key = Queue.pop todo in
     let q' =
@@ -247,9 +245,4 @@ let normalize_negations a =
     let trans = Hashtbl.find a.transitions q in
     let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
     Hashtbl.replace a.transitions q' trans'
-  done;
-  Hashtbl.iter (fun (q, b) q' ->
-    if not (b || StateSet.mem q a.bottom_states) then
-      a.bottom_states <- StateSet.add q' a.bottom_states
-  ) memo_state
-
+  done