X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fata.ml;h=b24fd6b70256b430f0cb489f90f5143dd7840136;hb=3791216bfb2b9d966718f83fd414e8bcd5f7a066;hp=8f7529faa658bf1d4f0594d277240ab90a513e76;hpb=ecec752325cb3d207894a4f8d772936bd7ad9f4a;p=SXSI%2Fxpathcomp.git

diff --git a/src/ata.ml b/src/ata.ml
index 8f7529f..b24fd6b 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,9 +120,8 @@ 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"
-	  TagSet.print
-	  (TagSet.inj_positive rel_labels));
+	LOG(__ "top-down-approx"  3  "Computed rel_labels: %a@\n"
+	       TagSet.print (TagSet.inj_positive rel_labels));
 	NODE
       end else STAR
 
@@ -209,42 +208,41 @@ let top_down_approx auto states tree =
       merge_trans by_states merge_labels
 	(List.sort by_states uniq_states_trs)
     in
-    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
+    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
+      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 "%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
     );
     let jump =
       compute_jump
@@ -260,7 +258,13 @@ 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 "tag=<%s>, %s: %a7C"
+	(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,