1 (***********************************************************************)
5 (* Lucca Hirschi, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
26 module NodeHash = Hashtbl.Make (Node)
28 type t = (StateSet.t*StateSet.t) NodeHash.t
29 (** Map from nodes to query and recognizing states *)
30 (* Note that we do not consider nil nodes *)
33 exception Over_max_fail
37 (* Hash Consign modules *)
39 module HashOracle = Hashtbl.Make(Oracle_fixpoint)
40 module HashRun = Hashtbl.Make(Run_fixpoint)
42 (* Mapped sets for leaves *)
43 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
45 let num_call_oracle_fixpoint = ref 0
46 let num_miss_oracle_fixpoint = ref 0
47 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
48 "Num: call %d, Num Miss: %d\n%!" (!num_call_oracle_fixpoint)
49 (!num_miss_oracle_fixpoint))
51 (* Build the Oracle *)
52 let rec bu_oracle asta run tree tnode hashOracle hashEval =
53 let node = Tree.preorder tree tnode in
54 if Tree.is_leaf tree tnode
58 else NodeHash.add run node (map_leaf asta)
60 let tfnode = Tree.first_child_x tree tnode
61 and tnnode = Tree.next_sibling tree tnode in
62 let fnode,nnode = (* their preorders *)
63 (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
65 bu_oracle asta run tree tfnode hashOracle hashEval;
66 bu_oracle asta run tree tnnode hashOracle hashEval;
67 (* add states which satisfy a transition *)
68 let rec result set qfr qnr flag = function
71 if Formula.eval_form (set,qfr,qnr) form hashEval
74 then result set qfr qnr 0 tl
75 else result (StateSet.add q set) qfr qnr 1 tl
76 else result set qfr qnr 0 tl in
77 (* compute the fixed point of states of node *)
78 let rec fix_point set_i qfr qnr list_tr t =
79 incr num_call_oracle_fixpoint;
80 try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
82 incr num_miss_oracle_fixpoint;
83 let set,flag = result set_i qfr qnr 0 list_tr in
84 HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
87 else fix_point set qfr qnr list_tr t in
88 let q_rec n = (* compute the set for child/sibling *)
89 try NodeHash.find run n
90 with Not_found -> map_leaf asta in
91 let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *)
92 and lab = Tree.tag tree tnode in
93 let _,list_tr = Asta.transitions_lab asta lab in (*only reco. tran.*)
94 NodeHash.add run node (StateSet.empty,
95 fix_point StateSet.empty qfr qnr list_tr lab)
98 let num_call_over_max_fixpoint = ref 0
99 let num_miss_over_max_fixpoint = ref 0
100 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
101 "Num: call %d, Num Miss: %d\n%!" (!num_call_over_max_fixpoint)
102 (!num_miss_over_max_fixpoint))
105 (* Build the over-approx. of the maximal run *)
106 let rec bu_over_max asta run tree tnode hashOver hashInfer =
107 if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
111 let tfnode = Tree.first_child_x tree tnode
112 and tnnode = Tree.next_sibling tree tnode in
114 bu_over_max asta run tree tfnode hashOver hashInfer;
115 bu_over_max asta run tree tnnode hashOver hashInfer;
117 (Tree.preorder tree tfnode, Tree.preorder tree tnnode)
118 and node = Tree.preorder tree tnode in
120 try NodeHash.find run n
121 with Not_found -> map_leaf asta in
122 let qf,qn = q_rec fnode,q_rec nnode in
123 let lab = Tree.tag tree tnode in
124 let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
125 and _,resultr = try NodeHash.find run node
126 with _ -> raise Over_max_fail in
127 let rec result set qf qn flag list_tr = function
128 | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
130 if StateSet.mem q set
131 then result set qf qn 0 list_tr tl
132 else if Formula.infer_form (set,resultr) qf qn form hashInfer
133 then result (StateSet.add q set) qf qn 1 list_tr tl
134 else result set qf qn 0 list_tr tl in
136 incr num_call_over_max_fixpoint;
137 try HashRun.find hashOver ((StateSet.empty,resultr),qf,qn,list_tr,lab)
139 incr num_miss_over_max_fixpoint;
140 let res = result StateSet.empty qf qn 0 list_tr list_tr in
142 ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
144 (* we keep the old recognizing states set *)
145 NodeHash.replace run node (result_set(), resultr)
148 let num_call_tp_max_fixpoint = ref 0
149 let num_miss_tp_max_fixpoint = ref 0
150 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
151 "Num: call %d, Num Miss: %d\n%!" (!num_call_tp_max_fixpoint)
152 (!num_miss_tp_max_fixpoint))
155 (* Build the maximal run *)
156 let rec tp_max asta run tree tnode hashMax hashInfer =
157 if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
161 let node = Tree.preorder tree tnode
162 and tfnode = Tree.first_child_x tree tnode
163 and tnnode = Tree.next_sibling tree tnode in
165 (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
167 if tnode == Tree.root tree (* we must intersect with top states *)
168 then let setq,_ = try NodeHash.find run node
169 with _ -> raise Max_fail in
170 NodeHash.replace run node
171 ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty)
174 try NodeHash.find run n
175 with Not_found -> map_leaf asta in
176 let qf,qn = q_rec fnode,q_rec nnode in
177 let lab = Tree.tag tree tnode in
178 let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
179 let (self_q,self_r) = try NodeHash.find run node
180 with Not_found -> raise Max_fail in
182 (* We must compute again accepting states from self transitions since
183 previous calls of tp_max may remove them *)
184 let rec result_q self_q queue = function (* for initializing the queue *)
187 if (StateSet.mem q self_q)
189 let q_cand,_,_ = Formula.st form in
190 StateSet.iter (fun x -> Queue.push x queue) q_cand;
191 result_q (StateSet.add q self_q) queue tl;
193 else result_q self_q queue tl
194 and result_st_q self_q queue flag = function (*for computing the fixed p*)
197 if Formula.infer_form (self_q,self_r) qf qn form hashInfer
199 let q_cand,_,_ = Formula.st form in
200 StateSet.iter (fun x -> Queue.push x queue) q_cand;
201 result_st_q self_q queue 1 tl;
203 else result_st_q self_q queue flag tl in
204 let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
205 if Queue.is_empty queue (* todo: to be hconsigned? *)
208 let q = Queue.pop queue in
209 let list_q,_ = Asta.transitions_st_lab asta q lab in
210 let flag,queue = result_st_q self_q_i queue 0 list_q in
211 let self_q = if flag = 1 then StateSet.add q self_q_i else self_q_i in
212 comp_acc_self self_q queue in
214 let self,queue_init = result_q self_q (Queue.create()) list_tr in
215 let self_q = comp_acc_self self_q queue_init in
216 NodeHash.replace run node (self_q,self_r);
217 (* From now, the correct set of states is mapped to (self) node! *)
218 let rec result self qf qn = function
221 if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
222 (Formula.infer_form self qf qn form hashInfer)
223 then form :: (result self qf qn tl)
224 else result self qf qn tl in
226 incr num_call_tp_max_fixpoint;
227 try HashRun.find hashMax ((self_q,self_r),qf,qn,list_tr,lab)
229 incr num_miss_tp_max_fixpoint;
230 let res = result (self_q,self_r) qf qn list_tr in
231 HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
233 (* compute states occuring in transition candidates *)
234 let rec add_st (ql,qr) = function
236 | f :: tl -> let sqs,sql,sqr = Formula.st f in
237 let ql' = StateSet.union sql ql
238 and qr' = StateSet.union sqr qr in
239 add_st (ql',qr') tl in
240 let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
241 let qfq,qfr = try NodeHash.find run fnode
242 with | _ -> map_leaf asta
243 and qnq,qnr = try NodeHash.find run nnode
244 with | _ -> map_leaf asta in
246 if tfnode == Tree.nil || Tree.is_attribute tree tnode
248 else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
249 if tnnode == Tree.nil || Tree.is_attribute tree tnode
251 else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
252 (* indeed we delete all states from self transitions! *)
253 tp_max asta run tree tfnode hashMax hashInfer;
254 tp_max asta run tree tnnode hashMax hashInfer;
258 let compute tree asta =
259 let flag = 2 in (* debug *)
260 let size_tree = 10000 in (* todo (Tree.size ?) *)
261 let size_hcons_O = 1000 in (* todo size Hashtbl *)
262 let size_hcons_M = 1000 in (* todo size Hashtbl *)
263 let size_hcons_F = 1000 in (* todo size Hashtbl *)
264 let map = NodeHash.create size_tree in
265 let hashOracle = HashOracle.create(size_hcons_O) in
266 let hashEval = Formula.HashEval.create(size_hcons_F) in
267 let hashInfer = Formula.HashInfer.create(size_hcons_F) in
268 bu_oracle asta map tree (Tree.root tree) hashOracle hashEval;
269 HashOracle.clear hashOracle;
270 Formula.HashEval.clear hashEval;
271 if flag > 0 then begin
272 let hashOver = HashRun.create(size_hcons_M) in
273 let hashMax = HashRun.create(size_hcons_M) in
274 bu_over_max asta map tree (Tree.root tree) hashOver hashInfer;
277 tp_max asta map tree (Tree.root tree) hashMax hashInfer
279 HashRun.clear hashOver;
280 HashRun.clear hashMax;
285 let selected_nodes tree asta =
286 let run = compute tree asta in
289 if not(StateSet.is_empty
290 (StateSet.inter (fst set) (Asta.selec_states asta)))
296 let print_d_set fmt (s_1,s_2) =
297 Format.fprintf fmt "(%a,%a)"
298 StateSet.print s_1 StateSet.print s_2 in
299 let print_map fmt run =
300 let pp = Format.fprintf fmt in
301 if NodeHash.length run = 0
302 then Format.fprintf fmt "ø"
304 NodeHash.iter (fun cle set -> pp "| %i->%a @ " cle print_d_set set)
306 let print_box fmt run =
307 let pp = Format.fprintf fmt in
308 pp "@[<hov 0>@. # Mapping:@. @[<hov 0>%a@]@]"
311 Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run