From: Lucca Hirschi Date: Thu, 5 Jul 2012 14:16:38 +0000 (+0200) Subject: Commentaries X-Git-Tag: Core^0 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=09cd270a1d9d1405795aa3d220267bc3141dd0bd Commentaries --- diff --git a/src/compil.ml b/src/compil.ml index 1ac98e2..574485e 100644 --- a/src/compil.ml +++ b/src/compil.ml @@ -30,12 +30,12 @@ let trans query = | [s] -> trans_last s | s :: tl -> trans tl; trans_step s | [] -> () - + (* Add THE top most state for top-level query (done in the end) *) and trans_init () = let top_st = Asta.new_state () in let or_top = - List.fold_left (fun acc x -> ((`Left *+ x) +| acc)) + List.fold_left (fun acc x -> ((`Left *+ x) +| acc)) (Formula.false_) (Asta.top_states asta) in Asta.add_quer asta top_st; @@ -43,7 +43,7 @@ let trans query = Asta.add_top asta top_st; Asta.add_bot asta top_st; (* for trees which are leaves *) Asta.add_tr asta (top_st, Asta.any_label, or_top) true - + (* A selecting state is needed *) and trans_last (ax,test,pred) = let fo_p = trans_pr pred in @@ -59,7 +59,7 @@ let trans query = and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in Asta.add_tr asta tr_selec true; Asta.add_tr asta tr_q true - + (* Add a new state and its transitions for the step *) and trans_step (ax,test,pred) = let fo_p = trans_pr pred @@ -67,7 +67,7 @@ let trans query = let Simple label = test and form_next = (fo_p) *& (* (\/ top_next) /\ predicat *) (List.fold_left (fun acc x -> (`Left *+ x ) +| acc) - Formula.false_ (Asta.top_states asta)) in + Formula.false_ (Asta.top_states asta)) in let tr_next = (q, label, form_next) and tr_propa = (q, Asta.any_label, form_propa q ax) in Asta.add_quer asta q; @@ -77,7 +77,7 @@ let trans query = Asta.add_tr asta tr_propa true; Asta.init_top asta; Asta.add_top asta q - + (* Translating of predicates. Either we apply De Morgan rules in xPath.parse or here *) and trans_pr = function @@ -88,7 +88,7 @@ let trans query = | Not (Expr Path q) -> (trans_pr_path false q) | Expr Path q -> (trans_pr_path true q) | x -> print_predicate pr_er x; raise Not_core_XPath - + (* Builds asta for predicate and gives the formula which must be satsified *) and trans_pr_path posi = function | Relative [] -> if posi then Formula.true_ else Formula.false_ @@ -97,7 +97,7 @@ let trans query = Formula.false_ (trans_pr_step_l steps) | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath | Absolute steps as x -> print pr_er x; raise Not_core_XPath - + (* Builds asta for a predicate query and give the formula *) and trans_pr_step_l = function | [step] -> trans_pr_step [] step diff --git a/src/formula.mli b/src/formula.mli index 6c54386..69bdb78 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -53,7 +53,7 @@ val size : t -> int (** Syntactic size of the formula *) val eval_form : (StateSet.t * StateSet.t) -> t -> bool -(** [eval_form sf,sn F] evaluates the formula [F] on [(sf,sn)] *) +(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *) val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool (** [eval_form S1 S2 F] infers S1; S2 |- F *) diff --git a/src/run.ml b/src/run.ml index 9ece6ee..482a749 100644 --- a/src/run.ml +++ b/src/run.ml @@ -33,7 +33,6 @@ exception Max_fail (* Mapped sets for leaves *) let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty) -let empty = (StateSet.empty,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 @@ -113,7 +112,7 @@ let rec tp_max asta run tree tnode = let (fnode,nnode) = (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in begin - if tnode == Tree.root tree (* we must intersectt with top states *) + 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 @@ -131,10 +130,11 @@ let rec tp_max asta run tree tnode = | [] -> [] | (q,form) :: tl -> if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) && - (StateSet.mem q set_node) + (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 + 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 @@ -160,7 +160,7 @@ let rec tp_max asta run tree tnode = 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