X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fata.ml;h=5287ed5a5169cd3a9a1b530acc3a9b2b01f6423d;hb=7c4c61cec6fe1ae3a1b83a59b17ce90adcfe9b0b;hp=21c1a7f38f3ca5c78391dd56d078e75cfa1108df;hpb=6a86f6e048fd6c2d5768e413c469a87d7bb54eb5;p=SXSI%2Fxpathcomp.git

diff --git a/src/ata.ml b/src/ata.ml
index 21c1a7f..5287ed5 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -1,5 +1,6 @@
 INCLUDE "debug.ml"
 INCLUDE "utils.ml"
+INCLUDE "log.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
+	LOG("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
@@ -182,7 +183,7 @@ let top_down_approx auto states tree =
 	    else TagSet.positive ts
 	  in
 	  let _, _, m, f = Transition.node tr in
-	  let (_, _, ls), (_, _, rs) = Formula.st f 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
@@ -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%!"
-
+    LOG(
+      "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
@@ -249,3 +253,27 @@ let top_down_approx auto states tree =
     in
     Cache.add cache states jump; jump
 
+
+
+let get_trans ?(attributes=TagSet.empty) auto states tag =
+  StateSet.fold (fun q acc ->
+    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
+      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,
+	 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)
+