Add counter for the tree hash-cons level 0.

diff --git a/src/run.ml b/src/run.ml
index 39eec26..6b38203 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -42,6 +42,12 @@ module HashRun = Hashtbl.Make(Run_fixpoint)
 (* Mapped sets for leaves *)
 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
 
+let num_call_oracle_fixpoint = ref 0
+let num_miss_oracle_fixpoint = ref 0
+let () = at_exit(fun () -> Format.fprintf Format.err_formatter
+  "Num: call %d, Num Miss: %d\n%!" (!num_call_oracle_fixpoint)
+  (!num_miss_oracle_fixpoint))
+
 (* Build the Oracle *)
 let rec bu_oracle asta run tree tnode hashOracle hashEval =
   let node = Tree.preorder tree tnode in
@@ -70,8 +76,10 @@ let rec bu_oracle asta run tree tnode hashOracle hashEval =
           else result set qfr qnr 0 tl in
       (* compute the fixed point of states of node *)
       let rec fix_point set_i qfr qnr list_tr t =
+        incr num_call_oracle_fixpoint;
         try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
         with _ -> 
+          incr num_miss_oracle_fixpoint;
           let set,flag = result set_i qfr qnr 0 list_tr in
           HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
           if flag = 0
@@ -87,6 +95,13 @@ let rec bu_oracle asta run tree tnode hashOracle hashEval =
                             fix_point StateSet.empty qfr qnr list_tr lab)
     end
 
+let num_call_over_max_fixpoint = ref 0
+let num_miss_over_max_fixpoint = ref 0
+let () = at_exit(fun () -> Format.fprintf Format.err_formatter
+  "Num: call %d, Num Miss: %d\n%!" (!num_call_over_max_fixpoint)
+  (!num_miss_over_max_fixpoint))
+
+
 (* Build the over-approx. of the maximal run *)
 let rec bu_over_max asta run tree tnode hashOver hashInfer =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
@@ -118,8 +133,11 @@ let rec bu_over_max asta run tree tnode hashOver hashInfer =
           then result (StateSet.add q set) qf qn 1 list_tr tl
           else result set qf qn 0 list_tr tl in
       let result_set () =
+        incr num_call_over_max_fixpoint;
         try HashRun.find hashOver ((StateSet.empty,resultr),qf,qn,list_tr,lab)
-        with _ -> let res = result StateSet.empty qf qn 0 list_tr list_tr in
+        with _ ->
+          incr num_miss_over_max_fixpoint;
+          let res = result StateSet.empty qf qn 0 list_tr list_tr in
                   HashRun.add hashOver
                     ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
                   res in
@@ -127,6 +145,12 @@ let rec bu_over_max asta run tree tnode hashOver hashInfer =
       NodeHash.replace run node (result_set(), resultr)
     end
 
+let num_call_tp_max_fixpoint = ref 0
+let num_miss_tp_max_fixpoint = ref 0
+let () = at_exit(fun () -> Format.fprintf Format.err_formatter
+  "Num: call %d, Num Miss: %d\n%!" (!num_call_tp_max_fixpoint)
+  (!num_miss_tp_max_fixpoint))
+
 
 (* Build the maximal run *)
 let rec tp_max asta run tree tnode hashMax hashInfer =
@@ -199,10 +223,13 @@ let rec tp_max asta run tree tnode hashMax hashInfer =
           then form :: (result self qf qn tl)
           else result self qf qn tl in      
       let list_form =
+        incr num_call_tp_max_fixpoint;
         try HashRun.find hashMax ((self_q,self_r),qf,qn,list_tr,lab) 
-        with _ -> let res = result (self_q,self_r) qf qn list_tr in
-                  HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
-                  res in
+        with _ ->
+          incr num_miss_tp_max_fixpoint;
+          let res = result (self_q,self_r) qf qn list_tr in
+          HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
+          res in
       (* compute states occuring in transition candidates *)
       let rec add_st (ql,qr) = function
         | [] -> ql,qr