From 32087f29ad6c547e2cbbe007a913458718026f17 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Sep 2017 17:17:17 +0200 Subject: [PATCH] streett_to_generalized_buchi: fix incorrect algorithm Fixes #284, reported by Juraj Major. * spot/twaalgos/totgba.cc: Fix the algorithm. * spot/twa/acc.hh: More doc for future generations. * tests/core/scc.test: More test cases. * NEWS: Mention the issues. --- NEWS | 7 ++++++ spot/twa/acc.hh | 9 +++++++ spot/twaalgos/totgba.cc | 24 ++++++++++++------- tests/core/scc.test | 53 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 85 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 2c5c5ccbf..de0c76ca5 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,13 @@ New in spot 2.4.0.dev (not yet released) - 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 eaaf8419a..5c0535974 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1046,6 +1046,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 ea8f981ac..8021cd903 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -130,7 +130,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); @@ -140,8 +142,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; @@ -231,11 +236,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) @@ -248,14 +256,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); @@ -291,7 +299,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 <