diff --git a/NEWS b/NEWS index da6b9f1be..8cb8e4a55 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,12 @@ New in spot 2.5.0.dev (not yet released) - iar() and iar_maybe() properly handle Rabin-like conditions. + - is_generalized_rabin() had a typo that caused some non-simplified + acceptance conditions like Fin(0)|(Fin(0)&Inf(1)) to be + incorrectly detecteded as generalized-Rabin 2 0 1 and then output + as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for + is_generalized_streett + New in spot 2.5 (2018-01-20) Build: diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 2de0d221e..0c36625b5 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -666,7 +666,7 @@ namespace spot auto s = code_.back().sub.size; acc_cond::mark_t seen_fin = 0U; acc_cond::mark_t seen_inf = 0U; - // Each pairs is the position of a Fin followed + // Each pair is the position of a Fin followed // by the number of Inf. std::map p; while (s) @@ -697,7 +697,7 @@ namespace spot unsigned i = m2.count(); // If we have seen this pair already, it must have the // same size. - if (p.emplace(m1.max_set(), i).first->second != i) + if (p.emplace(m1.max_set() - 1, i).first->second != i) return false; assert(i > 0); unsigned j = m1.max_set(); // == n+1 @@ -705,7 +705,6 @@ namespace spot if (!m2.has(j++)) return false; while (--i); - seen_fin |= m1; seen_inf |= m2; } @@ -715,8 +714,10 @@ namespace spot for (auto s: m1.sets()) // If we have seen this pair already, it must have the // same size. - if (p.emplace(s, 0U).first->second != 0U) - return false; + { + if (p.emplace(s, 0U).first->second != 0U) + return false; + } seen_fin |= m1; } else @@ -777,7 +778,7 @@ namespace spot unsigned i = m2.count(); // If we have seen this pair already, it must have the // same size. - if (p.emplace(m1.max_set(), i).first->second != i) + if (p.emplace(m1.max_set() - 1, i).first->second != i) return false; assert(i > 0); unsigned j = m1.max_set(); // == n+1 diff --git a/tests/core/accsimpl.test b/tests/core/accsimpl.test index 773dc85af..1feb8fed4 100755 --- a/tests/core/accsimpl.test +++ b/tests/core/accsimpl.test @@ -28,3 +28,26 @@ set -e ltlcross -f FGa \ 'ltl2tgba -G -D %f | autfilt --complement >%O' \ 'ltl2tgba -G -D %f | autfilt --complement | autfilt --simplify-acceptance >%O' + + +cat >325 < 325s +exp='4 Fin(0) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))' +test "$exp" = "`autfilt --stats='%a %g' 325s`"