From 41722c0c5f23b0def3dbe8242b0ab9b85254cadf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Mar 2018 13:52:39 +0100 Subject: [PATCH] remove_fin: never return acceptance "f" Fixes #333. * spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh, spot/twaalgos/totgba.cc: Adjust. The assert() added to remove_fin() triggered a lot of failure in the test suite before the different functions were fixed. * tests/core/remfin.test, tests/python/tra2tba.py: Adjust expected result. * NEWS: Mention the bug. --- NEWS | 3 +++ spot/twaalgos/remfin.cc | 39 ++++++++++++++++++++++++++++++++++++--- spot/twaalgos/remfin.hh | 6 +++++- spot/twaalgos/totgba.cc | 12 ++++++++++++ tests/core/remfin.test | 5 +++-- tests/python/tra2tba.py | 13 +++++-------- 6 files changed, 64 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index a558ef149..0d7f2f287 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,9 @@ New in spot 2.5.1.dev (not yet released) acc_cond::is_generalized_streett() would segfault on weird acceptance conditions such as "3 t" or "3 f". + - remove_fin(), streett_to_generalized_buchi() should never + return automata with "f" acceptance. + New in spot 2.5.1 (2018-02-20) Library: diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index cf0b25262..e6ce3f638 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -464,6 +464,20 @@ namespace spot twa_graph_ptr trivial_strategy(const const_twa_graph_ptr& aut) { + if (aut->acc().is_f()) + { + // The original acceptance was equivalent to + // "f". Simply return an empty automaton with "t" + // acceptance. + auto res = make_twa_graph(aut->get_dict()); + res->set_generalized_buchi(0); + res->set_init_state(res->new_state()); + res->prop_stutter_invariant(true); + res->prop_weak(true); + res->prop_complete(false); + return res; + } + return (!aut->acc().uses_fin_acceptance()) ? std::const_pointer_cast(aut) : nullptr; @@ -514,10 +528,14 @@ namespace spot if (acccode.is_f()) { // The original acceptance was equivalent to - // "f". Simply return an empty automaton. + // "f". Simply return an empty automaton with "t" + // acceptance. auto res = make_twa_graph(aut->get_dict()); - res->set_acceptance(0, acccode); + res->set_generalized_buchi(0); res->set_init_state(res->new_state()); + res->prop_stutter_invariant(true); + res->prop_weak(true); + res->prop_complete(false); return res; } } @@ -746,6 +764,18 @@ namespace spot trace << "before cleanup: " << res->get_acceptance() << '\n'; cleanup_acceptance_here(res); trace << "after cleanup: " << res->get_acceptance() << '\n'; + if (res->acc().is_f()) + { + // "f" is not generalized-Büchi. Just return an + // empty automaton instead. + auto res2 = make_twa_graph(res->get_dict()); + res2->set_generalized_buchi(0); + res2->set_init_state(res2->new_state()); + res2->prop_stutter_invariant(true); + res2->prop_weak(true); + res2->prop_complete(false); + return res2; + } res->merge_edges(); return res; } @@ -822,6 +852,9 @@ namespace spot twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut) { - return remove_fin_impl(aut); + twa_graph_ptr res = remove_fin_impl(aut); + assert(!res->acc().uses_fin_acceptance()); + assert(!res->acc().is_f()); + return res; } } diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 7eb26b6eb..5f234efdb 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -48,12 +48,16 @@ namespace spot rabin_to_buchi_maybe(const const_twa_graph_ptr& aut); /// \ingroup twa_acc_transform - /// \brief Rewrite an automaton without Fin acceptance. + /// \brief Rewrite an automaton without Fin or f acceptance. /// /// This algorithm dispatches between many strategies. It has /// dedicated algorithms for weak automata, automata with Rabin-like /// acceptance, automata with Streett-like acceptance, and some /// generic code that will work on any kind of acceptance condition. + /// + /// In Spot "f" acceptance is not considered Fin-less, because + /// it can be seen as a case of generalized co-Büchi with 0 sets. + /// Just like "t" corresponds generalized Büchi with 0 sets.) SPOT_API twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index bac6fad04..46532a672 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -753,6 +753,18 @@ namespace spot } } simplify_acceptance_here(out); + if (out->acc().is_f()) + { + // "f" is not generalized-Büchi. Just return an + // empty automaton instead. + auto res = make_twa_graph(out->get_dict()); + res->set_generalized_buchi(0); + res->set_init_state(res->new_state()); + res->prop_stutter_invariant(true); + res->prop_weak(true); + res->prop_complete(false); + return res; + } return out; } diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 48b720cbd..4479835b5 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -363,9 +363,10 @@ HOA: v1 States: 1 Start: 0 AP: 0 -acc-name: none -Acceptance: 0 f +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak --BODY-- State: 0 --END-- diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index b1d01ac44..e1e6dc8bd 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -91,18 +91,15 @@ State: 1 """) exp = """HOA: v1 -States: 2 +States: 1 Start: 0 -AP: 2 "a" "b" -acc-name: none -Acceptance: 0 f +AP: 0 +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak --BODY-- State: 0 -[!0] 0 -[0] 1 -State: 1 -[0] 1 --END--""" res = spot.remove_fin(aut)