fix a bug: attributes were considered as nodes -> using first_child_x

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index af23b8c..fff387a 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -43,7 +43,7 @@ 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
+    let tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     let fnode,nnode =                            (* their preorders *)
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
@@ -78,7 +78,7 @@ let rec bu_over_max asta run tree tnode =
   then
     ()
   else
-    let tfnode = Tree.first_child tree tnode
+    let tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     begin
       bu_over_max asta run tree tfnode;
@@ -120,7 +120,7 @@ let rec tp_max asta run tree tnode =
     ()
   else
     let node = Tree.preorder tree tnode
-    and tfnode = Tree.first_child tree tnode
+    and tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     let (fnode,nnode) =
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
@@ -141,19 +141,18 @@ let rec tp_max asta run tree tnode =
         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 comp_acc_self set flag =
+       () (* given a current set of states we add
+             states from self transitions which satisfy the two conditions *)
+      (* With result (below) we have all valid transitions at step 0
+      we compute the self states which occur in it and which are not in cthe current state.
+      For each of these states we compute the transitions with the correct label and state
+      we infer each of these transitions: true -> add self states occuring in it
+         to the acc and to the current set + add left and right states as result do *)
+      (* ----> With a FIFO *)
+      and fix_point selfq_i =
+        () in
+      NodeHash.replace run node (set_node, set_nr);
       
       let rec result = function
         | [] -> []
@@ -176,10 +175,10 @@ let rec tp_max asta run tree tnode =
       and qnq,qnr = try NodeHash.find run nnode
         with | _ -> map_leaf asta in
       begin
-        if tfnode == Tree.nil
+        if tfnode == Tree.nil || Tree.is_attribute tree tnode
         then ()
         else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
-        if tnnode == Tree.nil
+        if tnnode == Tree.nil || Tree.is_attribute tree tnode
         then ()
         else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
         (* indeed we delete all states from self transitions!  *)
@@ -208,7 +207,7 @@ let selected_nodes tree asta =
   NodeHash.fold
     (fun key set acc ->
       if not(StateSet.is_empty
-               (StateSet.inter (fst set) (Asta.selec_states asta)))        
+               (StateSet.inter (fst set) (Asta.selec_states asta)))
       then key :: acc
       else acc)
     run []