X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=d88352b98103973b69b49710565fa7b794ae33b3;hp=d6ca22d8247df119e99ac0f316885ed7058f596a;hb=c1b43e1dcdb3d0960dbc50db9f226d68ad30c16e;hpb=43df500d1441955e3bc932be2e76318f759f7295

diff --git a/src/run.ml b/src/run.ml
index d6ca22d..d88352b 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -27,6 +27,10 @@ type t = (StateSet.t*StateSet.t) NodeHash.t
 (** Map from node to query and recognizing states *)
 (* Note that we do not consider the nil nodes *)
 
+exception Oracle_fail
+exception Over_max_fail
+exception Max_fail
+
 (* Build the Oracle *)
 let rec bu_oracle asta run tree tnode =
   let init_set node =
@@ -40,10 +44,31 @@ let rec bu_oracle asta run tree tnode =
       init_set node
     else ()
   else
+    let tfnode = Tree.first_child tree tnode
+    and tnnode = Tree.next_sibling tree tnode in
     begin
-      bu_oracle asta run tree (Tree.first_child tree tnode);
-      bu_oracle asta run tree (Tree.next_sibling tree tnode);
-      ();
+      bu_oracle asta run tree tfnode;
+      bu_oracle asta run tree tnnode;
+      let (fnode,nnode) =
+        (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
+      let q_rec n =
+        try NodeHash.find run n
+        with Not_found -> (StateSet.empty,StateSet.empty) in
+      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 reco. *)
+      let result_set = ref StateSet.empty in
+      let rec result = function
+        | [] -> ()
+        | (q,form) :: tl ->
+          if Formula.eval_form (qf,qn) form
+          then begin
+            result_set := (StateSet.add q (!result_set));
+            result tl; end
+          else result tl in
+      result list_tr;
+      NodeHash.add run node (StateSet.empty, !result_set)
+    (* Do not remove elt in Hahs (the old one would appear) *)
     end
 
 (* Build the over-approx. of the maximal run *)