1 (***********************************************************************)
5 (* Lucca Hirschi, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
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 *)
14 (***********************************************************************)
16 (* utils.ml-> INCLUDE "utils.ml" HASHINT2 () *)
20 type label = QNameSet.t
22 type formula = Formula.t
26 type t = state * label * formula
28 let compare (st,la,f) (st',la',f') =
29 let x_1 = State.compare st st' in
31 else let x_2 = QNameSet.compare la la' in
33 else Formula.compare f f'
37 let print fmt (st,la,f) =
38 Format.fprintf fmt "%a ----%s---> %a"
40 (QNameSet.to_string la)
47 include Set.Make(Transition)
50 type transition = Transition.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;
62 exception Not_found_transition
63 exception Transition_not_injective
65 let transition asta st lab =
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))
72 | [] -> raise Not_found_transition
73 | x::y::z -> raise Transition_not_injective
74 | [l] -> Transition.fo l
76 let transitions asta st =
77 let filter (s,l,f) = State.compare s st = 0 in
78 let rec remove_states = function
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))))
84 let transitions_lab asta lab =
85 let filter (s,l,f) = QNameSet.mem lab l in
86 let rec remove_lab = function
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))))
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
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))))
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;
110 let any_label = QNameSet.complement (QNameSet.empty)
112 let new_state () = State.make()
114 let add_tr ast tr flag =
116 then ast.trans_q <- (SetT.add tr (ast.trans_q))
117 else ast.trans_r <- (SetT.add tr (ast.trans_r))
119 let add_quer ast st = ast.quer <- (StateSet.add st (ast.quer))
121 let add_reco ast st = ast.reco <- (StateSet.add st (ast.reco))
123 let add_selec ast st = ast.selec <- (StateSet.add st (ast.selec))
125 let add_bot ast st = ast.bottom <- (StateSet.add st (ast.bottom))
127 let add_top ast st = ast.top <- (StateSet.add st (ast.top))
129 let init_top ast = ast.top <- (StateSet.empty)
131 let top_states ast = StateSet.elements ast.top
133 let top_states_s ast = ast.top
135 let bot_states_s ast = ast.bottom
137 let selec_states ast = ast.selec
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 =
154 then Format.fprintf fmt "ø"
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
165 let to_file out asta = ()