13 (* Transitions of the Alternating automaton *)
14 trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
15 marking_states : StateSet.t;
16 topdown_marking_states : StateSet.t;
17 bottom_states : StateSet.t;
18 true_states : StateSet.t
27 Topdown marking states: %a
30 Alternating transitions\n"
32 StateSet.print a.states
34 StateSet.print a.marking_states
35 StateSet.print a.topdown_marking_states
36 StateSet.print a.bottom_states
37 StateSet.print a.true_states;
41 List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
43 let sorted_trs = List.stable_sort Transition.compare trs in
44 let strings = Transition.format_list sorted_trs in
48 let sline = Pretty.line (Pretty.length line) in
49 fprintf ppf "%s\n%!" sline;
50 List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
51 fprintf ppf "%s\n%!" sline
58 | JUMP_ONE of Ptset.Int.t
59 | JUMP_MANY of Ptset.Int.t
60 | CAPTURE_MANY of Ptset.Int.t
63 let print_kind fmt k =
66 | NIL -> fprintf fmt "NIL"
67 | STAR -> fprintf fmt "STAR"
68 | NODE -> fprintf fmt "NODE"
71 let t = TagSet.inj_positive t in
72 fprintf fmt "JUMP_ONE(%a)" TagSet.print t
75 let t = TagSet.inj_positive t in
76 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
79 let t = TagSet.inj_positive t in
80 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
85 let compute_jump auto tree states l marking =
86 let rel_trans, skip_trans =
88 (fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) ->
90 ((l == states && r == states)
91 || (l == StateSet.empty && states == r)
92 || (l == states && r = StateSet.empty)
93 || (l == StateSet.empty && r = StateSet.empty))
94 then (acc_rel, tr::acc_skip)
95 else (tr::acc_rel, acc_skip))
98 let rel_labels = List.fold_left
100 Ptset.Int.union (TagSet.positive ts) acc)
104 if Ptset.Int.is_empty rel_labels then NIL
106 match skip_trans with
107 [ (_, (l, r, _) ) ] when l == r && l == states ->
110 | [ (_, (l, r, m) ) ]
111 when (rel_labels == (Tree.element_tags tree) ||
112 Ptset.Int.is_singleton rel_labels)
113 && (StateSet.diff l auto.true_states) == states && m
114 -> CAPTURE_MANY(rel_labels)
116 JUMP_MANY(rel_labels)
119 | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
122 if Ptset.Int.mem Tag.pcdata rel_labels then begin
123 TRACE("top-down-approx", 3, __ "Computed rel_labels: %a\n"
125 (TagSet.inj_positive rel_labels));
129 module Cache = Hashtbl.Make(StateSet)
130 let cache = Cache.create 1023
131 let init () = Cache.clear cache
133 let by_labels (tags1, _) (tags2, _) = TagSet.compare tags1 tags2
135 let by_states x1 x2 =
136 let l1, r1, (m1 : bool) = snd x1
137 and l2, r2, (m2 : bool) = snd x2 in
138 (* force m1/m2 to be of type bool for efficient compare *)
139 let r = StateSet.compare l1 l2 in
142 let r' = StateSet.compare r1 r2 in
146 let merge_states (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
147 if tags1 == tags2 then
148 tags1, (StateSet.union l1 l2, StateSet.union r1 r2, m1 || m2)
151 let merge_labels (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
152 if l1 == l2 && r1 == r2 && m1 == m2 then
153 (TagSet.cup tags1 tags2), (l1, r1, m1)
156 let rec merge_trans comp f l =
160 if comp tr1 tr2 == 0 then merge_trans comp f ((f tr1 tr2)::ll)
161 else tr1 :: (merge_trans comp f (tr2::ll))
163 let fold_trans_of_states auto f states acc =
166 List.fold_left f tr_acc (Hashtbl.find auto.trans q))
170 let top_down_approx auto states tree =
171 try Cache.find cache states with
174 (* Collect all (ts, (l, r, m)) where
175 ts is a tagset, l and r are left and right set of states
178 fold_trans_of_states auto
179 (fun acc_tr (ts, tr) ->
181 if ts == TagSet.star then Tree.element_tags tree
182 else if ts == TagSet.any then Tree.node_tags tree
183 else TagSet.positive ts
185 let _, _, m, f = Transition.node tr in
186 let (_, _, ls), (_, _, rs) = Formula.st f in
187 if Ptset.Int.is_empty pos then acc_tr
189 (TagSet.inj_positive pos, (ls, rs, m))::acc_tr
194 (* for all labels in the tree compute which transition is taken *)
196 Ptset.Int.fold (fun tag acc ->
197 List.fold_left (fun acc' (ts, rhs) ->
198 if TagSet.mem tag ts then
199 (TagSet.singleton tag, rhs)::acc'
201 (Tree.node_tags tree) []
203 (* merge together states that have common labels *)
204 let uniq_states_trs =
205 merge_trans by_labels merge_states (List.sort by_labels all_trs)
207 (* merge together labels that have common states *)
209 merge_trans by_states merge_labels
210 (List.sort by_states uniq_states_trs)
213 "top-down-approx", 2,
214 let is_pairwise_disjoint l =
215 List.for_all (fun ((ts, _) as tr) ->
216 List.for_all (fun ((ts', _) as tr') ->
217 (ts == ts' && (by_states tr tr' == 0)) ||
218 TagSet.is_empty (TagSet.cap ts ts')) l) l
220 let is_complete l = TagSet.positive
221 (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
224 (Tree.node_tags tree)
226 let pr_td_approx fmt td_approx =
227 List.iter (fun (ts,(l,r, m)) ->
228 let ts = if TagSet.cardinal ts >10
229 then TagSet.diff TagSet.any
231 (TagSet.inj_positive (Tree.node_tags tree))
235 fprintf fmt "\t%a, %a, %b -> %a, %a\n%!"
236 StateSet.print states
244 __ " pairwise-disjoint:%b, complete:%b:\n%a"
245 (is_pairwise_disjoint td_approx)
246 (is_complete td_approx)
247 pr_td_approx td_approx
251 auto tree states td_approx
252 (List.exists (fun (_,(_,_,b)) -> b) td_approx)
254 Cache.add cache states jump; jump