projects
/
tatoo.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
d84a929
)
Add counter for the tree hash-cons level 0.
author
Lucca Hirschi
<lucca.hirschi@gmail.com>
Wed, 18 Jul 2012 11:41:44 +0000
(13:41 +0200)
committer
Lucca Hirschi
<lucca.hirschi@gmail.com>
Wed, 18 Jul 2012 11:41:44 +0000
(13:41 +0200)
src/run.ml
patch
|
blob
|
history
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)
(* 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
(* 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 =
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 _ ->
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
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
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 *)
(* 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 () =
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)
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
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
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 =
(* 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 =
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)
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
(* compute states occuring in transition candidates *)
let rec add_st (ql,qr) = function
| [] -> ql,qr