src/asta.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 (* utils.ml-> INCLUDE "utils.ml" HASHINT2 () *)
  17
  18 type state = State.t
  19
  20 type label = QNameSet.t
  21
  22 type formula = Formula.t
  23
  24 module Transition =
  25 struct
  26   type t = state * label * formula
  27
  28   let compare (st,la,f) (st',la',f') =
  29     let x_1 = State.compare st st' in
  30     if x_1 != 0 then x_1
  31     else let x_2 = QNameSet.compare la la' in
  32          if x_2 != 0 then x_2
  33          else Formula.compare f f'
  34   let st (st,la,f) = st
  35   let la (st,la,f) = la
  36   let fo (st,la,f) = f
  37   let print fmt (st,la,f) =
  38     Format.fprintf fmt "%a ----%s---> %a"
  39       State.print st
  40       (QNameSet.to_string la)
  41       Formula.print f
  42
  43 end
  44
  45 module  SetT =
  46 struct
  47   include Set.Make(Transition)
  48 end
  49
  50 type transition = Transition.t
  51
  52 type t = {
  53   mutable quer : StateSet.t;
  54   mutable reco : StateSet.t;
  55   mutable selec : StateSet.t;
  56   mutable bottom : StateSet.t;
  57   mutable top : StateSet.t;
  58   mutable trans_q : SetT.t;
  59   mutable trans_r : SetT.t;
  60 }
  61
  62 exception Not_found_transition
  63 exception Transition_not_injective
  64
  65 let transition asta st lab =
  66   let filter (s,l,f) =
  67     (State.compare s st = 0) && (QNameSet.compare l lab = 0) in
  68   let tr_set = (SetT.elements (SetT.filter filter asta.trans_q)) @
  69     (SetT.elements (SetT.filter filter asta.trans_r))
  70   in
  71   match tr_set with
  72     | [] -> raise Not_found_transition
  73     | x::y::z -> raise Transition_not_injective
  74     | [l] -> Transition.fo l
  75
  76 let transitions asta st =
  77   let filter (s,l,f) = State.compare s st = 0 in
  78   let rec remove_states = function
  79     | [] -> []
  80     | (s,l,f) :: tl -> (l,f) :: (remove_states tl) in
  81   (remove_states (SetT.elements (SetT.filter filter asta.trans_q)),
  82    (remove_states (SetT.elements (SetT.filter filter asta.trans_r))))
  83
  84 let transitions_lab asta lab =
  85   let filter (s,l,f) = QNameSet.mem lab l in
  86     let rec remove_lab = function
  87       | [] -> []
  88       | (s,l,f) :: tl -> (s,f) :: (remove_lab tl) in
  89     (remove_lab (SetT.elements (SetT.filter filter asta.trans_q)),
  90      (remove_lab (SetT.elements (SetT.filter filter asta.trans_r))))
  91
  92 let transitions_st_lab asta q lab =
  93   let filter (s,l,f) = q = s && QNameSet.mem lab l in
  94     let rec remove_st_lab = function
  95       | [] -> []
  96       | (s,l,f) :: tl -> f :: (remove_st_lab tl) in
  97     (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_q)),
  98      (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_r))))
  99
 100 let empty = {
 101   quer = StateSet.empty;
 102   reco = StateSet.empty;
 103   selec = StateSet.empty;
 104   bottom = StateSet.empty;
 105   top = StateSet.empty;
 106   trans_q = SetT.empty;
 107   trans_r = SetT.empty
 108 }
 109
 110 let any_label = QNameSet.complement (QNameSet.empty)
 111
 112 let new_state () = State.make()
 113
 114 let add_tr ast tr flag =
 115   if flag
 116   then ast.trans_q <- (SetT.add tr (ast.trans_q))
 117   else ast.trans_r <- (SetT.add tr (ast.trans_r))
 118
 119 let add_quer ast st = ast.quer <- (StateSet.add st (ast.quer))
 120
 121 let add_reco ast st = ast.reco <- (StateSet.add st (ast.reco))
 122
 123 let add_selec ast st = ast.selec <- (StateSet.add st (ast.selec))
 124
 125 let add_bot ast st = ast.bottom <- (StateSet.add st (ast.bottom))
 126
 127 let add_top ast st = ast.top <- (StateSet.add st (ast.top))
 128
 129 let init_top ast  = ast.top <- (StateSet.empty)
 130
 131 let top_states ast = StateSet.elements ast.top
 132
 133 let top_states_s ast = ast.top
 134
 135 let bot_states_s ast = ast.bottom
 136
 137 let selec_states ast = ast.selec
 138
 139 let print fmt asta =
 140   let print_box fmt flag =
 141     let pp = Format.fprintf fmt in
 142     pp "@[<v 0># Query states: %a@ @]"
 143       StateSet.print asta.quer;
 144     pp "@[<v 0># Recognizing states: %a@ @]"
 145       StateSet.print asta.reco;
 146     pp "@[<v 0># Selecting states: %a@ @]"
 147       StateSet.print asta.selec;
 148     pp "@[<v 0># Bottom states: %a@ @]"
 149       StateSet.print asta.bottom;
 150     pp "@[<v 0># Top states: %a@ @]"
 151       StateSet.print asta.top;
 152     let print_list_tr fmt z =
 153       if SetT.is_empty z
 154       then Format.fprintf fmt "ø"
 155       else
 156         SetT.iter (fun x -> Format.fprintf fmt "|  %a  @ "  Transition.print x) z in
 157     let print_box_list fmt trans =
 158       Format.fprintf fmt "  @[<hov 0>%a @]" print_list_tr trans in
 159     Format.fprintf fmt "@[<v 0># Queries transitions:@ %a@ @]"
 160       print_box_list asta.trans_q;
 161     Format.fprintf fmt "@[<v 0># Recognizing transitions:@ %a@]"
 162       print_box_list asta.trans_r in
 163   Format.fprintf fmt "@[<v 1>##### ASTA #####@. %a@ @]@." print_box 0
 164
 165 let to_file out asta = ()