Final test in run_test try my.query on my.xml (from thesis) + fixs in run.ml ==>...

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 8a7e066..9ece6ee 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -32,7 +32,7 @@ exception Over_max_fail
 exception Max_fail
 
 (* Mapped sets for leaves *)
-let map_leaf asta = (Asta.bot_states asta, StateSet.empty)
+let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
 let empty = (StateSet.empty,StateSet.empty)
 
 (* Build the Oracle *)
@@ -112,43 +112,52 @@ let rec tp_max asta run tree tnode =
     and tnnode = Tree.next_sibling tree tnode in
     let (fnode,nnode) =
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
-    let q_rec n =
-      try NodeHash.find run n
-      with Not_found -> (Asta.bot_states asta,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 query. *)
-    let set_node,_ = try NodeHash.find run node
-      with _ -> raise Max_fail in
-    let rec result = function
-      | [] -> []
-      | (q,form) :: tl ->
-        if (Formula.infer_form qf qn form) && (StateSet.mem q set_node)
-        then form :: (result tl)
-        else result tl in
-    let list_form = result list_tr in
-    let rec add_st (ql,qr) = function
-      | [] -> ql,qr
-      | f :: tl -> let 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
-    let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
-    let qfq,qfr = try NodeHash.find run fnode
-      with | _ -> map_leaf asta
-    and qnq,qnr = try NodeHash.find run nnode
-      with | _ -> map_leaf asta in
     begin
-      if Tree.is_leaf tree tfnode
-      then ()
-      else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
-      if Tree.is_leaf tree tnnode
-      then ()
-      else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
-      tp_max asta run tree tfnode;
-      tp_max asta run tree tnnode;
+      if tnode == Tree.root tree        (* we must intersectt with top states *)
+      then let setq,_  = try NodeHash.find run node
+        with _ -> raise Max_fail in
+           NodeHash.replace run node
+             ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty)
+      else ();
+      let q_rec n =
+        try NodeHash.find run n
+        with Not_found -> map_leaf asta in
+      let (qfq,qfr),(qnq,qnr) = 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 rec result = function
+        | [] -> []
+        | (q,form) :: tl ->
+          if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
+            (StateSet.mem q set_node)
+          then form :: (result tl)
+          else result tl in
+      let list_form = result list_tr in
+      let rec add_st (ql,qr) = function
+        | [] -> ql,qr
+        | f :: tl -> let 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
+      let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
+      let qfq,qfr = try NodeHash.find run fnode
+        with | _ -> map_leaf asta
+      and qnq,qnr = try NodeHash.find run nnode
+        with | _ -> map_leaf asta in
+      begin
+        if tfnode == Tree.nil
+        then ()
+        else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
+        if tnnode == Tree.nil
+        then ()
+        else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
+        tp_max asta run tree tfnode;
+        tp_max asta run tree tnnode;
+      end;
     end
-
+        
 let compute tree asta =
   let flag = 2 in                       (* debug  *)
   let size_tree = 10000 in              (* todo *)