10 (* Transitions of the Alternating automaton *)
11 trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
12 marking_states : StateSet.t;
13 topdown_marking_states : StateSet.t;
14 bottom_states : StateSet.t;
15 true_states : StateSet.t;
25 Topdown marking states: %a
28 Alternating transitions\n"
30 StateSet.print a.states
32 StateSet.print a.marking_states
33 StateSet.print a.topdown_marking_states
34 StateSet.print a.bottom_states
35 StateSet.print a.true_states;
39 List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
41 let sorted_trs = List.stable_sort Transition.compare trs in
42 let strings = Transition.format_list sorted_trs in
46 let sline = Pretty.line (Pretty.length line) in
47 fprintf ppf "%s\n%!" sline;
48 List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
49 fprintf ppf "%s\n%!" sline
54 | JUMP_ONE of Ptset.Int.t
55 | JUMP_MANY of Ptset.Int.t
56 | CAPTURE_MANY of Ptset.Int.t
58 let print_kind fmt k =
61 | NIL -> fprintf fmt "NIL"
62 | STAR -> fprintf fmt "STAR"
63 | NODE -> fprintf fmt "NODE"
64 | JUMP_ONE(t) -> let t = TagSet.inj_positive t in
65 fprintf fmt "JUMP_ONE(%a)" TagSet.print t
66 | JUMP_MANY(t) -> let t = TagSet.inj_positive t in
67 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
69 let t = TagSet.inj_positive t in
70 fprintf fmt "JUMP_MANY(%a)" TagSet.print t
73 let compute_jump auto tree states l marking =
74 let rel_trans, skip_trans =
76 (fun (acc_rel, acc_skip) ((ts, (l,r,m)) as tr) ->
78 ((l == states && r == states)
79 || (l == StateSet.empty && states == r)
80 || (l == states && r = StateSet.empty)
81 || (l == StateSet.empty && r = StateSet.empty))
82 then (acc_rel, tr::acc_skip)
83 else (tr::acc_rel, acc_skip))
86 let rel_labels = List.fold_left
88 Ptset.Int.union (TagSet.positive ts) acc)
92 if Ptset.Int.is_empty rel_labels then NIL
95 [ (_, (l, r, _) ) ] when l == r && l == states ->
99 when (rel_labels == (Tree.element_tags tree) ||
100 Ptset.Int.is_singleton rel_labels)
101 && (StateSet.diff l auto.true_states) == states && m
102 -> CAPTURE_MANY(rel_labels)
104 JUMP_MANY(rel_labels)
106 | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
107 | _ -> if Ptset.Int.mem Tag.pcdata rel_labels then
108 let () = D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!" TagSet.print (TagSet.inj_positive rel_labels)) in NODE else STAR
110 module Cache = Hashtbl.Make(StateSet)
111 let cache = Cache.create 1023
112 let init () = Cache.clear cache
114 let by_labels (tags1,(_,_,m1)) (tags2,(_,_,m2)) =
115 let r = TagSet.compare tags1 tags2 in r
117 if r == 0 then compare m1 m2 else r
119 let by_states (_,(l1,r1, m1)) (_, (l2,r2,m2)) =
120 let r = StateSet.compare l1 l2 in
122 let r' = StateSet.compare r1 r2 in
123 if r' == 0 then compare m1 m2
127 let merge_states (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
128 if tags1 == tags2 then (tags1,(StateSet.union l1 l2, StateSet.union r1 r2, m1 || m2))
131 let merge_labels (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
132 if (l1 == l2) && (r1 == r2) && (m1 == m2) then (TagSet.cup tags1 tags2),(l1,r1,m1)
135 let rec merge_trans comp f l =
139 if comp tr1 tr2 == 0 then merge_trans comp f ((f tr1 tr2)::ll)
140 else tr1 :: (merge_trans comp f (tr2::ll))
143 let top_down_approx auto states tree =
145 Cache.find cache states
152 (fun q acc -> List.fold_left
153 (fun acc_tr (ts, tr) ->
156 then Tree.element_tags tree
157 else if ts == TagSet.any then Tree.node_tags tree
158 else TagSet.positive ts
160 let _, _, m, f = Transition.node tr in
161 let (_, _, ls), (_, _, rs) = Formula.st f in
162 if Ptset.Int.is_empty pos then acc_tr else
163 (TagSet.inj_positive pos,(ls, rs, m))::acc_tr
166 (Hashtbl.find auto.trans q)
171 (* all labels in the tree compute what transition would be taken *)
173 Ptset.Int.fold (fun tag acc ->
174 List.fold_left (fun acc' (ts, lhs) ->
175 if TagSet.mem tag ts then
176 (TagSet.singleton tag, lhs)::acc'
178 (Tree.node_tags tree) []
180 (* now merge together states that have common labels *)
181 let uniq_states_trs =
182 merge_trans by_labels merge_states (List.sort by_labels all_trs)
184 (* now merge together labels that have common states *)
186 merge_trans by_states merge_labels (List.sort by_states uniq_states_trs)
189 let is_pairwise_disjoint l =
190 List.for_all (fun ((ts, _) as tr) ->
191 List.for_all (fun ((ts', _) as tr') ->
192 (ts == ts' && (by_states tr tr' == 0)) ||
193 TagSet.is_empty (TagSet.cap ts ts')) l) l
195 let is_complete l = TagSet.positive
196 (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts) TagSet.empty l)
198 (Tree.node_tags tree)
200 eprintf "Top-down approximation (%b, %b):\n%!"
201 (is_pairwise_disjoint td_approx)
202 (is_complete td_approx);
203 List.iter (fun (ts,(l,r, m)) ->
204 let ts = if TagSet.cardinal ts >10
205 then TagSet.diff TagSet.any
207 (TagSet.inj_positive (Tree.node_tags tree))
211 eprintf "%a, %a, %b -> %a, %a\n%!"
212 StateSet.print states
222 compute_jump auto tree states td_approx (List.exists (fun (_,(_,_,b)) -> b) td_approx)
227 Cache.add cache states jump; jump