From a924bc561ae4873d6a5b6a8ce5ae04791766c665 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Jan 2018 11:56:43 +0100 Subject: [PATCH] remove_fin: use simplify_acceptance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/remfin.cc: Simplify acceptance before trying the different strategies. * spot/twaalgos/cleanacc.cc: Skip simplify_complementary_marks_here() on generalized Büchi. * tests/core/remfin.test, tests/python/tra2tba.py: Adjust. * spot/twaalgos/totgba.cc: Simplify the result of Streett->GBA. * NEWS: Adjust. --- NEWS | 11 ++++++---- spot/twaalgos/cleanacc.cc | 3 ++- spot/twaalgos/remfin.cc | 42 ++++++++++++++++++--------------------- spot/twaalgos/totgba.cc | 5 +++-- tests/core/remfin.test | 16 +++++++-------- tests/python/tra2tba.py | 8 ++++---- 6 files changed, 43 insertions(+), 42 deletions(-) diff --git a/NEWS b/NEWS index a5b7ebd1c..ebeee2ac8 100644 --- a/NEWS +++ b/NEWS @@ -186,6 +186,9 @@ New in spot 2.4.4.dev (net yet released) are not very smart: if the input does not already have parity acceptance, it will simply be degeneralized or determinized. + - spot::remove_fin() will now call simplify_acceptance(), introduced + in 2.4, before attempting its different Fin-removal strategies. + - acc_cond::name(fmt) is a new method that name well-known acceptance conditions. The fmt parameter specify the format to use for that name (e.g. to the style used in HOA, or that used by print_dot()). @@ -258,10 +261,10 @@ New in spot 2.4.4.dev (net yet released) Bugs fixed: - - spot::simplify_acceptance() could produce incorrect output - if the first edge of the automaton was the only one with no - acceptance set. In spot 2.4.x this function was only used - by autfilt --simplify-acceptance. + - spot::simplify_acceptance() could produce incorrect output if the + first edge of the automaton was the only one with no acceptance + set. In spot 2.4.x this function was only used by autfilt + --simplify-acceptance; in 2.5 it is now used in remove_fin(). New in spot 2.4.4 (2017-12-25) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 75d699670..62082a6fd 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -325,7 +325,8 @@ namespace spot { cleanup_acceptance_here(aut, false); merge_identical_marks_here(aut); - simplify_complementary_marks_here(aut); + if (!aut->acc().is_generalized_buchi()) + simplify_complementary_marks_here(aut); cleanup_acceptance_here(aut, true); return aut; diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 0d25020ff..344e5d31a 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -256,11 +256,8 @@ namespace spot // TBA-typeness of the SCC, but the resulting automaton should // be correct nonetheless. twa_graph_ptr - tra_to_tba(const const_twa_graph_ptr& inaut) + tra_to_tba(const const_twa_graph_ptr& aut) { - // cleanup acceptance for easy detection of alone fins and infs - auto aut = cleanup_acceptance(inaut); - std::vector pairs; if (!aut->acc().is_rabin_like(pairs)) return nullptr; @@ -501,20 +498,6 @@ namespace spot twa_graph_ptr default_strategy(const const_twa_graph_ptr& aut) { - { - // We want a clean acceptance condition, i.e., one where all - // sets are useful. If that is not the case, clean it first. - acc_cond::mark_t unused = aut->acc().all_sets(); - for (auto& t: aut->edges()) - { - unused -= t.acc; - if (!unused) - break; - } - if (unused) - return remove_fin(cleanup_acceptance(aut)); - } - std::vector code; std::vector rem; std::vector keep; @@ -525,10 +508,21 @@ namespace spot { auto acccode = aut->get_acceptance(); if (!acccode.is_dnf()) - acccode = acccode.to_dnf(); + { + acccode = acccode.to_dnf(); + + if (acccode.is_f()) + { + // The original acceptance was equivalent to + // "f". Simply return an empty automaton. + auto res = make_twa_graph(aut->get_dict()); + res->set_acceptance(0, acccode); + res->set_init_state(res->new_state()); + return res; + } + } auto split = split_dnf_acc_by_fin(acccode); - auto sz = split.size(); assert(sz > 0); @@ -759,9 +753,11 @@ namespace spot twa_graph_ptr remove_fin_impl(const const_twa_graph_ptr& aut, const strategy_t skip = {}) { + auto simp = simplify_acceptance(aut); + auto handle = [&](strategy stra, strategy_t type) -> twa_graph_ptr { - return (type & skip) ? nullptr : stra(aut); + return (type & skip) ? nullptr : stra(simp); }; if (auto maybe = handle(trivial_strategy, strategy_t::trivial)) @@ -785,7 +781,7 @@ namespace spot return maybe; if (auto maybe = handle(streett_strategy, strategy_t::streett)) return maybe; - return default_strategy(aut); + return default_strategy(simp); } } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 41ea61202..9dac455e4 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -724,6 +724,7 @@ namespace spot } } } + simplify_acceptance_here(out); return out; } diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 12437b69d..269ceb1a0 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -394,7 +394,8 @@ State: 0 [!0] 0 [0] 1 State: 1 {0} -[t] 1 +[!0] 1 +[0] 1 --END-- HOA: v1 States: 10 @@ -589,9 +590,8 @@ HOA: v1 States: 37 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 12 -Acceptance: 12 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)\ -&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete --BODY-- State: 0 @@ -731,7 +731,7 @@ State: 32 State: 33 [t] 33 [!1] 36 -State: 34 {0 1 2 3 4 5 6 7 8 9 10 11} +State: 34 {0} [t] 34 State: 35 [1] 34 @@ -750,11 +750,11 @@ properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 -[!0] 0 [0] 1 +[!0] 0 State: 1 {0} -[!0] 0 [0] 1 +[!0] 0 --END-- HOA: v1 States: 21 diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index 715fdeafe..b1d01ac44 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -94,8 +94,8 @@ exp = """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" -acc-name: Buchi -Acceptance: 1 Inf(0) +acc-name: none +Acceptance: 0 f properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 @@ -383,11 +383,11 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 {0} -[!1&!2] 0 [1&!2] 1 +[!1&!2] 0 State: 1 -[!1&!2] 0 [1&!2] 1 +[!1&!2] 0 --END--""" res = spot.remove_fin(aut)