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 de2ba81..d88352b 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -1,7 +1,9 @@
 (***********************************************************************)
 (*                                                                     *)
-(*                  Lucca Hirschi, ?   *)
-(*                  ?   *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                   Lucca Hirschi, LRI UMR8623                        *)
+(*                   Université Paris-Sud & CNRS                       *)
 (*                                                                     *)
 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
 (*  Recherche Scientifique. All rights reserved.  This file is         *)
@@ -11,8 +13,6 @@
 (*                                                                     *)
 (***********************************************************************)
 
-INCLUDE "utils.ml"
-
 module Node  =
 struct
   type t = int
@@ -25,14 +25,68 @@ module NodeHash = Hashtbl.Make (Node)
   
 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 =
+    let set = (StateSet.empty,StateSet.empty) in
+    NodeHash.add run node set
+  and node = Tree.preorder tree tnode in
+  if (Tree.is_leaf tree tnode)
+  then
+    if not (tnode == Tree.nil)
+    then
+      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 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 *)
+let rec bu_over_max asta run tree node =
+  ()
+
+(* Build the maximal run *)
+let rec tp_max asta run tree node =
+  ()
+
 let compute tree asta =
   let size_tree = 10000 in              (* todo *)
   let map = NodeHash.create size_tree in
-  
-  
+  bu_oracle asta map tree (Tree.root tree);
+  bu_over_max asta map tree (Tree.root tree);
+  tp_max asta map tree (Tree.root tree);
   map
-    
+
 let print fmt run =
   let print_d_set fmt (s_1,s_2) = 
     Format.fprintf fmt "@[<hov 0>(%a,@ %a)@]"
@@ -42,12 +96,11 @@ let print fmt run =
     if NodeHash.length run = 0
     then Format.fprintf fmt "ø"
     else
-      NodeHash.iter (fun cle set -> pp "|  %i-->%a@ " cle print_d_set set)
+      NodeHash.iter (fun cle set -> pp "|  %i-->%a  @ " cle print_d_set set)
         run in
   let print_box fmt run =
     let pp = Format.fprintf fmt in
-    pp "@[<v 0># Mapping: %a@ @]"
+    pp "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
       print_map run
   in
-  Format.fprintf fmt "@[<v 1>##### RUN #####@, %a@ @]@." print_box run
-  
+  Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run