From: Kim Nguyễn <kn@lri.fr>
Date: Thu, 14 Mar 2013 10:26:51 +0000 (+0100)
Subject: Reuse the same cache between different iterations.
X-Git-Tag: v0.1~120
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=4a4bc22723f8953276f7d6768225334c5c4c2565

Reuse the same cache between different iterations.
---

diff --git a/src/auto/eval.ml b/src/auto/eval.ml
index 19bcf6f..71adf56 100644
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 19:02:13 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-14 11:12:24 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -106,15 +106,8 @@ module Make (T : Tree.Sig.S) :
   in
   loop ltrs ss
 
-  let top_down_run auto tree node cache _i =
+  let top_down_run auto tree node cache trans_cache2 trans_cache6  _i =
     let redo = ref false in
-    let dummy2 = Ata.TransList.cons
-      (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
-      Ata.TransList.nil
-    in
-    let dummy6 = (dummy2, StateSet.empty) in
-    let trans_cache6 = Cache.N6.create 17 dummy6 in
-    let trans_cache2 = Cache.N2.create 17 dummy2 in
     let rec loop node =
       if node != T.nil then begin
         let parent = T.parent tree node in
@@ -127,7 +120,7 @@ module Make (T : Tree.Sig.S) :
             Cache.N2.find trans_cache2
               (tag.QName.id :> int) (auto.Ata.states.StateSet.id :> int)
           in
-          if trs == dummy2 then
+          if trs == Cache.N2.dummy trans_cache2 then
             let trs = Ata.get_trans auto auto.Ata.states tag in
             (Cache.N2.add
               trans_cache2
@@ -184,8 +177,23 @@ module Make (T : Tree.Sig.S) :
     let cache = Cache.N1.create (T.size tree) StateSet.empty in
     let redo = ref true in
     let iter = ref 0 in
+    let dummy2 = Ata.TransList.cons
+      (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
+      Ata.TransList.nil
+    in
+    let dummy6 = (dummy2, StateSet.empty) in
+    let trans_cache6 = Cache.N6.create 17 dummy6 in
+    let trans_cache2 = Cache.N2.create 17 dummy2 in
+    let () = at_exit (fun () ->
+      let num_phi = ref 0 in
+      let num_trans = ref 0 in
+      Cache.N6.iteri (fun _ _ _ _ _ _ _ b  -> if not b then incr num_phi) trans_cache6;
+      Cache.N2.iteri (fun _ _ _ b -> if not b then incr num_trans) trans_cache2;
+      Format.eprintf "PROFILE:materialized %i transitions and %i configurations\n@." !num_trans !num_phi
+    )
+    in
     while !redo do
-      redo := top_down_run auto tree node cache !iter;
+      redo := top_down_run auto tree node cache trans_cache2 trans_cache6 !iter;
       incr iter;
     done;
     get_results auto tree node cache