src/asta.ml

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