X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fata.ml;h=5287ed5a5169cd3a9a1b530acc3a9b2b01f6423d;hb=7c4c61cec6fe1ae3a1b83a59b17ce90adcfe9b0b;hp=8f7529faa658bf1d4f0594d277240ab90a513e76;hpb=5db22d04b3c81471dd521537a819da9ce541a171;p=SXSI%2Fxpathcomp.git diff --git a/src/ata.ml b/src/ata.ml index 8f7529f..5287ed5 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -1,6 +1,6 @@ INCLUDE "debug.ml" INCLUDE "utils.ml" -INCLUDE "trace.ml" +INCLUDE "log.ml" open Format @@ -120,7 +120,7 @@ let compute_jump auto tree states l marking = | _ -> if Ptset.Int.mem Tag.pcdata rel_labels then begin - TRACE("top-down-approx", 3, __ "Computed rel_labels: %a\n" + LOG("top-down-approx", 3, __ "Computed rel_labels: %a\n" TagSet.print (TagSet.inj_positive rel_labels)); NODE @@ -209,7 +209,7 @@ let top_down_approx auto states tree = merge_trans by_states merge_labels (List.sort by_states uniq_states_trs) in - TRACE( + LOG( "top-down-approx", 2, let is_pairwise_disjoint l = List.for_all (fun ((ts, _) as tr) -> @@ -260,7 +260,14 @@ let get_trans ?(attributes=TagSet.empty) auto states tag = List.fold_left (fun ((tr_acc, l_acc, r_acc) as acc) (ts, tr) -> let ts = if ts == TagSet.star then TagSet.diff ts attributes else ts in - if TagSet.mem tag ts then + let b = TagSet.mem tag ts in + let () = LOG("transition", 3, __ "Transition: %a, tag=%s, %s\n%!" + Transition.print + tr + (Tag.to_string tag) + (if b then "selected" else "not selected")) + in + if b then let _, _, _, f = Transition.node tr in let l, r = Formula.st f in (Translist.cons tr tr_acc,