12 (* Transitions of the Alternating automaton *)
13 trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
14 marking_states : StateSet.t;
15 topdown_marking_states : StateSet.t;
16 bottom_states : StateSet.t;
17 true_states : StateSet.t }
26 Topdown marking states: %a
29 Alternating transitions\n"
31 StateSet.print a.states
33 StateSet.print a.marking_states
34 StateSet.print a.topdown_marking_states
35 StateSet.print a.bottom_states
36 StateSet.print a.true_states;
40 List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
42 let sorted_trs = List.stable_sort Transition.compare trs in
43 let strings = Transition.format_list sorted_trs in
47 let sline = Pretty.line (Pretty.length line) in
48 fprintf ppf "%s\n%!" sline;
49 List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
50 fprintf ppf "%s\n%!" sline
57 | JUMP_ONE of Ptset.Int.t
58 | JUMP_MANY of Ptset.Int.t
59 | CAPTURE_MANY of Ptset.Int.t
62 let print_kind fmt k =
65 | NIL -> fprintf fmt "NIL"
66 | STAR -> fprintf fmt "STAR"
67 | NODE -> fprintf fmt "NODE"
70 let t = TagSet.inj_positive t in
71 fprintf fmt "JUMP_ONE(%a)" TagSet.print t
74 let t = TagSet.inj_positive t in
75 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
78 let t = TagSet.inj_positive t in
79 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
84 let compute_jump auto tree states l marking =
85 let rel_trans, skip_trans =
87 (fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) ->
89 ((l == states && r == states)
90 || (l == StateSet.empty && states == r)
91 || (l == states && r = StateSet.empty)
92 || (l == StateSet.empty && r = StateSet.empty))
93 then (acc_rel, tr::acc_skip)
94 else (tr::acc_rel, acc_skip))
97 let rel_labels = List.fold_left
99 Ptset.Int.union (TagSet.positive ts) acc)
103 if Ptset.Int.is_empty rel_labels then NIL
105 match skip_trans with
106 [ (_, (l, r, _) ) ] when l == r && l == states ->
109 | [ (_, (l, r, m) ) ]
110 when (rel_labels == (Tree.element_tags tree) ||
111 Ptset.Int.is_singleton rel_labels)
112 && (StateSet.diff l auto.true_states) == states && m
113 -> CAPTURE_MANY(rel_labels)
115 JUMP_MANY(rel_labels)
118 | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
121 if Ptset.Int.mem Tag.pcdata rel_labels then
123 D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!"
124 TagSet.print (TagSet.inj_positive rel_labels))
128 module Cache = Hashtbl.Make(StateSet)
129 let cache = Cache.create 1023
130 let init () = Cache.clear cache
132 let by_labels (tags1, _) (tags2, _) = TagSet.compare tags1 tags2
134 let by_states x1 x2 =
135 let l1, r1, (m1 : bool) = snd x1
136 and l2, r2, (m2 : bool) = snd x2 in
137 (* force m1/m2 to be of type bool for efficient compare *)
138 let r = StateSet.compare l1 l2 in
141 let r' = StateSet.compare r1 r2 in
145 let merge_states (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
146 if tags1 == tags2 then
147 tags1, (StateSet.union l1 l2, StateSet.union r1 r2, m1 || m2)
150 let merge_labels (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
151 if l1 == l2 && r1 == r2 && m1 == m2 then
152 (TagSet.cup tags1 tags2), (l1, r1, m1)
155 let rec merge_trans comp f l =
159 if comp tr1 tr2 == 0 then merge_trans comp f ((f tr1 tr2)::ll)
160 else tr1 :: (merge_trans comp f (tr2::ll))
162 let fold_trans_of_states auto f states acc =
165 List.fold_left f tr_acc (Hashtbl.find auto.trans q))
169 let top_down_approx auto states tree =
170 try Cache.find cache states with
173 (* Collect all (ts, (l, r, m)) where
174 ts is a tagset, l and r are left and right set of states
177 fold_trans_of_states auto
178 (fun acc_tr (ts, tr) ->
180 if ts == TagSet.star then Tree.element_tags tree
181 else if ts == TagSet.any then Tree.node_tags tree
182 else TagSet.positive ts
184 let _, _, m, f = Transition.node tr in
185 let (_, _, ls), (_, _, rs) = Formula.st f in
186 if Ptset.Int.is_empty pos then acc_tr
188 (TagSet.inj_positive pos, (ls, rs, m))::acc_tr
193 (* for all labels in the tree compute which transition is taken *)
195 Ptset.Int.fold (fun tag acc ->
196 List.fold_left (fun acc' (ts, rhs) ->
197 if TagSet.mem tag ts then
198 (TagSet.singleton tag, rhs)::acc'
200 (Tree.node_tags tree) []
202 (* merge together states that have common labels *)
203 let uniq_states_trs =
204 merge_trans by_labels merge_states (List.sort by_labels all_trs)
206 (* merge together labels that have common states *)
208 merge_trans by_states merge_labels
209 (List.sort by_states uniq_states_trs)
212 let is_pairwise_disjoint l =
213 List.for_all (fun ((ts, _) as tr) ->
214 List.for_all (fun ((ts', _) as tr') ->
215 (ts == ts' && (by_states tr tr' == 0)) ||
216 TagSet.is_empty (TagSet.cap ts ts')) l) l
218 let is_complete l = TagSet.positive
219 (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
222 (Tree.node_tags tree)
224 eprintf "Top-down approximation (%b, %b):\n%!"
225 (is_pairwise_disjoint td_approx)
226 (is_complete 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 eprintf "%a, %a, %b -> %a, %a\n%!"
236 StateSet.print states
247 auto tree states td_approx
248 (List.exists (fun (_,(_,_,b)) -> b) td_approx)
250 Cache.add cache states jump; jump