X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fata.ml;h=b24fd6b70256b430f0cb489f90f5143dd7840136;hb=3791216bfb2b9d966718f83fd414e8bcd5f7a066;hp=96d13d444e907dd27efc74bf027fbf2124ebc908;hpb=13f8cb39ae4df2a6ae68f013eef6d3dc61489263;p=SXSI%2Fxpathcomp.git diff --git a/src/ata.ml b/src/ata.ml index 96d13d4..b24fd6b 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -1,25 +1,26 @@ 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 @@ -37,17 +38,17 @@ Alternating transitions\n" 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 = @@ -118,12 +119,11 @@ 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 @@ -170,10 +170,10 @@ let top_down_approx auto states tree = 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 = @@ -182,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 @@ -190,7 +190,7 @@ let top_down_approx auto states tree = 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) -> @@ -199,16 +199,16 @@ let top_down_approx auto states tree = 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') -> @@ -221,26 +221,28 @@ let top_down_approx auto states tree = == (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 @@ -249,3 +251,26 @@ 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 "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) +