X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=2dd5ad5cecf051d8a47feea5184810327394c7c7;hp=8a9bf9e2d161610f7727c4accb769735180b4958;hb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615;hpb=9c56424fe98c1182060170c724ef603392c82074

diff --git a/src/run.ml b/src/run.ml
index 8a9bf9e..2dd5ad5 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -79,10 +79,11 @@ module Make (T : Tree.S) =
    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 *)
-                        (* 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 *)
@@ -93,28 +94,33 @@ module Make (T : Tree.S) =
          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 =
-           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
-           "{ 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 =
-     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 = {
@@ -252,7 +258,9 @@ DEFINE AND_(t1,t2) =
                            | `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)
@@ -279,13 +287,25 @@ DEFINE AND_(t1,t2) =
          let phi =
            get_form cache2 auto tag q
          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
+  (*   Logger.msg `STATS ""; *)
      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 _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 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
-      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
@@ -334,17 +355,22 @@ DEFINE AND_(t1,t2) =
 
         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
-              { sat = StateSet.empty;
+              { rank = i;
+                sat = c.NodeStatus.node.sat;
                 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
@@ -469,7 +495,8 @@ DEFINE AND_(t1,t2) =
       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
@@ -490,10 +517,10 @@ DEFINE AND_(t1,t2) =
     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;
-    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
@@ -506,7 +533,7 @@ DEFINE AND_(t1,t2) =
     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;