Buggy version of Run with self transitions (hard part is TP_MAX).

diff --git a/run_tests b/run_tests
index 4a26469..6ee6c55 100755 (executable)
--- 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 (file)
--- 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;