INCLUDE "debug.ml"
INCLUDE "utils.ml"
+INCLUDE "trace.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
+ TRACE("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 =
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_(
- 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
- eprintf "Top-down approximation (%b, %b):\n%!"
- (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%!"
-
+ 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
);
let jump =
compute_jump
(List.exists (fun (_,(_,_,b)) -> b) td_approx)
in
Cache.add cache states jump; jump
-