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 83fa0e0..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,20 +13,94 @@
 (*                                                                     *)
 (***********************************************************************)
 
-
-(* Il faut tout paramétrer par tr!!!! je ne sais pas comment faire >< **)
-
 module Node  =
 struct
-  type t = Tree.node
-  let tr = Tree.load_xml_string "<a></a>"
-  let compare n1 n2 = (Tree.preorder tr n2) - (Tree.preorder tr n1)
+  type t = int
+  let hash n = n
+  let compare n1 n2 = n1 - n2
+  let equal n1 n2 = n1 = n2
 end
   
-module NodeMap = Map.Make (Node)
+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 =
+  ()
 
-type t = StateSet.t NodeMap.t
+(* Build the maximal run *)
+let rec tp_max asta run tree node =
+  ()
 
-let compute tree asta = NodeMap.empty
+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 fmt run =
+  let print_d_set fmt (s_1,s_2) = 
+    Format.fprintf fmt "@[<hov 0>(%a,@ %a)@]"
+      StateSet.print s_1 StateSet.print s_2 in
+  let print_map fmt run = 
+    let pp = Format.fprintf fmt in
+    if NodeHash.length run = 0
+    then Format.fprintf fmt "ø"
+    else
+      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 "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
+      print_map run
+  in
+  Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run