X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=482a7494d50c6afea8816885ace254e2f45255b1;hp=8a7e066ef5292a2fb60360109276b707316a5f1d;hb=09cd270a1d9d1405795aa3d220267bc3141dd0bd;hpb=83c90cb5eeebfffa05d0383430eb80e7905b46a0 diff --git a/src/run.ml b/src/run.ml index 8a7e066..482a749 100644 --- a/src/run.ml +++ b/src/run.ml @@ -32,8 +32,7 @@ exception Over_max_fail exception Max_fail (* Mapped sets for leaves *) -let map_leaf asta = (Asta.bot_states asta, StateSet.empty) -let empty = (StateSet.empty,StateSet.empty) +let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty) (* Build the Oracle *) let rec bu_oracle asta run tree tnode = @@ -46,21 +45,21 @@ let rec bu_oracle asta run tree tnode = else let tfnode = Tree.first_child tree tnode (* first child *) and tnnode = Tree.next_sibling tree tnode in (* next-sibling *) - let fnode,nnode = + let fnode,nnode = (* their preorders *) (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in begin bu_oracle asta run tree tfnode; bu_oracle asta run tree tnnode; - let q_rec n = + let q_rec n = (* compute the set for child/sibling *) try NodeHash.find run n with Not_found -> map_leaf asta in let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *) and lab = Tree.tag tree tnode in - let _,list_tr = Asta.transitions_lab asta lab in (* only take reco. *) + let _,list_tr = Asta.transitions_lab asta lab in (* only reco. tran.*) let rec result set = function | [] -> set | (q,form) :: tl -> - if Formula.eval_form (qfr,qnr) form + if Formula.eval_form (qfr,qnr) form (* evaluates the formula *) then result (StateSet.add q set) tl else result set tl in let result_set = result StateSet.empty list_tr in @@ -90,14 +89,14 @@ let rec bu_over_max asta run tree tnode = let rec result set = function | [] -> set | (q,form) :: tl -> - if Formula.infer_form (qfq,qnq) (qfr,qnr) form + if Formula.infer_form (qfq,qnq) (qfr,qnr) form (* infers the formula*) then result (StateSet.add q set) tl else result set tl in let _,resultr = try NodeHash.find run node with _ -> raise Over_max_fail in let result_set = result StateSet.empty list_tr in + (* we keep the old recognizing states set *) NodeHash.replace run node (result_set, resultr) - (* Never remove elt in Hash (the old one would appear) *) end @@ -112,46 +111,56 @@ let rec tp_max asta run tree tnode = and tnnode = Tree.next_sibling tree tnode in let (fnode,nnode) = (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in - let q_rec n = - try NodeHash.find run n - with Not_found -> (Asta.bot_states asta,StateSet.empty) in - let (qf),(qn) = q_rec fnode,q_rec nnode in - let lab = Tree.tag tree tnode in - let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *) - let set_node,_ = try NodeHash.find run node - with _ -> raise Max_fail in - let rec result = function - | [] -> [] - | (q,form) :: tl -> - if (Formula.infer_form qf qn form) && (StateSet.mem q set_node) - then form :: (result tl) - else result tl in - let list_form = result list_tr in - let rec add_st (ql,qr) = function - | [] -> ql,qr - | f :: tl -> let sql,sqr = Formula.st f in - let ql' = StateSet.union sql ql - and qr' = StateSet.union sqr qr in - add_st (ql',qr') tl in - let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in - let qfq,qfr = try NodeHash.find run fnode - with | _ -> map_leaf asta - and qnq,qnr = try NodeHash.find run nnode - with | _ -> map_leaf asta in begin - if Tree.is_leaf tree tfnode - then () - else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr); - if Tree.is_leaf tree tnnode - then () - else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr); - tp_max asta run tree tfnode; - tp_max asta run tree tnnode; + if tnode == Tree.root tree (* we must intersect with top states *) + then let setq,_ = try NodeHash.find run node + with _ -> raise Max_fail in + NodeHash.replace run node + ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty) + else (); + let q_rec n = + try NodeHash.find run n + with Not_found -> map_leaf asta in + let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in + let lab = Tree.tag tree tnode in + let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *) + let set_node,_ = try NodeHash.find run node + with _ -> raise Max_fail in + let rec result = function + | [] -> [] + | (q,form) :: tl -> + if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) && + (StateSet.mem q set_node) (* infers & trans. can start here *) + then form :: (result tl) + else result tl in + let list_form = result list_tr in (* tran. candidates *) + (* compute states occuring in transition candidates *) + let rec add_st (ql,qr) = function + | [] -> ql,qr + | f :: tl -> let sql,sqr = Formula.st f in + let ql' = StateSet.union sql ql + and qr' = StateSet.union sqr qr in + add_st (ql',qr') tl in + let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in + let qfq,qfr = try NodeHash.find run fnode + with | _ -> map_leaf asta + and qnq,qnr = try NodeHash.find run nnode + with | _ -> map_leaf asta in + begin + if tfnode == Tree.nil + then () + else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr); + if tnnode == Tree.nil + then () + else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr); + tp_max asta run tree tfnode; + tp_max asta run tree tnnode; + end; end - + let compute tree asta = let flag = 2 in (* debug *) - let size_tree = 10000 in (* todo *) + let size_tree = 10000 in (* todo (Tree.size ?) *) let map = NodeHash.create size_tree in bu_oracle asta map tree (Tree.root tree); if flag > 0 then begin