From 21e8a30a098420df8cab5d91ea2ffc8bf65bc95e Mon Sep 17 00:00:00 2001 From: Lucca Hirschi Date: Thu, 12 Jul 2012 17:53:52 +0200 Subject: [PATCH] Buggy version of Run with self transitions (hard part is TP_MAX). --- run_tests | 3 ++- src/run.ml | 29 ++++++++++++++++++++++------- 2 files changed, 24 insertions(+), 8 deletions(-) diff --git a/run_tests b/run_tests index 4a26469..6ee6c55 100755 --- a/run_tests +++ b/run_tests @@ -6,4 +6,5 @@ echo "__________________________________________________________________________ echo "________________________________________________________________________________" ./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old echo "Expected answer: 43 (the b from the second big sub-tree)." -./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result \ No newline at end of file +./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result +./test.native ./tests/docs/my.xml '/descendant::b/self::b' \ No newline at end of file diff --git a/src/run.ml b/src/run.ml index 2e0cf95..af23b8c 100644 --- a/src/run.ml +++ b/src/run.ml @@ -43,8 +43,8 @@ let rec bu_oracle asta run tree tnode = then () else NodeHash.add run node (map_leaf asta) else - let tfnode = Tree.first_child tree tnode (* first child *) - and tnnode = Tree.next_sibling tree tnode in (* next-sibling *) + let tfnode = Tree.first_child tree tnode + and tnnode = Tree.next_sibling tree tnode in let fnode,nnode = (* their preorders *) (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in begin @@ -137,15 +137,29 @@ let rec tp_max asta run tree tnode = 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 self = try NodeHash.find run node + let (set_node,set_nr) as self = try NodeHash.find run node with Not_found -> raise Max_fail in + (* We must compute again accepting states from self transitions since + previous calls of tp_max may remove them *) + let rec comp_acc_self set flag = function + | [] -> set,flag + | (q,form) :: tl -> + if Formula.infer_form set qf qn form + then if StateSet.mem q set + then comp_acc_self set 0 tl + else comp_acc_self (StateSet.add q set) 1 tl + else comp_acc_self set 0 tl + and rec fix_point selfq_i = + let setq,flag = comp_acc_self selfq_i 0 list_tr in + if flag = 1 then set + else fix_point setq qf qn 0 in + NodeHash.replace run node (fix_point set_node, set_nr); + let rec result = function | [] -> [] | (q,form) :: tl -> - if (Formula.infer_form self qf qn form) && - (StateSet.mem q set_node) (* infers & trans. can start here *) + if (StateSet.mem q set_node) && (* infers & trans. can start here *) + (Formula.infer_form self qf qn form) then form :: (result tl) else result tl in let list_form = result list_tr in (* tran. candidates *) @@ -168,6 +182,7 @@ let rec tp_max asta run tree tnode = if tnnode == Tree.nil 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; tp_max asta run tree tnnode; end; -- 2.17.1