X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Frun.ml;h=5d6580ab7b93abce211a49a0ea9a3bf25ca68610;hb=d4e704decf927be044d72a6fe4314aea3c8125a5;hp=fed18f00e08e7b289644b650f73ef7871a670cea;hpb=48457c0a99124a16ab29d7b84bcca85e0f3185a4;p=tatoo.git

diff --git a/src/run.ml b/src/run.ml
index fed18f0..5d6580a 100644
--- 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
@@ -165,7 +165,7 @@ let rec tp_max asta run tree tnode =
       (* compute states occuring in transition candidates *)
       let rec add_st (ql,qr) = function
         | [] -> ql,qr
-        | f :: tl -> let sql,sqr = Formula.st f in
+        | f :: tl -> let sqs,sql,sqr = Formula.st f in
                      let ql' = StateSet.union sql ql
                      and qr' = StateSet.union sqr qr in
                      add_st (ql',qr') tl in
@@ -175,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!  *)
@@ -207,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 []