X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Feval.ml;h=71adf56e145b28067e06c388fcfc906a95256f3c;hp=cc9ed71074436f9d9acf4f20ed538f8c9d6f77dd;hb=4a4bc22723f8953276f7d6768225334c5c4c2565;hpb=9b3611f8b650edf4183169a9c2c4317e13be536d

diff --git a/src/auto/eval.ml b/src/auto/eval.ml
index cc9ed71..71adf56 100644
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 18:54:08 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-14 11:12:24 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -77,37 +77,37 @@ module Make (T : Tree.Sig.S) :
     loop phi
 
   let eval_trans cache ltrs node_info fcs nss ps ss =
-    let i = (ltrs.Ata.TransList.id :> int)
-    and j = (node_info.NodeInfo.id :> int)
+    let j = (node_info.NodeInfo.id :> int)
     and k = (fcs.StateSet.id :> int)
     and l = (nss.StateSet.id :> int)
-    and m = (ps.StateSet.id :> int)
+    and m = (ps.StateSet.id :> int) in
+  let rec loop ltrs ss =
+    let i = (ltrs.Ata.TransList.id :> int)
     and n = (ss.StateSet.id :> int) in
-    let res = Cache.N6.find cache i j k l m n in
-    if res == Cache.N6.dummy cache then
-      let res =
-        Ata.TransList.fold (fun trs (acct, accs) ->
-          let q, _, phi = Ata.Transition.node trs in
-          if StateSet.mem q accs then (acct, accs) else
-            if eval_form phi node_info fcs nss ps accs then
-              (acct, StateSet.add q accs)
-            else
-              (Ata.TransList.cons trs acct, accs)
-        ) ltrs (Ata.TransList.nil, ss)
-      in
-      Cache.N6.add cache i j k l m n res; res
-    else
-      res
+    let (new_ltrs, new_ss) as res =
+      let res = Cache.N6.find cache i j k l m n in
+      if res == Cache.N6.dummy cache then
+        let res =
+          Ata.TransList.fold (fun trs (acct, accs) ->
+            let q, _, phi = Ata.Transition.node trs in
+            if StateSet.mem q accs then (acct, accs) else
+              if eval_form phi node_info fcs nss ps accs then
+                (acct, StateSet.add q accs)
+              else
+                (Ata.TransList.cons trs acct, accs)
+          ) ltrs (Ata.TransList.nil, ss)
+        in
+        Cache.N6.add cache i j k l m n res; res
+      else
+        res
+    in
+    if new_ss == ss then res else
+      loop new_ltrs new_ss
+  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
@@ -120,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
@@ -177,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