src/run.ml

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