X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=190c4c72443ec18c6d76186eda0c96f326d37bd3;hp=f55452ea0932ed469e10c9354b966f6daa92bcb4;hb=6844beef9142975d1bf4a2b3fb72b93dfa3402dc;hpb=35abea737ead2d4fd121d0cb8bdbda38cfcaa8d3

diff --git a/src/ata.ml b/src/ata.ml
index f55452e..190c4c7 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -445,14 +445,24 @@ let compute_dependencies auto =
 
   edges
 
+let state_prerequisites dir auto q =
+  Hashtbl.fold (fun q' trans acc ->
+    List.fold_left (fun acc (_, phi) ->
+      let m_phi = Formula.get_states_by_move phi in
+      if StateSet.mem q (Move.get m_phi dir)
+      then StateSet.add q' acc else acc)
+      acc trans) auto.transitions StateSet.empty
 
 let compute_rank auto =
   let dependencies = compute_dependencies auto in
   let upward = [ `Stay ; `Parent ; `Previous_sibling ] in
   let downward = [ `Stay; `First_child; `Next_sibling ] in
   let swap dir = if dir == upward then downward else upward in
-  let is_satisfied q t =
-    Move.for_all (fun _ set -> StateSet.(is_empty (remove q set))) t
+  let is_satisfied dir q t =
+    Move.for_all (fun d set ->
+      if List.mem d dir then
+        StateSet.(is_empty (remove q set))
+      else StateSet.is_empty set) t
   in
   let update_dependencies dir initacc =
     let rec loop acc =
@@ -464,7 +474,7 @@ let compute_rank auto =
               Move.set deps m (StateSet.diff (Move.get deps m) to_remove)
             )
             dir;
-          if is_satisfied q deps then StateSet.add q acc else acc
+          if is_satisfied dir q deps then StateSet.add q acc else acc
         ) dependencies acc
       in
       if acc == new_acc then new_acc else loop new_acc
@@ -490,7 +500,6 @@ let compute_rank auto =
   done;
   let by_rank = Hashtbl.create 17 in
   List.iter (fun (r,s) ->
-    let r = r/2 in
     let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
     Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
   auto.ranked_states <-