From 2efd7484edbffd870e3ef1cd68d210e4c2ae5b54 Mon Sep 17 00:00:00 2001 From: Lucca Hirschi Date: Wed, 18 Jul 2012 13:41:44 +0200 Subject: [PATCH] Add counter for the tree hash-cons level 0. --- src/run.ml | 35 +++++++++++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/src/run.ml b/src/run.ml index 39eec26..6b38203 100644 --- 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 -- 2.17.1