diff --git a/NEWS b/NEWS index 444f15a15..8377926a7 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,8 @@ New in spot 1.99.1a (not yet released) * Bugs fixed: - p[+][:*2] was not detected as belonging to siPSL + - scc_filter() would incorrectly remove Fin marks from + rejecting SCCs. New in spot 1.99.1 (2015-06-23) diff --git a/src/tests/sccdot.test b/src/tests/sccdot.test index c89f090b1..1c817c607 100755 --- a/src/tests/sccdot.test +++ b/src/tests/sccdot.test @@ -168,7 +168,7 @@ State: 2 [0&1] 0 {0 1} State: 3 [1] 1 -[!1] 3 +[!1] 3 {2} State: 4 [!0&1] 4 {0 1} [0&1] 4 {0 2} diff --git a/src/tests/sccsimpl.test b/src/tests/sccsimpl.test index fc51e2966..65a02bb4b 100755 --- a/src/tests/sccsimpl.test +++ b/src/tests/sccsimpl.test @@ -240,3 +240,105 @@ grep 'Acceptance: 2 ' out8.txt run 0 ../ikwiad -R3 -s -RDS -ks \ '(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt grep 'states: 6$' out9.txt + + +# Spot 1.99.1 used to incorrectly remove Fin sets from rejecting SCCs +# in scc_filter(). +cat >input <output +# cat >expected <output +cat >expected < - struct acc_filter_all: next_filter + // non-accepting SCCs. If "RemoveAll" is false, keep those on + // transitions entering accepting SCCs. + template + struct acc_filter_mask: next_filter { + acc_cond::mark_t accmask; + template - acc_filter_all(scc_info* si, Args&&... args) + acc_filter_mask(scc_info* si, Args&&... args) : next_filter(si, std::forward(args)...) { + acc_cond::mark_t fin; + acc_cond::mark_t inf; + std::tie(inf, fin) = + si->get_aut()->acc().get_acceptance().used_inf_fin_sets(); + // If an SCC is rejecting, we can mask all the sets that are + // used only as Inf in the acceptance. + accmask = ~(inf - fin); } filtered_trans trans(unsigned src, unsigned dst, @@ -144,41 +154,18 @@ namespace spot if (keep) { - unsigned u = this->si->scc_of(src); + unsigned u = this->si->scc_of(dst); // If the edge is between two SCCs, or in a // non-accepting SCC. Remove the acceptance sets. - if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst)) - acc = 0U; + if ((this->si->is_rejecting_scc(u)) + || (RemoveAll && u != this->si->scc_of(src))) + acc &= accmask; } return filtered_trans(keep, cond, acc); } }; - // Remove acceptance conditions from all edges whose - // destination is not an accepting SCCs. - template - struct acc_filter_some: next_filter - { - template - acc_filter_some(scc_info* si, Args&&... args) - : next_filter(si, std::forward(args)...) - { - } - - filtered_trans trans(unsigned src, unsigned dst, - bdd cond, acc_cond::mark_t acc) - { - bool keep; - std::tie(keep, cond, acc) = - this->next_filter::trans(src, dst, cond, acc); - - if (this->si->is_rejecting_scc(this->si->scc_of(dst))) - acc = 0U; - return filtered_trans(keep, cond, acc); - } - }; - // Simplify redundant acceptance sets used in each SCCs. template struct acc_filter_simplify: next_filter @@ -329,22 +316,24 @@ namespace spot if (aut->acc().is_generalized_buchi()) { if (remove_all_useless) - res = scc_filter_apply>>>(aut, given_si); + res = + scc_filter_apply>>>(aut, given_si); else - res = scc_filter_apply>>>(aut, given_si); + res = + scc_filter_apply>>>(aut, given_si); } else { if (remove_all_useless) res = scc_filter_apply>>(aut, given_si); + >>(aut, given_si); else res = scc_filter_apply>>(aut, given_si); + >>(aut, given_si); } res->merge_edges(); res->prop_copy(aut, @@ -365,19 +354,19 @@ namespace spot if (remove_all_useless) res = scc_filter_apply>>>>(aut, given_si, - suspvars, - ignoredvars, - early_susp); + >>>>(aut, given_si, + suspvars, + ignoredvars, + early_susp); else res = scc_filter_apply>>>>(aut, given_si, - suspvars, - ignoredvars, - early_susp); + >>>>(aut, given_si, + suspvars, + ignoredvars, + early_susp); res->merge_edges(); res->prop_copy(aut, { false, // state-based acceptance is not preserved