diff --git a/NEWS b/NEWS index 8cb8e4a55..e38fc55b6 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,13 @@ New in spot 2.5.0.dev (not yet released) as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for is_generalized_streett + - the conversion from Rabin to Büchi was broken on Rabin-like + acceptance condition where one pair used Fin(x) and another pair + used Inf(x) with the same x. Unfortunately, this situation could + also occur as a side effect of simplifying the acceptance + condition (by merging identical set) prior to running the + conversion to Büchi. + New in spot 2.5 (2018-01-20) Build: diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 85b4b67f6..e194ac8d4 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1397,19 +1397,12 @@ namespace spot }); } - acc_cond::mark_t paired_with(unsigned mark) const + acc_cond::mark_t paired_with_fin(unsigned mark) const { acc_cond::mark_t res = 0U; for (const auto& p: pairs_) - { - if (visible(p.fin) && visible(p.inf)) - { - if (p.fin.has(mark)) - res |= p.inf; - if (p.inf.has(mark)) - res |= p.fin; - } - } + if (p.fin.has(mark) && visible(p.fin) && visible(p.inf)) + res |= p.inf; return res; } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 2206d8741..682bddc40 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -312,7 +312,7 @@ namespace spot for (const auto& e: si.edges_of(scc)) { - bool acc{e.acc & scc_infs_alone}; + bool acc = (e.acc & scc_infs_alone) != 0; res->new_acc_edge(e.src, e.dst, e.cond, acc); } @@ -320,6 +320,7 @@ namespace spot for (auto r: scc_pairs.fins().sets()) { + acc_cond::mark_t pairinf = scc_pairs.paired_with_fin(r); unsigned base = res->new_states(states.size()); for (auto s: states) state_map[s] = base++; @@ -329,9 +330,7 @@ namespace spot continue; auto src = state_map[e.src]; auto dst = state_map[e.dst]; - bool cacc = fins_alone.has(r) - ? true - : ((scc_pairs.paired_with(r) & e.acc) != 0); + bool cacc = fins_alone.has(r) || (pairinf & e.acc) != 0; res->new_acc_edge(src, dst, e.cond, cacc); // We need only one non-deterministic jump per // cycle. As an approximation, we only do diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 269ceb1a0..48b720cbd 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1504,6 +1504,27 @@ run 0 autfilt -H --tgba test1 > output cat output diff -u output expected-tgba +# Issue #324. +cat > 324 < out +test 2 = `autfilt -c --reject-word='a;cycle{!a&!b}' 324 out` # Add 10 small random automata for the next case randaut -A'random 6' -Q10 -n10 3 -Hl >> test1