X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fata.ml;h=da2f8ce2c765589f85b1b6f3cd533ed6e875a2b9;hb=a6baedc6c67cb1de0587a779f8bcddf276b0bf4c;hp=21c1a7f38f3ca5c78391dd56d078e75cfa1108df;hpb=63db110485e97e189313abd1a6ce1bedf941d76d;p=SXSI%2Fxpathcomp.git diff --git a/src/ata.ml b/src/ata.ml index 21c1a7f..da2f8ce 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -1,5 +1,6 @@ INCLUDE "debug.ml" INCLUDE "utils.ml" +INCLUDE "trace.ml" open Format @@ -118,12 +119,12 @@ let compute_jump auto tree states l marking = | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels) | _ -> - if Ptset.Int.mem Tag.pcdata rel_labels then - let () = - D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!" - TagSet.print (TagSet.inj_positive rel_labels)) - in NODE - else STAR + if Ptset.Int.mem Tag.pcdata rel_labels then begin + TRACE("top-down-approx", 3, __ "Computed rel_labels: %a\n" + TagSet.print + (TagSet.inj_positive rel_labels)); + NODE + end else STAR module Cache = Hashtbl.Make(StateSet) let cache = Cache.create 1023 @@ -208,39 +209,42 @@ let top_down_approx auto states tree = merge_trans by_states merge_labels (List.sort by_states uniq_states_trs) in - D_TRACE_( - 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 - in - let is_complete l = TagSet.positive - (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts) - TagSet.empty l) - == - (Tree.node_tags tree) - in - eprintf "Top-down approximation (%b, %b):\n%!" - (is_pairwise_disjoint td_approx) - (is_complete 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 - eprintf "%a, %a, %b -> %a, %a\n%!" - StateSet.print states - TagSet.print ts - m - StateSet.print l - StateSet.print r - ) td_approx; - eprintf "\n%!" - + TRACE( + "top-down-approx", 2, + 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 + in + let is_complete l = TagSet.positive + (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 "\t%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 + __ " pairwise-disjoint:%b, complete:%b:\n%a" + (is_pairwise_disjoint td_approx) + (is_complete td_approx) + pr_td_approx td_approx ); let jump = compute_jump @@ -248,4 +252,3 @@ let top_down_approx auto states tree = (List.exists (fun (_,(_,_,b)) -> b) td_approx) in Cache.add cache states jump; jump -