Implement the ranked automata evaluation to guarantee a O(|D|x|Q|)

worst case complexity. The states of an automaton are given a rank (an
integer) such that if rank(q) = i, then state q can be satisfied
during run i at the latest. The maximum rank of a state is bounded by
the number of "bi-directional" states, that is, the number of states
which depends at the same time on a state upward and on another state
downard. Therefore, the rank is at most |Q|. For the moment, we
evaluate state [q] *only* during run i. This implies the O(|D|x|Q|)
overal complexity but also means we loose a chance to discard (or
accept) [q] early. A heuristic could improve that.

diff --git a/src/ata.ml b/src/ata.ml
index 3263e46..80843e6 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -54,6 +54,17 @@ module Move =
         true
       with
         Exit -> false
         true
       with
         Exit -> false

+    let for_all2 p m1 m2 =
+      try
+        for i = 0 to 4 do
+          let v1 = m1.(i)
+          and v2 = m2.(i) in
+          if not (p (ridx i) v1 v2) then raise Exit
+        done;
+        true
+      with
+        Exit -> false
+

     let exists p m =
       try
         iter (fun i v -> if p i v then raise Exit) m;
     let exists p m =
       try
         iter (fun i v -> if p i v then raise Exit) m;


@@ -206,6 +217,7 @@ type t = {
   mutable starting_states : StateSet.t;
   mutable selecting_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
   mutable starting_states : StateSet.t;
   mutable selecting_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;

+  mutable ranked_states : StateSet.t array

 }
 
 let uid t = t.id
 }
 
 let uid t = t.id


@@ -213,7 +225,8 @@ let uid t = t.id
 let get_states a = a.states
 let get_starting_states a = a.starting_states
 let get_selecting_states a = a.selecting_states
 let get_states a = a.states
 let get_starting_states a = a.starting_states
 let get_selecting_states a = a.selecting_states

-
+let get_states_by_rank a = a.ranked_states
+let get_max_rank a = Array.length a.ranked_states - 1

 
 let _pr_buff = Buffer.create 50
 let _str_fmt = formatter_of_buffer _pr_buff
 
 let _pr_buff = Buffer.create 50
 let _str_fmt = formatter_of_buffer _pr_buff


@@ -229,12 +242,15 @@ let print fmt a =
      Number of states: %i@\n\
      Starting states: %a@\n\
      Selection states: %a@\n\
      Number of states: %i@\n\
      Starting states: %a@\n\
      Selection states: %a@\n\

+     Ranked states: %a@\n\

      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states
     (StateSet.cardinal a.states)
     StateSet.print a.starting_states
      Alternating transitions:@\n"
     (a.id :> int)
     StateSet.print a.states
     (StateSet.cardinal a.states)
     StateSet.print a.starting_states

-    StateSet.print a.selecting_states;
+    StateSet.print a.selecting_states
+    (let r = ref 0 in Pretty.print_array ~sep:", " (fun ppf s ->
+      fprintf ppf "%i:%a" !r StateSet.print s; incr r)) a.ranked_states;

   let trs =
     Hashtbl.fold
       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
   let trs =
     Hashtbl.fold
       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)


@@ -379,26 +395,99 @@ let normalize_negations auto =
 
   while not (Queue.is_empty todo) do
     let (q, b) as key = Queue.pop todo in
 
   while not (Queue.is_empty todo) do
     let (q, b) as key = Queue.pop todo in

-    let q' =
-      try
-        Hashtbl.find memo_state key
-      with
-        Not_found ->
-          let nq = if b then q else
-              let nq = State.make () in
-              auto.states <- StateSet.add nq auto.states;
-              nq
-          in
-          Hashtbl.add memo_state key nq; nq
-    in
-    let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in
-    let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
-    Hashtbl.replace auto.transitions q' trans';
+    if not (StateSet.mem q auto.starting_states) then
+      let q' =
+        try
+          Hashtbl.find memo_state key
+        with
+          Not_found ->
+            let nq = if b then q else
+                let nq = State.make () in
+                auto.states <- StateSet.add nq auto.states;
+                nq
+            in
+            Hashtbl.add memo_state key nq; nq
+      in
+      let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in
+      let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
+      Hashtbl.replace auto.transitions q' trans';

   done;
   cleanup_states auto
 
   done;
   cleanup_states auto
 

-
-
+(* [compute_dependencies auto] returns a hash table storing for each
+   states [q] a Move.table containing the set of states on which [q]
+   depends (loosely). [q] depends on [q'] if there is a transition
+   [q, {...} -> phi], where [q'] occurs in [phi].
+*)
+let compute_dependencies auto =
+  let edges = Hashtbl.create 17 in
+  StateSet.iter
+    (fun q -> Hashtbl.add edges q (Move.create_table StateSet.empty))
+    auto.starting_states;
+  Hashtbl.iter (fun q trans ->
+    let moves = try Hashtbl.find edges q with Not_found ->
+      let m = Move.create_table StateSet.empty in
+      Hashtbl.add edges q m;
+      m
+    in
+    List.iter (fun (_, phi) ->
+      let m_phi = Formula.get_states_by_move phi in
+      Move.iter (fun m set ->
+        Move.set moves m (StateSet.union set (Move.get moves m)))
+        m_phi) trans) auto.transitions;
+
+  edges
+
+
+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
+  in
+  let update_dependencies dir initacc =
+    let rec loop acc =
+      let new_acc =
+        Hashtbl.fold (fun q deps acc ->
+          let to_remove = StateSet.union acc initacc in
+          List.iter
+            (fun m ->
+              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
+        ) dependencies acc
+      in
+      if acc == new_acc then new_acc else loop new_acc
+    in
+    let satisfied = loop StateSet.empty in
+    StateSet.iter (fun q ->
+      Hashtbl.remove dependencies q) satisfied;
+    satisfied
+  in
+  let current_states = ref StateSet.empty in
+  let rank_list = ref [] in
+  let rank = ref 0 in
+  let current_dir = ref upward in
+  let detect_cycle = ref 0 in
+  while Hashtbl.length dependencies != 0 do
+    let new_sat = update_dependencies !current_dir !current_states in
+    if StateSet.is_empty new_sat then incr detect_cycle;
+    if !detect_cycle > 2 then assert false;
+    rank_list := (!rank, new_sat) :: !rank_list;
+    rank := !rank + 1;
+    current_dir := swap !current_dir;
+    current_states := StateSet.union new_sat !current_states;
+  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 <-
+    Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i)

 
 
 module Builder =
 
 
 module Builder =


@@ -415,26 +504,9 @@ module Builder =
           starting_states = StateSet.empty;
           selecting_states = StateSet.empty;
           transitions = Hashtbl.create MED_H_SIZE;
           starting_states = StateSet.empty;
           selecting_states = StateSet.empty;
           transitions = Hashtbl.create MED_H_SIZE;

+          ranked_states = [| |]

         }
       in
         }
       in

-      (*
-      at_exit (fun () ->
-        let n4 = ref 0 in
-        let n2 = ref 0 in
-        Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2;
-        Cache.N4.iteri (fun _ _ _ _ _ b -> if b then incr n4) auto.cache4;
-        Logger.msg `STATS "automaton %i, cache2: %i entries, cache6: %i entries"
-          (auto.id :> int) !n2 !n4;
-        let c2l, c2u = Cache.N2.stats auto.cache2 in
-        let c4l, c4u = Cache.N4.stats auto.cache4 in
-        Logger.msg `STATS
-          "cache2: length: %i, used: %i, occupation: %f"
-          c2l c2u (float c2u /. float c2l);
-        Logger.msg `STATS
-          "cache4: length: %i, used: %i, occupation: %f"
-          c4l c4u (float c4u /. float c4l)
-
-      ); *)

       auto
 
     let add_state a ?(starting=false) ?(selecting=false) q =
       auto
 
     let add_state a ?(starting=false) ?(selecting=false) q =


@@ -469,6 +541,7 @@ module Builder =
     let finalize a =
       complete_transitions a;
       normalize_negations a;
     let finalize a =
       complete_transitions a;
       normalize_negations a;

+      compute_rank a;

       a
   end
 
       a
   end
 


@@ -502,6 +575,7 @@ let rename_states mapper a =
         (fun l ->
           (List.map (fun (labels, form) -> (labels, map_form rename form)) l))
         a.transitions;
         (fun l ->
           (List.map (fun (labels, form) -> (labels, map_form rename form)) l))
         a.transitions;

+    ranked_states = Array.map (map_set rename) a.ranked_states

   }
 
 let copy a =
   }
 
 let copy a =


@@ -526,16 +600,17 @@ let concat a1 a2 =
     (fun q ->
       Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)])
     a2.starting_states;
     (fun q ->
       Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)])
     a2.starting_states;

-  { a1 with
+  let a = { a1 with

     states = StateSet.union a1.states a2.states;
     selecting_states = a2.selecting_states;
     transitions = a1.transitions;
   }
     states = StateSet.union a1.states a2.states;
     selecting_states = a2.selecting_states;
     transitions = a1.transitions;
   }

+  in compute_rank a; a

 
 let merge a1 a2 =
   let a1 = copy a1 in
   let a2 = copy a2 in
 
 let merge a1 a2 =
   let a1 = copy a1 in
   let a2 = copy a2 in

-  { a1 with
+  let a = { a1 with

     states = StateSet.union a1.states a2.states;
     selecting_states = StateSet.union a1.selecting_states a2.selecting_states;
     starting_states = StateSet.union a1.starting_states a2.starting_states;
     states = StateSet.union a1.states a2.states;
     selecting_states = StateSet.union a1.selecting_states a2.selecting_states;
     starting_states = StateSet.union a1.starting_states a2.starting_states;


@@ -544,11 +619,12 @@ let merge a1 a2 =
         Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions
       in
       a1.transitions
         Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions
       in
       a1.transitions

-  }
+  } in
+  compute_rank a ; a

 
 
 let link a1 a2 q link_phi =
 
 
 let link a1 a2 q link_phi =

-  { a1 with
+  let a = { a1 with

     states = StateSet.union a1.states a2.states;
     selecting_states = StateSet.singleton q;
     starting_states = StateSet.union a1.starting_states a2.starting_states;
     states = StateSet.union a1.states a2.states;
     selecting_states = StateSet.singleton q;
     starting_states = StateSet.union a1.starting_states a2.starting_states;


@@ -559,6 +635,8 @@ let link a1 a2 q link_phi =
       Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)];
       a1.transitions
   }
       Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)];
       a1.transitions
   }

+  in
+  compute_rank a; a

 
 let union a1 a2 =
   let a1 = copy a1 in
 
 let union a1 a2 =
   let a1 = copy a1 in


@@ -587,7 +665,7 @@ let inter a1 a2 =
 let neg a =
   let a = copy a in
   let q = State.make () in
 let neg a =
   let a = copy a in
   let q = State.make () in

-  let link_phi = 
+  let link_phi =

     StateSet.fold
       (fun q phi -> Formula.(and_ (not_(stay q)) phi))
       a.selecting_states
     StateSet.fold
       (fun q phi -> Formula.(and_ (not_(stay q)) phi))
       a.selecting_states


@@ -599,7 +677,6 @@ let neg a =
       selecting_states = StateSet.singleton q;
     }
   in
       selecting_states = StateSet.singleton q;
     }
   in

-  normalize_negations a; a
+  normalize_negations a; compute_rank a; a

 
 let diff a1 a2 = inter a1 (neg a2)
 
 let diff a1 a2 = inter a1 (neg a2)

-

diff --git a/src/ata.mli b/src/ata.mli
index 650673e..2aa27b3 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -32,6 +32,7 @@ module Move :
     val iter : (t -> 'a -> unit) -> 'a table -> unit
     val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
     val for_all : (t -> 'a -> bool) -> 'a table -> bool
     val iter : (t -> 'a -> unit) -> 'a table -> unit
     val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
     val for_all : (t -> 'a -> bool) -> 'a table -> bool

+    val for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool

     val exists : (t -> 'a -> bool) -> 'a table -> bool
   end
 
     val exists : (t -> 'a -> bool) -> 'a table -> bool
   end
 


@@ -48,7 +49,7 @@ type predicate =
 
 module Atom : sig
   include Hcons.S with type data = predicate
 
 module Atom : sig
   include Hcons.S with type data = predicate

-  include Common_sig.Printable with type t:= t
+  include Common_sig.Printable with type t := t

 end
 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
 
 end
 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
 


@@ -112,6 +113,15 @@ val get_starting_states : t -> StateSet.t
 val get_selecting_states : t -> StateSet.t
 (** return the set of selecting states of the automaton *)
 
 val get_selecting_states : t -> StateSet.t
 (** return the set of selecting states of the automaton *)
 

+val get_states_by_rank : t -> StateSet.t array
+(** return an array of states ordered by ranks.
+*)
+
+val get_max_rank : t -> int
+(** return the maximal rank of a state in the automaton, that is the
+    maximum number of runs needed to fuly evaluate the automaton.
+*)
+

 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 (** [get_trans auto l q] returns the list of transitions taken by [auto]
     for label [l] in state [q]. Takes time proportional to the number of
 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 (** [get_trans auto l q] returns the list of transitions taken by [auto]
     for label [l] in state [q]. Takes time proportional to the number of

diff --git a/src/pretty.ml b/src/pretty.ml
index 6d1dd46..66a0225 100644 (file)
--- a/src/pretty.ml
+++ b/src/pretty.ml
@@ -128,11 +128,13 @@ let pp_print_list ?(sep=dummy_printer) printer fmt l =
   match l with
     [] -> ()
   | [ e ] -> printer fmt e
   match l with
     [] -> ()
   | [ e ] -> printer fmt e

-  | e :: es -> printer fmt e; List.iter
+  | e :: es -> printer fmt e;
+    List.iter

     (fun x ->
       sep fmt ();
       fprintf fmt "%a" printer x) es
 
     (fun x ->
       sep fmt ();
       fprintf fmt "%a" printer x) es
 

+

 let pp_print_array ?(sep=dummy_printer) printer fmt a =
   pp_print_list ~sep:sep printer fmt (Array.to_list a)
 
 let pp_print_array ?(sep=dummy_printer) printer fmt a =
   pp_print_list ~sep:sep printer fmt (Array.to_list a)
 


@@ -144,5 +146,3 @@ let print_list ?(sep=" ") printer fmt l =
 
 let print_array ?(sep=" ") printer fmt a =
   print_list ~sep:sep printer fmt (Array.to_list a)
 
 let print_array ?(sep=" ") printer fmt a =
   print_list ~sep:sep printer fmt (Array.to_list a)

-
-

diff --git a/src/run.ml b/src/run.ml
index 8a9bf9e..2dd5ad5 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -79,10 +79,11 @@ module Make (T : Tree.S) =
    end
 
    type node_status = {
    end
 
    type node_status = {

+     rank : int;

      sat : StateSet.t;  (* States that are satisfied at the current node *)
      todo : StateSet.t; (* States that remain to be proven *)
      sat : StateSet.t;  (* States that are satisfied at the current node *)
      todo : StateSet.t; (* States that remain to be proven *)

-                        (* For every node_status and automaton a:
-                           a.states - (sat U todo) = unsat *)
+        (* For every node_status and automaton a,
+           a.states - (sat U todo) = unsat *)

      summary : NodeSummary.t; (* Summary of the shape of the node *)
    }
 (* Describe what is kept at each node for a run *)
      summary : NodeSummary.t; (* Summary of the shape of the node *)
    }
 (* Describe what is kept at each node for a run *)


@@ -93,28 +94,33 @@ module Make (T : Tree.S) =
          type t = node_status
          let equal c d =
            c == d ||
          type t = node_status
          let equal c d =
            c == d ||

+             c.rank == d.rank &&

              c.sat == d.sat &&
              c.todo == d.todo &&
              c.summary == d.summary
 
          let hash c =
              c.sat == d.sat &&
              c.todo == d.todo &&
              c.summary == d.summary
 
          let hash c =

-           HASHINT3((c.sat.StateSet.id :> int),
+           HASHINT4(c.rank,
+                    (c.sat.StateSet.id :> int),

                     (c.todo.StateSet.id :> int),
                     c.summary)
        end
        )
        let print ppf s =
          fprintf ppf
                     (c.todo.StateSet.id :> int),
                     c.summary)
        end
        )
        let print ppf s =
          fprintf ppf

-           "{ sat: %a; todo: %a; summary: _ }"
+           "{ rank: %i; sat: %a; todo: %a; summary: _ }"
+           s.node.rank

            StateSet.print s.node.sat
            StateSet.print s.node.todo
      end
 
    let dummy_status =
            StateSet.print s.node.sat
            StateSet.print s.node.todo
      end
 
    let dummy_status =

-     NodeStatus.make { sat = StateSet.empty;
-                       todo = StateSet.empty;
-                       summary = NodeSummary.dummy;
-                     }
+     NodeStatus.make {
+       rank = -1;
+       sat = StateSet.empty;
+       todo = StateSet.empty;
+       summary = NodeSummary.dummy;
+     }

 
 
    type run = {
 
 
    type run = {


@@ -252,7 +258,9 @@ DEFINE AND_(t1,t2) =
                            | `Parent | `Previous_sibling -> ps
                            | `Stay -> ss
                          in
                            | `Parent | `Previous_sibling -> ps
                            | `Stay -> ss
                          in

-                         if sum == dummy_status || StateSet.mem q n_sum.todo then
+                         if sum == dummy_status
+                           || n_sum.rank < ss.NodeStatus.node.rank
+                           || StateSet.mem q n_sum.todo then

                            Unknown
                          else
                            of_bool (b == StateSet.mem q n_sum.sat)
                            Unknown
                          else
                            of_bool (b == StateSet.mem q n_sum.sat)


@@ -279,13 +287,25 @@ DEFINE AND_(t1,t2) =
          let phi =
            get_form cache2 auto tag q
          in
          let phi =
            get_form cache2 auto tag q
          in

+

          let v = eval_form phi fcs nss ps old_status old_summary in
          let v = eval_form phi fcs nss ps old_status old_summary in

+(*
+         Logger.msg `STATS "Evaluating for tag %a, state %a@\ncontext: %a@\nleft: %a@\nright: %a@\n\t formula %a yields %s"
+           QName.print tag
+           State.print q
+           NodeStatus.print old_status
+           NodeStatus.print fcs
+           NodeStatus.print nss
+           Ata.Formula.print phi
+           (match v with True -> "True" | False -> "False" | _ -> "Unknown");
+*)

          match v with
            True -> StateSet.add q a_sat, a_todo
          | False -> acc
          | Unknown -> a_sat, StateSet.add q a_todo
        ) old_todo (old_sat, StateSet.empty)
      in
          match v with
            True -> StateSet.add q a_sat, a_todo
          | False -> acc
          | Unknown -> a_sat, StateSet.add q a_todo
        ) old_todo (old_sat, StateSet.empty)
      in

+  (*   Logger.msg `STATS ""; *)

      if old_sat != sat || old_todo != todo then
        NodeStatus.make { os_node with sat; todo }
      else old_status
      if old_sat != sat || old_todo != todo then
        NodeStatus.make { os_node with sat; todo }
      else old_status


@@ -313,17 +333,18 @@ DEFINE AND_(t1,t2) =
 
 
   let top_down run =
 
 
   let top_down run =

-    let _i = run.pass in
+    let i = run.pass in

     let tree = run.tree in
     let auto = run.auto in
     let status = run.status in
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable in
     let tree = run.tree in
     let auto = run.auto in
     let status = run.status in
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable in

-    let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in
+    let states_by_rank = Ata.get_states_by_rank auto in
+    let init_todo = states_by_rank.(i) in

     let rec loop node =
       let node_id = T.preorder tree node in
     let rec loop node =
       let node_id = T.preorder tree node in

-      if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
+      if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false else begin

         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in
         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in


@@ -334,17 +355,22 @@ DEFINE AND_(t1,t2) =
 
         let status0 =
           let c = unsafe_get_status status node_id in
 
         let status0 =
           let c = unsafe_get_status status node_id in

-          if c == dummy_status then
-            (* first time we visit the node *)
+          if c.NodeStatus.node.rank < i then
+            (* first time we visit the node during this run *)

             NodeStatus.make
             NodeStatus.make

-              { sat = StateSet.empty;
+              { rank = i;
+                sat = c.NodeStatus.node.sat;

                 todo = init_todo;
                 todo = init_todo;

-                summary = NodeSummary.make
-                  (node == T.first_child tree parent) (* is_left *)
-                  (node == T.next_sibling tree parent) (* is_right *)
-                  (fc != T.nil) (* has_left *)
-                  (ns != T.nil) (* has_right *)
-                  (T.kind tree node) (* kind *)
+                summary = let summary = c.NodeStatus.node.summary
+                          in
+                          if summary != NodeSummary.dummy then summary
+                          else
+                            NodeSummary.make
+                              (node == T.first_child tree parent) (* is_left *)
+                              (node == T.next_sibling tree parent) (* is_right *)
+                              (fc != T.nil) (* has_left *)
+                              (ns != T.nil) (* has_right *)
+                              (T.kind tree node) (* kind *)

               }
           else c
         in
               }
           else c
         in


@@ -469,7 +495,8 @@ DEFINE AND_(t1,t2) =
       let ns = T.next_sibling tree node in
       let status0 =
         NodeStatus.make
       let ns = T.next_sibling tree node in
       let status0 =
         NodeStatus.make

-          { sat = Ata.get_starting_states auto;
+          { rank = 0;
+            sat = Ata.get_starting_states auto;

             todo =
               StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
             summary = NodeSummary.make
             todo =
               StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
             summary = NodeSummary.make


@@ -490,10 +517,10 @@ DEFINE AND_(t1,t2) =
     tree_size := T.size tree;
     let run = make auto tree in
     prepare_run run nodes;
     tree_size := T.size tree;
     let run = make auto tree in
     prepare_run run nodes;

-    while run.redo do
+    for i = 0 to Ata.get_max_rank auto do

       top_down run
     done;
       top_down run
     done;

-    pass := run.pass;
+    pass := Ata.get_max_rank auto + 1;

     IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
 
     run
     IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
 
     run


@@ -506,7 +533,7 @@ DEFINE AND_(t1,t2) =
     let r = compute_run auto tree nodes in
     get_results r
 
     let r = compute_run auto tree nodes in
     get_results r
 

-  let stats () = { 
+  let stats () = {

     tree_size = !tree_size;
     run = !pass;
     cache2_access = !cache2_access;
     tree_size = !tree_size;
     run = !pass;
     cache2_access = !cache2_access;