(* Hash Consign modules *)
-
-module type Oracle_fixpoint =
-sig
- type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
- val equal : t -> t -> bool
- val hash : t -> int
-end
-
-type dStateS = StateSet.t*StateSet.t
-module type Run_fixpoint =
-sig
- type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
- val equal : t -> t -> bool
- val hash : t -> int
-end
-
-module Oracle_fixpoint : Oracle_fixpoint = struct
- type t =
- StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
- let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
- StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
- let hash (s,l,r,list,t) =
- HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
-end
-
-let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
-let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
-module Run_fixpoint : Run_fixpoint = struct
- type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
- let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
- dequal l l' && dequal r r' && QName.equal t t'
- let hash (s,l,r,list,t) =
- HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
-end
-
+open Hconsed_run
module HashOracle = Hashtbl.Make(Oracle_fixpoint)
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
+ "For bu_oracle: call %d, miss: %d\n%!" (!num_call_oracle_fixpoint)
+ (!num_miss_oracle_fixpoint))
+
(* Build the Oracle *)
-let rec bu_oracle asta run tree tnode hashOracle=
+let rec bu_oracle asta run tree tnode hashOracle hashEval =
let node = Tree.preorder tree tnode in
if Tree.is_leaf tree tnode
then
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
begin
- bu_oracle asta run tree tfnode hashOracle;
- bu_oracle asta run tree tnnode hashOracle;
+ bu_oracle asta run tree tfnode hashOracle hashEval;
+ bu_oracle asta run tree tnnode hashOracle hashEval;
(* add states which satisfy a transition *)
let rec result set qfr qnr flag = function
| [] -> set,flag
| (q,form) :: tl ->
- if Formula.eval_form (set,qfr,qnr) form (* evaluates the formula*)
+ if Formula.eval_form (set,qfr,qnr) form hashEval
then
if StateSet.mem q set
then result set qfr qnr 0 tl
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);
+ HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
if flag = 0
then set
else fix_point set qfr qnr list_tr t in
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
+ "For bu_over_max: call %d, 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 hashRun =
+let rec bu_over_max asta run tree tnode hashOver hashInfer =
if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
then
()
let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
begin
- bu_over_max asta run tree tfnode hashRun;
- bu_over_max asta run tree tnnode hashRun;
+ bu_over_max asta run tree tfnode hashOver hashInfer;
+ bu_over_max asta run tree tnnode hashOver hashInfer;
let (fnode,nnode) =
(Tree.preorder tree tfnode, Tree.preorder tree tnnode)
and node = Tree.preorder tree tnode in
let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
and _,resultr = try NodeHash.find run node
with _ -> raise Over_max_fail in
- let rec result set flag = function
- | [] -> if flag = 0 then set else result set 0 list_tr
+ let rec result set qf qn flag list_tr = function
+ | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
| (q,form) :: tl ->
if StateSet.mem q set
- then result set 0 tl
- else if Formula.infer_form (set,resultr) qf qn form
- then result (StateSet.add q set) 1 tl
- else result set 0 tl in
- let result_set = result StateSet.empty 0 list_tr in
+ then result set qf qn 0 list_tr tl
+ else if Formula.infer_form (set,resultr) qf qn form 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 _ ->
+ 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
(* we keep the old recognizing states set *)
- NodeHash.replace run node (result_set, resultr)
+ 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
+ "For tp_max: call %d, 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 hashRun =
+let rec tp_max asta run tree tnode hashMax hashInfer =
if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
then
()
and result_st_q self_q queue flag = function (*for computing the fixed p*)
| [] -> flag,queue
| form :: tl ->
- if Formula.infer_form (self_q,self_r) qf qn form
+ if Formula.infer_form (self_q,self_r) qf qn form hashInfer
then begin
let q_cand,_,_ = Formula.st form in
StateSet.iter (fun x -> Queue.push x queue) q_cand;
end
else result_st_q self_q queue flag tl in
let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
- if Queue.is_empty queue
+ if Queue.is_empty queue (* todo: to be hconsigned? *)
then self_q_i
else
let q = Queue.pop queue in
let self,queue_init = result_q self_q (Queue.create()) list_tr in
let self_q = comp_acc_self self_q queue_init in
NodeHash.replace run node (self_q,self_r);
- (* From now, the correct set of states is mapped to node! *)
- let rec result = function
+ (* From now, the correct set of states is mapped to (self) node! *)
+ let rec result self qf qn = function
| [] -> []
| (q,form) :: tl ->
- if (StateSet.mem q self) && (* infers & trans. can start here *)
- (Formula.infer_form (self_q,self_r) qf qn form)
- then form :: (result tl)
- else result tl in
- let list_form = result list_tr in (* tran. candidates *)
+ if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
+ (Formula.infer_form self qf qn form 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 _ ->
+ 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
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
(* indeed we delete all states from self transitions! *)
- tp_max asta run tree tfnode hashRun;
- tp_max asta run tree tnnode hashRun;
+ tp_max asta run tree tfnode hashMax hashInfer;
+ tp_max asta run tree tnnode hashMax hashInfer;
end;
end
let size_tree = 10000 in (* todo (Tree.size ?) *)
let size_hcons_O = 1000 in (* todo size Hashtbl *)
let size_hcons_M = 1000 in (* todo size Hashtbl *)
+ let size_hcons_F = 1000 in (* todo size Hashtbl *)
let map = NodeHash.create size_tree in
let hashOracle = HashOracle.create(size_hcons_O) in
- bu_oracle asta map tree (Tree.root tree) hashOracle;
+ let hashEval = Formula.HashEval.create(size_hcons_F) in
+ let hashInfer = Formula.HashInfer.create(size_hcons_F) in
+ bu_oracle asta map tree (Tree.root tree) hashOracle hashEval;
HashOracle.clear hashOracle;
+ Formula.HashEval.clear hashEval;
if flag > 0 then begin
- let hashRun = HashRun.create(size_hcons_M) in
- bu_over_max asta map tree (Tree.root tree) hashRun;
+ let hashOver = HashRun.create(size_hcons_M) in
+ let hashMax = HashRun.create(size_hcons_M) in
+ bu_over_max asta map tree (Tree.root tree) hashOver hashInfer;
if flag = 2
then
- tp_max asta map tree (Tree.root tree) hashRun
+ tp_max asta map tree (Tree.root tree) hashMax hashInfer
else ();
- HashRun.clear hashRun;
+ HashRun.clear hashOver;
+ HashRun.clear hashMax;
end
else ();
map