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
  27 let compute tree asta =
  28   let size_tree = 10000 in              (* todo *)
  29   let map = NodeHash.create size_tree in
  30
  31
  32   map
  33
  34 let print fmt run =
  35   let print_d_set fmt (s_1,s_2) =
  36     Format.fprintf fmt "@[<hov 0>(%a,@ %a)@]"
  37       StateSet.print s_1 StateSet.print s_2 in
  38   let print_map fmt run =
  39     let pp = Format.fprintf fmt in
  40     if NodeHash.length run = 0
  41     then Format.fprintf fmt "ø"
  42     else
  43       NodeHash.iter (fun cle set -> pp "|  %i-->%a@ " cle print_d_set set)
  44         run in
  45   let print_box fmt run =
  46     let pp = Format.fprintf fmt in
  47     pp "@[<v 0># Mapping: %a@ @]"
  48       print_map run
  49   in
  50   Format.fprintf fmt "@[<v 1>##### RUN #####@, %a@ @]@." print_box run