Uses the Logger.print function instead of Printf.eprintf
[SXSI/xpathcomp.git] / src / ata.ml
index 0ae811d..3c27ae8 100644 (file)
@@ -1,6 +1,6 @@
 INCLUDE "debug.ml"
 INCLUDE "utils.ml"
-INCLUDE "trace.ml"
+INCLUDE "log.ml"
 
 open Format
 
@@ -9,25 +9,24 @@ type t = {
   states : StateSet.t;
   init : StateSet.t;
   last : State.t;
-
-      (* Transitions of the Alternating automaton *)
+  (* Transitions of the Alternating automaton *)
   trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
   marking_states : StateSet.t;
   topdown_marking_states : StateSet.t;
   bottom_states : StateSet.t;
   true_states : StateSet.t
- }
+}
 
 let print ppf a =
   fprintf ppf
-    "Automaton (%i) :
-States %a
-Initial states: %a
-Marking states: %a
-Topdown marking states: %a
-Bottom states: %a
-True states: %a
-Alternating transitions\n"
+    "Automaton (%i) :@\n\
+     States %a@\n\
+     Initial states: %a@\n\
+     Marking states: %a@\n\
+     Topdown marking states: %a@\n\
+     Bottom states: %a@\n\
+     True states: %a@\n\
+     Alternating transitions:@\n"
     a.id
     StateSet.print a.states
     StateSet.print a.init
@@ -37,18 +36,19 @@ Alternating transitions\n"
     StateSet.print a.true_states;
   let trs =
     Hashtbl.fold
-      (fun _ t acc ->
-       List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
+      (fun _ t acc -> List.fold_left (fun acc (_, tr) -> tr::acc) acc t)
+      a.trans
+      []
   in
   let sorted_trs = List.stable_sort Transition.compare trs in
   let strings = Transition.format_list sorted_trs in
   match strings with
-    [] -> ()
-  | line::_ -> 
+  | [] -> ()
+  | line::_ ->
     let sline = Pretty.line (Pretty.length line) in
-    fprintf ppf "%s\n%!" sline;
-    List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
-    fprintf ppf "%s\n%!" sline
+    fprintf ppf "%s@\n" sline;
+    List.iter (fun s -> fprintf ppf "%s@\n" s) strings;
+    fprintf ppf "%s@\n" sline
 
 
 type jump_kind =
@@ -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
 
@@ -183,7 +182,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,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
@@ -255,3 +253,24 @@ 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 "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,
+        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)
+