INCLUDE "debug.ml"
INCLUDE "utils.ml"
+INCLUDE "log.ml"
open Format
-type t =
- { id : int;
- states : StateSet.t;
- init : StateSet.t;
- last : State.t;
-
- (* 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 }
+type t = {
+ id : int;
+ states : StateSet.t;
+ init : StateSet.t;
+ last : State.t;
+ (* 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) :
+ "Automaton (%i) :
States %a
Initial states: %a
Marking states: %a
let trs =
Hashtbl.fold
(fun _ t acc ->
- List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
+ 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::_ ->
- 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
+ match strings with
+ [] -> ()
+ | 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
type jump_kind =
| [ (_, (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
try Cache.find cache states with
| Not_found ->
let trs =
- (* Collect all (ts, (l, r, m)) where
- ts is a tagset, l and r are left and right set of states
- m is marking flag
- *)
+ (* Collect all (ts, (l, r, m)) where
+ ts is a tagset, l and r are left and right set of states
+ m is marking flag
+ *)
fold_trans_of_states auto
(fun acc_tr (ts, tr) ->
let pos =
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
states
[]
in
- (* for all labels in the tree compute which transition is taken *)
+ (* for all labels in the tree compute which transition is taken *)
let all_trs =
Ptset.Int.fold (fun tag acc ->
List.fold_left (fun acc' (ts, rhs) ->
else acc') acc trs)
(Tree.node_tags tree) []
in
- (* merge together states that have common labels *)
+ (* merge together states that have common labels *)
let uniq_states_trs =
merge_trans by_labels merge_states (List.sort by_labels all_trs)
in
- (* merge together labels that have common states *)
+ (* merge together labels that have common states *)
let td_approx =
merge_trans by_states merge_labels
(List.sort by_states uniq_states_trs)
in
- D_TRACE_(
+ LOG(
let is_pairwise_disjoint l =
List.for_all (fun ((ts, _) as tr) ->
List.for_all (fun ((ts', _) as tr') ->
==
(Tree.node_tags tree)
in
- eprintf "Top-down approximation (%b, %b):\n%!"
+ 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);
- 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%!"
-
+ (is_complete td_approx)
+ pr_td_approx td_approx
);
let jump =
compute_jump
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 "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)
+
projects / SXSI / xpathcomp.git / blobdiff