From: Lucca Hirschi Date: Tue, 3 Jul 2012 14:04:20 +0000 (+0200) Subject: Found two bugs by rewriting the compilation in the thesis. X-Git-Tag: Core~12 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=eb490bfac81cf551554f996a3e1de1993c291acd Found two bugs by rewriting the compilation in the thesis. + minor --- diff --git a/src/asta.ml b/src/asta.ml index dc7b88d..56bb8da 100644 --- a/src/asta.ml +++ b/src/asta.ml @@ -122,7 +122,7 @@ let print fmt asta = StateSet.print asta.selec; pp "@[# Bottom states: %a@ @]" StateSet.print asta.bottom; - pp "@[# Tom states: %a@ @]" + pp "@[# Top states: %a@ @]" StateSet.print asta.top; let print_list_tr fmt z= if SetT.is_empty z diff --git a/src/compil.ml b/src/compil.ml index f505229..94d321f 100644 --- a/src/compil.ml +++ b/src/compil.ml @@ -22,15 +22,17 @@ exception Not_core_XPath let pr_er = Format.err_formatter let trans query = - let asta = Asta.empty in (* Buidling of the ASTA step by step with a special case for the last step. Then add a top most state. Each function modifies asta. *) - let rec trans = function (* builds asta from the bottom of the query *) + let asta = Asta.empty in + (* builds asta from the bottom of the query *) + let rec trans = function | [s] -> trans_last s | s :: tl -> trans tl; trans_step s | [] -> () - and trans_init () = (* add THE top most state *) + (* 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)) @@ -39,9 +41,11 @@ let trans query = Asta.add_quer asta top_st; Asta.init_top asta; 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 - and trans_last (ax,test,pred) = (* a selecting state is needed *) + (* A selecting state is needed *) + and trans_last (ax,test,pred) = let fo_p = trans_pr pred in let q,q' = Asta.new_state(), Asta.new_state() in Asta.add_selec asta q'; @@ -49,15 +53,15 @@ let trans query = Asta.add_quer asta q'; Asta.add_top asta q; Asta.add_top asta q'; - Asta.add_bot asta q; - Asta.add_bot asta q'; + Asta.add_bot asta q; (* q' \notin B !! *) let Simple lab = test in let tr_selec = (q', lab, fo_p) 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 - and trans_step (ax,test,pred) = (* add a new state for the step *) + (* Add a new state and its transitions for the step *) + and trans_step (ax,test,pred) = let fo_p = trans_pr pred and q = Asta.new_state() in let Simple label = test @@ -74,8 +78,9 @@ let trans query = Asta.init_top asta; Asta.add_top asta q - and trans_pr = function (* either we apply De Morgan rules - in xPath.parse or here *) + (* Translating of predicates. Either we apply De Morgan rules + in xPath.parse or here *) + and trans_pr = function | Expr True -> Formula.true_ | Expr False -> Formula.false_ | Or (p_1,p_2) -> trans_pr(p_1) +| trans_pr(p_2) @@ -83,9 +88,9 @@ 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 - - and trans_pr_path posi = function (* builds asta for predicate and gives - the formula which must be satsified *) + + (* 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_ | Relative steps -> List.fold_left (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc) @@ -93,14 +98,15 @@ let trans query = | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath | Absolute steps as x -> print pr_er x; raise Not_core_XPath - and trans_pr_step_l = function (* builds asta for a predicate query *) + (* Builds asta for a predicate query and give the formula *) + and trans_pr_step_l = function | [step] -> trans_pr_step [] step | step :: tl -> let list_top = trans_pr_step_l tl in trans_pr_step list_top step | [] -> failwith "Can not happened! 1" - and trans_pr_step list (ax,test,pred) = (* add a step on the top of - list in a predicate *) + (* Add a step on the top of a list of states in a predicate *) + and trans_pr_step list (ax,test,pred) = let form_next = if list = [] then trans_pr pred @@ -114,21 +120,23 @@ let trans query = Asta.add_reco asta q; Asta.add_tr asta tr_next false; Asta.add_tr asta tr_propa false; - [q] (* always one element here, but not with self - axis*) - - and form_propa q = function (* gives the propagation formula *) + [q] (* always one element here, but more with self + axis *) + (* Gives the propagation formula *) + and form_propa q = function | Child -> `Right *+ q | Descendant -> (`Left *+ q +| `Right *+ q) | x -> print_axis pr_er x; raise Not_core_XPath - and form_propa_selec q q' = function (* the same with a selecting state *) + (* The same with a selecting state *) + and form_propa_selec q q' = function | Child -> `Right *+ q +| `Right *+ q' | Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q') | x -> print_axis pr_er x; raise Not_core_XPath in - match query with (* match the top-level query *) + (* Match the top-level query *) + match query with | Absolute steps -> trans steps; trans_init(); asta | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath | Relative steps as x -> print pr_er x; raise Not_core_XPath diff --git a/tests/results/my.result b/tests/results/my.result index 227e738..57e54c1 100644 --- a/tests/results/my.result +++ b/tests/results/my.result @@ -17,8 +17,8 @@ Parse query OK ! Parse Tree OK ! Compil OK ! Run OK ! # Query states: { q₁ q₂ q₈ q₉ } # Recognizing states: { q₀ q₃ q₄ q₅ q₆ q₇ } # Selecting states: { q₁ } - # Bottom states: { q₁ q₂ q₈ } - # Tom states: { q₉ } + # Bottom states: { q₂ q₈ q₉ } + # Top states: { q₉ } # Queries transitions: | q₁ ----F(b)---> ↓₁q₀ | q₂ ----Cof(ø)---> ↓₁q₂ ∨ ↓₂q₂ ∨ ↓₁q₁ ∨ ↓₂q₁