diff --git a/NEWS b/NEWS index 892f5fbcc..492cc8706 100644 --- a/NEWS +++ b/NEWS @@ -70,11 +70,6 @@ New in spot 2.4.0.dev (not yet released) will work either on f or its negation. (see https://spot.lrde.epita.fr/hierarchy.html for details). - Bugs fixed: - - - spot::scc_info::determine_unknown_acceptance() incorrectly - considered some rejecting SCC as accepting. - Deprecation notices: (These functions still work but compilers emit warnings.) @@ -86,6 +81,16 @@ New in spot 2.4.0.dev (not yet released) Bugs fixed: + - spot::scc_info::determine_unknown_acceptance() incorrectly + considered some rejecting SCC as accepting. + + - spot::streett_to_generalized_buchi() could generate automata with + empty language if some Fin set did not intersect all accepting + SCCs. As a consequence, some Streett-like automata were + considered empty even though they were not. Also, the same + function could crash on input that had a Streett-like acceptance + not using all declared sets. + - The twa_graph::mege_edges() function relied on BDD IDs to sort edges. This in turn caused some algorithm (like the degeneralization) to produce slighltly different outputs (but diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 224a0f40b..34a3a7683 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1051,6 +1051,15 @@ namespace spot // Returns a number of pairs (>=0) if Streett, or -1 else. int is_streett() const; + /// \brief Rabin/streett pairs used by is_rabin_like and is_streett_like. + /// + /// These pairs hold two marks which can each contain one or no set. + /// + /// For instance is_streett_like() rewrites Inf(0)&(Inf(2)|Fin(1))&Fin(3) + /// as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})]. + /// + /// Empty marks should be interpreted in a way that makes them + /// false in Streett, and true in Rabin. struct SPOT_API rs_pair { rs_pair() = default; diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index f28a7cc05..8d20f8fbe 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -533,7 +533,9 @@ namespace spot acc_cond::mark_t fin; std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); unsigned p = inf.count(); - acc_cond::mark_t fin_not_inf = fin - inf; + // At some point we will remove anything that is not used as Inf. + acc_cond::mark_t to_strip = in->acc().all_sets() - inf; + acc_cond::mark_t inf_alone = 0U; if (!p) return remove_fin(in); @@ -543,8 +545,11 @@ namespace spot std::vector inf_to_finpairs(numsets, 0U); for (auto pair: pairs) { - for (unsigned mark: pair.fin.sets()) - fin_to_infpairs[mark] |= pair.inf; + if (pair.fin) + for (unsigned mark: pair.fin.sets()) + fin_to_infpairs[mark] |= pair.inf; + else + inf_alone |= pair.inf; for (unsigned mark: pair.inf.sets()) inf_to_finpairs[mark] |= pair.fin; @@ -634,11 +639,14 @@ namespace spot for (unsigned mark: (t.acc & fin).sets()) pend |= fin_to_infpairs[mark]; + // If we see some Inf set immediately, they are not + // pending anymore. pend -= t.acc & inf; + // Label this transition with all non-pending // inf sets. The strip will shift everything // to the correct numbers in the targets. - acc = (inf - pend).strip(fin - inf); + acc = (inf - pend).strip(to_strip); // Adjust the pending sets to what will be necessary // required on the destination state. if (sbacc) @@ -651,14 +659,14 @@ namespace spot pend -= a & inf; } - pend |= scc_inf_wo_fin; + pend |= inf_alone; } else if (no_fin && maybe_acc) { // If the acceptance is (Fin(0) | Inf(1)) & Inf(2) - // but we do not see any Fin set in this SCC, an + // but we do not see any Fin set in this SCC, a // mark {2} should become {1,2} before striping. - acc = (t.acc | (inf - scc_inf_wo_fin)).strip(fin_not_inf); + acc = (t.acc | (inf - scc_inf_wo_fin)).strip(to_strip); } assert((acc & out->acc().all_sets()) == acc); @@ -694,7 +702,7 @@ namespace spot stpend -= a & inf; } - st2gba_state d(t.dst, stpend | scc_inf_wo_fin); + st2gba_state d(t.dst, stpend | inf_alone); // Have we already seen this destination? unsigned dest; auto dres = bs2num.emplace(d, 0); diff --git a/tests/core/scc.test b/tests/core/scc.test index 8835402c5..b1a8704f2 100755 --- a/tests/core/scc.test +++ b/tests/core/scc.test @@ -139,3 +139,56 @@ State: 3 {1} --END-- EOF test 2 = `autfilt --stats=%[a]c in.hoa` + +# From issue #284, reported by Juraj Major. +cat >in.hoa <out +cat >exp <