X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=cb2ea3b548b4fa879733285788de5c7544765e71;hp=d7d5177a3275c5dc175a1b8beccdaaccaec5c499;hb=6ca42ffbd541cede6afcc473b563e54b848ee534;hpb=398ce5dca1bee23f5137a3eba21df17d7aaaf1fa

diff --git a/src/run.ml b/src/run.ml
index d7d5177..cb2ea3b 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -222,6 +222,38 @@ END
          loop phi
 
 
+   let eval_trans_aux cache4 fcs nss ps ss old_config =
+     let { sat = old_sat;
+           unsat = old_unsat;
+           todo = old_todo;
+           summary = old_summary } = old_config.NodeStatus.node
+     in
+     let sat, unsat, removed, kept, todo =
+       Ata.TransList.fold
+         (fun trs acc ->
+           let q, lab, phi = Ata.Transition.node trs in
+           let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
+           if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
+             let new_phi =
+               eval_form phi fcs nss ps old_config old_summary
+             in
+             if Ata.Formula.is_true new_phi then
+               StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+             else if Ata.Formula.is_false new_phi then
+               a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+             else
+               let new_tr = Ata.Transition.make (q, lab, new_phi) in
+               (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
+         ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
+     in
+           (* States that have been removed from the todo list and not kept are now
+              unsatisfiable *)
+     let unsat = StateSet.union unsat (StateSet.diff removed kept) in
+           (* States that were found once to be satisfiable remain so *)
+     let unsat = StateSet.diff unsat sat in
+     let new_config = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in
+     new_config
+
 
    let eval_trans cache4 fcs nss ps ss =
      let fcsid = (fcs.NodeStatus.id :> int) in
@@ -233,35 +265,9 @@ END
          let res = Cache.N4.find cache4 oid fcsid nssid psid in
          if res != dummy_status then res
          else
-           let { sat = old_sat;
-                 unsat = old_unsat;
-                 todo = old_todo;
-                 summary = old_summary } = old_config.NodeStatus.node
+           let new_config = 
+             eval_trans_aux cache4 fcs nss ps ss old_config
            in
-           let sat, unsat, removed, kept, todo =
-             Ata.TransList.fold
-               (fun trs acc ->
-                 let q, lab, phi = Ata.Transition.node trs in
-                 let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
-                 if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
-                   let new_phi =
-                     eval_form phi fcs nss ps old_config old_summary
-                   in
-                   if Ata.Formula.is_true new_phi then
-                     StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
-                   else if Ata.Formula.is_false new_phi then
-                     a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
-                   else
-                     let new_tr = Ata.Transition.make (q, lab, new_phi) in
-                     (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
-               ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
-           in
-        (* States that have been removed from the todo list and not kept are now
-           unsatisfiable *)
-           let unsat = StateSet.union unsat (StateSet.diff removed kept) in
-        (* States that were found once to be satisfiable remain so *)
-           let unsat = StateSet.diff unsat sat in
-           let new_config = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in
            Cache.N4.add cache4 oid fcsid nssid psid new_config;
            new_config
        in
@@ -294,10 +300,11 @@ END
           let c = unsafe_get_status status node_id in
           if c == dummy_status then
             (* first time we visit the node *)
+            let ltrs = get_trans cache2 auto tag (Ata.get_states auto) in
             NodeStatus.make
               { sat = StateSet.empty;
                 unsat = Ata.get_starting_states auto;
-                todo = get_trans cache2 auto tag (Ata.get_states auto);
+                todo = ltrs;
                 summary = NodeSummary.make
                   (node == T.first_child tree parent) (* is_left *)
                   (node == T.next_sibling tree parent) (* is_right *)
@@ -416,6 +423,35 @@ END
     in
     loop (T.root tree) []
 
+
+  let get_full_results run =
+    let cache = run.status in
+    let auto = run.auto in
+    let tree = run.tree in
+    let res_mapper = Hashtbl.create MED_H_SIZE in
+    let () =
+      StateSet.iter
+        (fun q -> Hashtbl.add res_mapper q [])
+        (Ata.get_selecting_states auto)
+    in
+    let rec loop node =
+      if node != T.nil then
+        let () = loop (T.next_sibling tree node) in
+        let () = loop (T.first_child tree node) in
+        StateSet.iter
+          (fun q ->
+            try
+              let acc = Hashtbl.find res_mapper q in
+              Hashtbl.replace res_mapper q (node::acc)
+            with
+              Not_found -> ())
+          cache.(T.preorder tree node).NodeStatus.node.sat
+    in
+    loop (T.root tree);
+    StateSet.fold
+      (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+      (Ata.get_selecting_states auto) []
+
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in
@@ -444,12 +480,24 @@ END
       status.(node_id) <- status0) list
 
 
-
-  let eval auto tree nodes =
+  let eval full auto tree nodes =
     let run = make auto tree in
     prepare_run run nodes;
     while run.redo do
-      top_down run;
+      top_down run
     done;
-    get_results run
+    if full then `Full (get_full_results run)
+    else `Normal (get_results run)
+
+
+  let full_eval auto tree nodes =
+    match eval true auto tree nodes with
+      `Full l -> l
+    | _ -> assert false
+
+  let eval auto tree nodes =
+    match eval false auto tree nodes with
+      `Normal l -> l
+    | _ -> assert false
+
 end