- try
- Cache.find cache states
- with
- Not_found ->
- let jump =
- begin
- let trs =
- StateSet.fold
- (fun q acc -> List.fold_left
- (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
- )
- acc
- (Hashtbl.find auto.trans q)
- )
- states
- []
- in
- (* all labels in the tree compute what transition would be taken *)
- let all_trs =
- Ptset.Int.fold (fun tag acc ->
- List.fold_left (fun acc' (ts, lhs) ->
- if TagSet.mem tag ts then
- (TagSet.singleton tag, lhs)::acc'
- else acc') acc trs)
- (Tree.node_tags tree) []
- in
- (* now merge together states that have common labels *)
- let uniq_states_trs =
- merge_trans by_labels merge_states (List.sort by_labels all_trs)
- in
- (* now 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%!"
-
- );
- let jump =
- compute_jump auto tree states td_approx (List.exists (fun (_,(_,_,b)) -> b) td_approx)
+ 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
+ *)
+ 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
+ []
+ 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) []
+ in
+ (* merge together states that have common labels *)
+ let uniq_states_trs =
+ merge_trans by_labels merge_states (List.sort by_labels all_trs)