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

diff --git a/src/ata.ml b/src/ata.ml
index 0ae811d..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
@@ -183,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
@@ -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) ->
@@ -255,3 +255,25 @@ let top_down_approx auto states tree =
 
 
 
+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)
+