1 (***********************************************************************)
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 (***********************************************************************)
18 type label = QNameSet.t
20 type formula = Formula.t
24 type t = state * label * formula
26 let compare (st,la,f) (st',la',f') =
27 let x_1 = State.compare st st' in
29 else let x_2 = QNameSet.compare la la' in
31 else Formula.compare f f'
35 let print fmt (st,la,f) =
36 Format.fprintf fmt "%a ----%s---> %a"
38 (QNameSet.to_string la)
44 include Set.Make(Transition)
47 type transition = Transition.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;
59 exception Not_found_transition
60 exception Transition_not_injective
62 let transition asta st lab =
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))
69 | [] -> raise Not_found_transition
70 | x::y::z -> raise Transition_not_injective
71 | [l] -> Transition.fo l
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
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))))
82 quer = StateSet.empty;
83 reco = StateSet.empty;
84 selec = StateSet.empty;
85 bottom = StateSet.empty;
91 let any_label = QNameSet.complement (QNameSet.empty)
93 let new_state () = State.make()
95 let add_tr ast tr flag =
97 then ast.trans_q <- (SetT.add tr (ast.trans_q))
98 else ast.trans_r <- (SetT.add tr (ast.trans_r))
100 let add_quer ast st = ast.quer <- (StateSet.add st (ast.quer))
102 let add_reco ast st = ast.reco <- (StateSet.add st (ast.reco))
104 let add_selec ast st = ast.selec <- (StateSet.add st (ast.selec))
106 let add_bot ast st = ast.bottom <- (StateSet.add st (ast.bottom))
108 let add_top ast st = ast.top <- (StateSet.add st (ast.top))
110 let init_top ast = ast.top <- (StateSet.empty)
112 let top_states ast = StateSet.elements ast.top
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=
129 then Format.fprintf fmt "ø"
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
140 let to_file out asta = ()