Full implem BU Oracle + eval_form in Formula (impossible in Asta) + transitions_lab...

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index d6ca22d..d88352b 100644 (file)
--- 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 *)