end;
fprintf fmt "%!"
+let pr_trans fmt (ts, (l, r, m)) =
+ Format.fprintf fmt "%a %s %a %a"
+ TagSet.print ts
+ (if m then Pretty.double_right_arrow else Pretty.right_arrow)
+ StateSet.print l
+ StateSet.print r
let compute_jump auto tree states l marking =
let rel_trans, skip_trans =
List.fold_left
(fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) ->
- if not marking &&
- ((l == states && r == states)
- || (l == StateSet.empty && states == r)
- || (l == states && r = StateSet.empty)
- || (l == StateSet.empty && r = StateSet.empty))
- then (acc_rel, tr::acc_skip)
- else (tr::acc_rel, acc_skip))
+ if not marking &&
+ ((l == states && r == states)
+ || (l == StateSet.empty && states == r)
+ || (l == states && r = StateSet.empty)
+ || (l == StateSet.empty && r = StateSet.empty))
+ then (acc_rel, tr::acc_skip)
+ else (tr::acc_rel, acc_skip))
([],[]) l
in
let rel_labels = List.fold_left
else
match skip_trans with
[ (_, (l, r, _) ) ] when l == r && l == states ->
- begin
- match rel_trans with
- | [ (_, (l, r, m) ) ]
- when (rel_labels == (Tree.element_tags tree) ||
- Ptset.Int.is_singleton rel_labels)
- && (StateSet.diff l auto.true_states) == states && m
- -> CAPTURE_MANY(rel_labels)
- | _ ->
- JUMP_MANY(rel_labels)
- end
+ begin
+ match rel_trans with
+ | [ (_, (l, r, m) ) ]
+ when (rel_labels == (Tree.element_tags tree) ||
+ Ptset.Int.is_singleton rel_labels)
+ && (StateSet.diff l auto.true_states) == states && m
+ -> CAPTURE_MANY(rel_labels)
+ | _ ->
+ JUMP_MANY(rel_labels)
+ end
| [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
| _ ->
if Ptset.Int.mem Tag.pcdata rel_labels then begin
- LOG(__ "top-down-approx" 3 "Computed rel_labels: %a@\n"
- TagSet.print (TagSet.inj_positive rel_labels));
- NODE
+ LOG(__ "top-down-approx" 3 "Computed rel_labels: %a"
+ TagSet.print (TagSet.inj_positive rel_labels));
+ LOG(__ "top-down-approx" 3 "skip_trans:@\n%a"
+ (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans)
+ skip_trans);
+ LOG(__ "top-down-approx" 3 "rel_trans:@\n%a"
+ (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans)
+ rel_trans);
+ NODE
end else STAR
module Cache = Hashtbl.Make(StateSet)
| Not_found ->
let trs =
(* Collect all (ts, (l, r, m)) where
- ts is a tagset, l and r are left and right set of states
- m is marking flag
+ ts is a tagset, l and r are left and right set of states
+ m is marking flag
*)
fold_trans_of_states auto
- (fun acc_tr (ts, tr) ->
- let pos =
- if ts == TagSet.star then Tree.element_tags tree
- else if ts == TagSet.any then Tree.node_tags tree
- else TagSet.positive ts
- in
- let _, _, m, f = Transition.node tr in
- let ls, rs = Formula.st f in
- if Ptset.Int.is_empty pos then acc_tr
- else
- (TagSet.inj_positive pos, (ls, rs, m))::acc_tr
- )
- states
- []
+ (fun acc_tr (ts, tr) ->
+ let pos =
+ if ts == TagSet.star then Tree.element_tags tree
+ else if ts == TagSet.any then Tree.node_tags tree
+ else TagSet.positive ts
+ in
+ let _, _, m, f = Transition.node tr in
+ let ls, rs = Formula.st f in
+ if Ptset.Int.is_empty pos then acc_tr
+ else
+ (TagSet.inj_positive pos, (ls, rs, m))::acc_tr
+ )
+ states
+ []
in
(* for all labels in the tree compute which transition is taken *)
let all_trs =
Ptset.Int.fold (fun tag acc ->
- List.fold_left (fun acc' (ts, rhs) ->
- if TagSet.mem tag ts then
- (TagSet.singleton tag, rhs)::acc'
- else acc') acc trs)
- (Tree.node_tags tree) []
+ List.fold_left (fun acc' (ts, rhs) ->
+ if TagSet.mem tag ts then
+ (TagSet.singleton tag, rhs)::acc'
+ else acc') acc trs)
+ (Tree.node_tags tree) []
in
(* merge together states that have common labels *)
let uniq_states_trs =
(* merge together labels that have common states *)
let td_approx =
merge_trans by_states merge_labels
- (List.sort by_states uniq_states_trs)
+ (List.sort by_states uniq_states_trs)
in
LOG(
let is_pairwise_disjoint l =
- List.for_all (fun ((ts, _) as tr) ->
- List.for_all (fun ((ts', _) as tr') ->
- (ts == ts' && (by_states tr tr' == 0)) ||
- TagSet.is_empty (TagSet.cap ts ts')) l) l
+ List.for_all (fun ((ts, _) as tr) ->
+ List.for_all (fun ((ts', _) as tr') ->
+ (ts == ts' && (by_states tr tr' == 0)) ||
+ TagSet.is_empty (TagSet.cap ts ts')) l) l
in
let is_complete l = TagSet.positive
- (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
- TagSet.empty l)
- ==
- (Tree.node_tags tree)
+ (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
+ TagSet.empty l)
+ ==
+ (Tree.node_tags tree)
in
let pr_td_approx fmt td_approx =
- List.iter (fun (ts,(l,r, m)) ->
- let ts = if TagSet.cardinal ts >10
- then TagSet.diff TagSet.any
- (TagSet.diff
- (TagSet.inj_positive (Tree.node_tags tree))
- ts)
- else ts
- in
- fprintf fmt "%a, %a, %b -> %a, %a@\n"
- StateSet.print states
- TagSet.print ts
- m
- StateSet.print l
- StateSet.print r
- ) td_approx;
- fprintf fmt "\n%!"
+ List.iter (fun (ts,(l,r, m)) ->
+ let ts = if TagSet.cardinal ts >10
+ then TagSet.diff TagSet.any
+ (TagSet.diff
+ (TagSet.inj_positive (Tree.node_tags tree))
+ ts)
+ else ts
+ in
+ fprintf fmt "%a, %a, %b -> %a, %a@\n"
+ StateSet.print states
+ TagSet.print ts
+ m
+ StateSet.print l
+ StateSet.print r
+ ) td_approx;
+ fprintf fmt "\n%!"
in
__ "top-down-approx" 2 " pairwise-disjoint:%b, complete:%b:@\n%a"
- (is_pairwise_disjoint td_approx)
- (is_complete td_approx)
- pr_td_approx td_approx
+ (is_pairwise_disjoint td_approx)
+ (is_complete td_approx)
+ pr_td_approx td_approx
);
let jump =
compute_jump
- auto tree states td_approx
- (List.exists (fun (_,(_,_,b)) -> b) td_approx)
+ auto tree states td_approx
+ (List.exists (fun (_,(_,_,b)) -> b) td_approx)
in
Cache.add cache states jump; jump
in
let b = TagSet.mem tag ts in
let () = LOG(__ "transition" 3 "tag=<%s>, %s: %a7C"
- (Tag.to_string tag)
- (if b then " taking" else "not taking")
- Transition.print tr)
+ (Tag.to_string tag)
+ (if b then " taking" else "not taking")
+ Transition.print tr)
in
if b then
- let _, _, _, f = Transition.node tr in
- let l, r = Formula.st f in
- (Translist.cons tr tr_acc,
- StateSet.union l l_acc,
- StateSet.union r r_acc)
+ let _, _, _, f = Transition.node tr in
+ let l, r = Formula.st f in
+ (Translist.cons tr tr_acc,
+ StateSet.union l l_acc,
+ StateSet.union r r_acc)
else acc) acc (Hashtbl.find auto.trans q))
states
(Translist.nil, StateSet.empty, StateSet.empty)
-
projects / SXSI / xpathcomp.git / blobdiff