X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=8a13705c5d5e056c4cec98123f0ab281b015ce80;hp=80843e6deae7aafb8860db5a3b8bce7125968ed5;hb=be682346caf089e95dc3254f89119f93797813f4;hpb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615

diff --git a/src/ata.ml b/src/ata.ml
index 80843e6..8a13705 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -206,7 +206,10 @@ end =
     let print ppf ?(sep="\n") l =
       iter (fun t ->
         let q, lab, f = Transition.node t in
-        fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l
+        fprintf ppf "%a, %a → %a%s"
+          State.print q
+          QNameSet.print lab
+          Formula.print f sep) l
   end
 
 
@@ -258,18 +261,19 @@ let print fmt a =
       []
   in
   let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
-    let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+    let c = State.compare q2 q1 in if c == 0 then QNameSet.compare s2 s1 else c)
     trs
   in
   let _ = _flush_str_fmt () in
-  let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
-    let s1 = State.print _str_fmt q; _flush_str_fmt () in
-    let s2 = QNameSet.print _str_fmt s;  _flush_str_fmt () in
-    let s3 = Formula.print _str_fmt f;  _flush_str_fmt () in
-    let pre = Pretty.length s1 + Pretty.length s2 in
-    let all = Pretty.length s3 in
-    ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
-  ) ([], 0, 0) sorted_trs
+  let strs_strings, max_pre, max_all =
+    List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+      let s1 = State.print _str_fmt q; _flush_str_fmt () in
+      let s2 = QNameSet.print _str_fmt s;  _flush_str_fmt () in
+      let s3 = Formula.print _str_fmt f;  _flush_str_fmt () in
+      let pre = Pretty.length s1 + Pretty.length s2 in
+      let all = Pretty.length s3 in
+      ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+    ) ([], 0, 0) sorted_trs
   in
   let line = Pretty.line (max_all + max_pre + 6) in
   let prev_q = ref State.dummy in
@@ -278,7 +282,8 @@ let print fmt a =
     if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n"  line;
     prev_q := q;
     fprintf fmt "%s, %s" s1 s2;
-    fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+    fprintf fmt "%s"
+      (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
     fprintf fmt " %s  %s@\n" Pretty.right_arrow s3;
   ) strs_strings;
   fprintf fmt "%s@\n" line
@@ -357,8 +362,10 @@ let normalize_negations auto =
   let rec flip b f =
     match Formula.expr f with
       Boolean.True | Boolean.False -> if b then f else Formula.not_ f
-    | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
-    | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
+    | Boolean.Or(f1, f2) ->
+      (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
+    | Boolean.And(f1, f2) ->
+      (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
     | Boolean.Atom(a, b') -> begin
       match a.Atom.node with
       | Move (m,  q) ->
@@ -444,8 +451,11 @@ let compute_rank auto =
   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 =
@@ -457,7 +467,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
@@ -483,7 +493,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 <-