diff --git a/NEWS b/NEWS index 432525b7d..7cd025721 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,15 @@ New in spot 2.8.3.dev (not yet released) parity_min_odd(n) = parity_min(true, n) parity_min_even(n) = parity_min(false, n) + Bugs fixed: + + - The Rabin-to-Büchi conversion could misbehave when applied to + Rabin-like acceptance with where some pairs have missing Inf(.) + (e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not + visit the remaining Inf(.). This indirectly caused the + complementation algorithm to produce incorrect results on such + inputs, causing false positives in ltlcross and autcross. + New in spot 2.8.3 (2019-11-06) Build: diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 83a0f36b7..18f16a9f3 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -126,7 +126,8 @@ namespace spot auto scc_pairs = rs_pairs_view(aut_pairs.pairs(), scc_acc); // If there is one aut_fin_alone that is not in the SCC, // any cycle in the SCC is accepting. - if (scc_pairs.fins_alone().proper_subset(aut_pairs.fins_alone())) + auto aut_fin_alone = aut_pairs.fins_alone(); + if ((scc_acc & aut_fin_alone) != aut_fin_alone) { for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e) { diff --git a/tests/core/complement.test b/tests/core/complement.test index 555336d3c..35931f82c 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -142,3 +142,19 @@ State: 1 --END-- EOF diff out expected + +# The following automaton used to be badly complemented due +# to a bug in the Rabin-to-BA conversion. +# Reported by Juraj Major and Tereza Šťastná. +cat >pos.hoa <neg.hoa +autfilt -q --intersect=pos.hoa neg.hoa && exit 1 +: