diff --git a/NEWS b/NEWS index 05686a9d9..1ed6d66b5 100644 --- a/NEWS +++ b/NEWS @@ -36,6 +36,12 @@ New in spot 2.3.2.dev (not yet released) - In bench/stutter/ the .cc files were not compiling due to warnings being caught as errors. + - The code in charge of detecting DBA-type Rabin automata is + actually written to handle a slightly larger class of acceptance + conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to + correctly detect DBA-typeness in some of these non-Rabin + acceptance. + Backward-incompatible changes: - spot::acc_cond::mark_t::operator bool() has been marked as diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 52a6919fd..a85422366 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -73,7 +73,7 @@ namespace spot // accepting, but which becomes non-accepting when extended with // more states. i -= f; - i |= (inf_alone & sets); + i |= inf_alone & sets; if (!i) { // Check whether the SCC is accepting. We do that by simply @@ -192,14 +192,9 @@ namespace spot ba_final_states[s] = true; scc_ba_type = true; } - // Conversely, if all fin_alone appear in the SCC, then it - // cannot be accepting. - else if (sets & fin_alone) - { - scc_ba_type = false; - } - // In the generale case (no fin_alone involved), we need - // a dedicated check. + // In the general case, we need a dedicated check. Note + // that the used fin_alone sets can be ignored, as they + // cannot contribute to Büchi-typeness, else { scc_ba_type = is_scc_ba_type(aut, si.states_of(scc), diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 16d2fb978..6bd214bbf 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1,7 +1,8 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). + +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -236,6 +237,19 @@ State: 15 [t] 15 {4 15} [1] 16 {4} [!1] 22 {15} State: 16 [t] 16 {4 16} [t] 31 {14} [!1] 32 State: 32 [t] 32 {15} [1] 33 State: 33 [t] 33 {16} [!1] 36 State: 34 [t] 34 State: 35 [1] 34 {11} [!1] 35 {5} State: 36 [1] 34 {23} [!1] 36 {17} --END-- +HOA: v1 +States: 2 +Acceptance: 3 Fin(0) | (Fin(1)&Inf(2)) +Start: 0 +AP: 1 "a" +--BODY-- +State: 0 {0} +[0] 1 +[!0] 0 +State: 1 {2} +[0] 1 +[!0] 0 +--END-- EOF acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)' @@ -713,6 +727,22 @@ State: 36 [1] 34 [!1] 36 {0 1 2 3 4 5 6 7 8 9 10} --END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 0 +State: 1 {0} +[0] 1 +[!0] 0 +--END-- EOF cat >expected-tgba < output