src/run.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                   Lucca Hirschi, LRI UMR8623                        *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 module Node  =
  17 struct
  18   type t = int
  19   let hash n = n
  20   let compare n1 n2 = n1 - n2
  21   let equal n1 n2 = n1 = n2
  22 end
  23
  24 module NodeHash = Hashtbl.Make (Node)
  25
  26 type t = (StateSet.t*StateSet.t) NodeHash.t
  27 (** Map from node to query and recognizing states *)
  28 (* Note that we do not consider the nil nodes *)
  29
  30 (* Build the Oracle *)
  31 let rec bu_oracle asta run tree tnode =
  32   let init_set node =
  33     let set = (StateSet.empty,StateSet.empty) in
  34     NodeHash.add run node set
  35   and node = Tree.preorder tree tnode in
  36   if (Tree.is_leaf tree tnode)
  37   then
  38     if not (tnode == Tree.nil)
  39     then
  40       init_set node
  41     else ()
  42   else
  43     begin
  44       bu_oracle asta run tree (Tree.first_child tree tnode);
  45       bu_oracle asta run tree (Tree.next_sibling tree tnode);
  46       ();
  47     end
  48
  49 (* Build the over-approx. of the maximal run *)
  50 let rec bu_over_max asta run tree node =
  51   ()
  52
  53 (* Build the maximal run *)
  54 let rec tp_max asta run tree node =
  55   ()
  56
  57 let compute tree asta =
  58   let size_tree = 10000 in              (* todo *)
  59   let map = NodeHash.create size_tree in
  60   bu_oracle asta map tree (Tree.root tree);
  61   bu_over_max asta map tree (Tree.root tree);
  62   tp_max asta map tree (Tree.root tree);
  63   map
  64
  65 let print fmt run =
  66   let print_d_set fmt (s_1,s_2) =
  67     Format.fprintf fmt "@[<hov 0>(%a,@ %a)@]"
  68       StateSet.print s_1 StateSet.print s_2 in
  69   let print_map fmt run =
  70     let pp = Format.fprintf fmt in
  71     if NodeHash.length run = 0
  72     then Format.fprintf fmt "ø"
  73     else
  74       NodeHash.iter (fun cle set -> pp "|  %i-->%a  @ " cle print_d_set set)
  75         run in
  76   let print_box fmt run =
  77     let pp = Format.fprintf fmt in
  78     pp "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
  79       print_map run
  80   in
  81   Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run