structure of Run.compute + pretty-printing (run+tree with preorder)

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 57e037d..bd85dd4 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -23,14 +23,43 @@ 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 *)
+
+(* 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
+    begin
+      bu_oracle asta run tree (Tree.first_child tree tnode);
+      bu_oracle asta run tree (Tree.next_sibling tree tnode);
+      ();
+    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)@]"
@@ -40,11 +69,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