From df04c715cfef32e2f58b7ef7e68a71e6a4bc1eae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Aug 2017 17:43:01 +0200 Subject: [PATCH] remove_fin: fix incorrect state-based output * spot/twaalgos/remfin.cc: If no Inf set is used, set sbacc early so that it is used in the algorithm. * tests/core/remfin.test: Add more tests. * NEWS: Mention the bug. --- NEWS | 7 ++ spot/twaalgos/remfin.cc | 11 +-- tests/core/remfin.test | 191 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 204 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index b3b62f8ab..80e1e9578 100644 --- a/NEWS +++ b/NEWS @@ -194,6 +194,13 @@ New in spot 2.3.5.dev (not yet released) - The 'spot.gen' package exports the functions from libspotgen. See https://spot.lrde.epita.fr/ipynb/gen.html for examples. + Bugs fixed: + + - When the remove_fin() function was called on some automaton with + Inf-less acceptance involving at least one disjunction (e.g., + generalized co-Büchi), it would sometime output an automaton with + transition-based acceptance but marked as state-based. + 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 ba82d987d..09656bf93 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -27,7 +27,7 @@ #include #include "spot/priv/enumflags.hh" -//#define TRACE +// #define TRACE #ifdef TRACE #define trace std::cerr #else @@ -672,7 +672,11 @@ namespace spot res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_init_state(aut->get_init_state_number()); - bool sbacc = aut->prop_state_acc().is_true(); + // If the input had no Inf, the output is a state-based automaton. + if (allinf == 0U) + res->prop_state_acc(true); + + bool sbacc = res->prop_state_acc().is_true(); scc_info si(aut); unsigned nscc = si.scc_count(); std::vector state_map(nst); @@ -749,9 +753,6 @@ namespace spot } } - // If the input had no Inf, the output is a state-based automaton. - if (allinf == 0U) - res->prop_state_acc(true); res->purge_dead_states(); trace << "before cleanup: " << res->get_acceptance() << '\n'; diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 7f279753e..ac087e2ee 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -250,6 +250,20 @@ State: 1 {2} [0] 1 [!0] 0 --END-- +/* +** This random automaton caused remove_fin() to output +** an automaton with transition-based acceptance incorrectly marked as +** state-based. +*/ +HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" Acceptance: 4 Fin(1) | +(Fin(2) & Fin(3) & Fin(0)) properties: trans-labels explicit-labels +trans-acc --BODY-- State: 0 [!0&1] 5 [!0&1] 7 State: 1 [0&!1] 2 {2} +[0&1] 9 {1} [!0&1] 1 [0&!1] 6 {1 3} State: 2 [!0&1] 8 {0 1} [!0&!1] +1 {1} State: 3 [!0&1] 5 {1} [0&1] 2 State: 4 [0&!1] 4 {1} [0&1] 6 {0} +[0&1] 5 {1} State: 5 [0&1] 9 {1} State: 6 [0&1] 5 {2 3} [!0&1] 9 {2} +[!0&1] 4 State: 7 [0&!1] 8 {3} [!0&!1] 7 {2} [0&!1] 3 {2} [!0&1] 5 {1} +State: 8 [!0&1] 8 {2} [!0&!1] 3 {1} [!0&1] 4 State: 9 [0&!1] 6 {0 3} +[!0&1] 2 --END-- EOF acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)' @@ -715,6 +729,91 @@ State: 1 {0} [!0] 0 [0] 1 --END-- +HOA: v1 +States: 21 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 {0} +[!0&1] 5 +[!0&1] 7 +State: 1 +[!0&1] 1 +[0&!1] 2 +[0&!1] 6 +[0&1] 9 +[!0&1] 14 +[!0&1] 20 +State: 2 +[!0&!1] 1 +[!0&1] 8 +[!0&!1] 20 +State: 3 +[0&1] 2 +[!0&1] 5 +[0&1] 18 +State: 4 +[0&!1] 4 +[0&1] 5 +[0&1] 6 +[0&!1] 17 +State: 5 +[0&1] 9 +State: 6 +[!0&1] 4 +[0&1] 5 +[!0&1] 9 +[!0&1] 12 +[!0&1] 17 +State: 7 {0} +[0&!1] 3 +[!0&1] 5 +[!0&!1] 7 +[0&!1] 8 +State: 8 +[!0&!1] 3 +[!0&1] 4 +[!0&1] 8 +[!0&1] 12 +[!0&1] 13 +[!0&1] 17 +[!0&!1] 19 +State: 9 +[!0&1] 2 +[0&!1] 6 +[0&!1] 11 +[!0&1] 18 +State: 10 {0} +[0&!1] 11 +State: 11 {0} +[!0&1] 10 +[!0&1] 12 +State: 12 {0} +[0&1] 11 +State: 13 {0} +[!0&1] 12 +[!0&1] 13 +State: 14 {0} +[!0&1] 14 +State: 15 {0} +[0&1] 16 +State: 16 {0} +[!0&1] 18 +State: 17 {0} +[0&1] 15 +[0&!1] 17 +State: 18 {0} +[!0&!1] 20 +State: 19 {0} +[!0&1] 15 +[0&1] 18 +State: 20 {0} +[0&1] 16 +[!0&1] 20 +--END-- EOF cat >expected-tgba < output @@ -1183,3 +1367,10 @@ diff -u output expected run 0 $autfilt -H --tgba test1 > output cat output diff -u output expected-tgba + +# make sure the above expected automata are correct +autcross --language-preserved 'autfilt --remove-fin' 'autfilt --tgba' -Ftest1 + +# try 10 small random automata just in case +randaut -A'random 6' -Q10 -n10 3 | +autcross --verbose --language-preserved 'autfilt --remove-fin' 'autfilt --tgba'