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
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 =
end;
fprintf fmt "%!"
+let pr_trans fmt (ts, (l, r, m)) =
+ Format.fprintf fmt "%a %s %a %a"
+ TagSet.print ts
+ (if m then Pretty.double_right_arrow else Pretty.right_arrow)
+ StateSet.print l
+ StateSet.print r
let compute_jump auto tree states l marking =
let rel_trans, skip_trans =
List.fold_left
(fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) ->
- if not marking &&
- ((l == states && r == states)
- || (l == StateSet.empty && states == r)
- || (l == states && r = StateSet.empty)
- || (l == StateSet.empty && r = StateSet.empty))
- then (acc_rel, tr::acc_skip)
- else (tr::acc_rel, acc_skip))
+ if not marking &&
+ ((l == states && r == states)
+ || (l == StateSet.empty && states == r)
+ || (l == states && r = StateSet.empty)
+ || (l == StateSet.empty && r = StateSet.empty))
+ then (acc_rel, tr::acc_skip)
+ else (tr::acc_rel, acc_skip))
([],[]) l
in
let rel_labels = List.fold_left
else
match skip_trans with
[ (_, (l, r, _) ) ] when l == r && l == states ->
- begin
- match rel_trans with
- | [ (_, (l, r, m) ) ]
- when (rel_labels == (Tree.element_tags tree) ||
- Ptset.Int.is_singleton rel_labels)
- && (StateSet.diff l auto.true_states) == states && m
- -> CAPTURE_MANY(rel_labels)
- | _ ->
- JUMP_MANY(rel_labels)
- end
+ begin
+ match rel_trans with
+ | [ (_, (l, r, m) ) ]
+ when (rel_labels == (Tree.element_tags tree) ||
+ Ptset.Int.is_singleton rel_labels)
+ && (StateSet.diff l auto.true_states) == states && m
+ -> CAPTURE_MANY(rel_labels)
+ | _ ->
+ JUMP_MANY(rel_labels)
+ end
| [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
| _ ->
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
+ LOG(__ "top-down-approx" 3 "Computed rel_labels: %a"
+ TagSet.print (TagSet.inj_positive rel_labels));
+ LOG(__ "top-down-approx" 3 "skip_trans:@\n%a"
+ (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans)
+ skip_trans);
+ LOG(__ "top-down-approx" 3 "rel_trans:@\n%a"
+ (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans)
+ rel_trans);
+ NODE
end else STAR
module Cache = Hashtbl.Make(StateSet)
| 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
+ 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 =
- if ts == TagSet.star then Tree.element_tags tree
- else if ts == TagSet.any then Tree.node_tags tree
- else TagSet.positive ts
- in
- let _, _, m, f = Transition.node tr 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
- []
+ (fun acc_tr (ts, tr) ->
+ let pos =
+ if ts == TagSet.star then Tree.element_tags tree
+ else if ts == TagSet.any then Tree.node_tags tree
+ else TagSet.positive ts
+ in
+ let _, _, m, f = Transition.node tr 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 *)
let all_trs =
Ptset.Int.fold (fun tag acc ->
- List.fold_left (fun acc' (ts, rhs) ->
- if TagSet.mem tag ts then
- (TagSet.singleton tag, rhs)::acc'
- else acc') acc trs)
- (Tree.node_tags tree) []
+ List.fold_left (fun acc' (ts, rhs) ->
+ if TagSet.mem tag ts then
+ (TagSet.singleton tag, rhs)::acc'
+ else acc') acc trs)
+ (Tree.node_tags tree) []
in
(* merge together states that have common labels *)
let uniq_states_trs =
(* merge together labels that have common states *)
let td_approx =
merge_trans by_states merge_labels
- (List.sort by_states uniq_states_trs)
+ (List.sort by_states uniq_states_trs)
in
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 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
- auto tree states td_approx
- (List.exists (fun (_,(_,_,b)) -> b) td_approx)
+ auto tree states td_approx
+ (List.exists (fun (_,(_,_,b)) -> b) td_approx)
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 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
+ LOG(__ "transition" 3 "tag=<%s>, %s: %a"
+ (Tag.to_string tag)
+ (if b then " taking" else "not taking")
+ Transition.print tr);
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)
+ 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)
-