From bdac53511addb0890f7425d37e7e50854af45e96 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Sep 2022 14:36:23 +0200 Subject: [PATCH] =?UTF-8?q?degen:=20learn=20to=20work=20on=20generalized-C?= =?UTF-8?q?o-B=C3=BCchi=20as=20well?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Adjust degeneralize() and degeneralize_tba() to work on generalized-co-Büchi. * NEWS: Mention this. * spot/twaalgos/cobuchi.hh, spot/twaalgos/cobuchi.cc (to_nca): Use degeneralization on generalized-co-Büchi. * spot/twaalgos/postproc.cc: Use degeneralization for generalized co-Büchi as well. * bin/autfilt.cc: Improve chain products of co-Büchi automata by using generalization if too many colors are needed. * tests/core/prodchain.test, tests/python/pdegen.py: Add test cases. --- NEWS | 3 +++ bin/autfilt.cc | 32 +++++++++++++--------- spot/twaalgos/cobuchi.cc | 16 +++++++---- spot/twaalgos/cobuchi.hh | 9 ++++--- spot/twaalgos/degen.cc | 56 ++++++++++++++++++++++++++++++--------- spot/twaalgos/degen.hh | 55 +++++++++++++++++++++++--------------- spot/twaalgos/postproc.cc | 29 +++++++++++++++----- tests/core/prodchain.test | 35 ++++++++++++------------ tests/python/pdegen.py | 15 ++++++++++- 9 files changed, 169 insertions(+), 81 deletions(-) diff --git a/NEWS b/NEWS index 66f56e75d..38beaa062 100644 --- a/NEWS +++ b/NEWS @@ -114,6 +114,9 @@ New in spot 2.10.6.dev (not yet released) to obtain a simple model checker (that returns true or false, without counterexample). + - degeneralize() and degeneralize_tba() learned to work on + generalized-co-Büchi as well. + - product() learned that the product of two co-Büchi automata is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 74fe44220..49543e596 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -713,10 +713,12 @@ ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) return p.run(aut); } -static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut) +static spot::twa_graph_ptr +ensure_tba(spot::twa_graph_ptr aut, + spot::postprocessor::output_type type = spot::postprocessor::Buchi) { spot::postprocessor p; - p.set_type(spot::postprocessor::Buchi); + p.set_type(type); p.set_pref(spot::postprocessor::Any); p.set_level(spot::postprocessor::Low); return p.run(aut); @@ -726,12 +728,14 @@ static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut) static spot::twa_graph_ptr product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { - if ((type == spot::postprocessor::Buchi) - && (left->num_sets() + right->num_sets() > - spot::acc_cond::mark_t::max_accsets())) + // Are we likely to fail because of too many colors? + if ((left->num_sets() + right->num_sets() > + spot::acc_cond::mark_t::max_accsets()) + && (type == spot::postprocessor::Buchi + || type == spot::postprocessor::CoBuchi)) { - left = ensure_tba(left); - right = ensure_tba(right); + left = ensure_tba(left, type); + right = ensure_tba(right, type); } return spot::product(left, right); } @@ -739,12 +743,14 @@ product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) static spot::twa_graph_ptr product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { - if ((type == spot::postprocessor::Buchi) - && (left->num_sets() + right->num_sets() > - spot::acc_cond::mark_t::max_accsets())) + // Are we likely to fail because of too many colors? + if ((left->num_sets() + right->num_sets() > + spot::acc_cond::mark_t::max_accsets()) + && (type == spot::postprocessor::Buchi + || type == spot::postprocessor::CoBuchi)) { - left = ensure_tba(left); - right = ensure_tba(right); + left = ensure_tba(left, type); + right = ensure_tba(right, type); } return spot::product_or(left, right); } @@ -988,7 +994,7 @@ parse_opt(int key, char* arg, struct argp_state*) if (!opt->included_in) opt->included_in = aut; else - opt->included_in = spot::product_or(opt->included_in, aut); + opt->included_in = ::product_or(opt->included_in, aut); } break; case OPT_INHERENTLY_WEAK_SCCS: diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 783cd0903..23d4871a0 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,6 +26,7 @@ #include #include #include +#include #include #include #include @@ -338,23 +339,26 @@ namespace spot twa_graph_ptr to_nca(const_twa_graph_ptr aut, bool named_states) { - if (aut->acc().is_co_buchi()) + const acc_cond& acc = aut->acc(); + if (acc.is_co_buchi()) return make_twa_graph(aut, twa::prop_set::all()); if (auto weak = weak_to_cobuchi(aut)) return weak; + if (acc.is_generalized_co_buchi()) + return degeneralize_tba(aut); + const acc_cond::acc_code& code = aut->get_acceptance(); std::vector pairs; - if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) + if (acc.is_streett_like(pairs) || acc.is_parity()) return nsa_to_nca(aut, named_states); else if (code.is_dnf()) return dnf_to_nca(aut, named_states); auto tmp = make_twa_graph(aut, twa::prop_set::all()); - tmp->set_acceptance(aut->acc().num_sets(), - aut->get_acceptance().to_dnf()); + tmp->set_acceptance(acc.num_sets(), code.to_dnf()); return to_nca(tmp, named_states); } @@ -683,6 +687,8 @@ namespace spot return make_twa_graph(aut, twa::prop_set::all()); if (auto weak = weak_to_cobuchi(aut)) return weak; + if (aut->acc().is_generalized_co_buchi()) + return degeneralize_tba(aut); } const acc_cond::acc_code& code = aut->get_acceptance(); diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh index 5c8d85e59..b02c0535d 100644 --- a/spot/twaalgos/cobuchi.hh +++ b/spot/twaalgos/cobuchi.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -92,8 +92,8 @@ namespace spot /// original language, and is a superset iff the original language /// can not be expressed using a co-Büchi acceptance condition. /// - /// The implementation dispatches between dnf_to_nca, nsa_to_nca, - /// and a trivial implementation for weak automata. + /// The implementation dispatches between dnf_to_nca(), nsa_to_nca(), + /// degeneralize_tba(), and a trivial implementation for weak automata. SPOT_API twa_graph_ptr to_nca(const_twa_graph_ptr aut, bool named_states = false); @@ -126,7 +126,8 @@ namespace spot /// can not be expressed using a co-Büchi acceptance condition. /// /// The implementation dispatches between dnf_to_dca, nsa_to_dca, - /// and a trivial implementation for deterministic weak automata. + /// degeneralize(), and a trivial implementation for deterministic + /// weak automata. SPOT_API twa_graph_ptr to_dca(const_twa_graph_ptr aut, bool named_states = false); } diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 333efe6e6..d79844b84 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -80,7 +80,8 @@ namespace spot void fill_cache(unsigned s) { unsigned s1 = scc_of(s); - acc_cond::mark_t common = a_->acc().all_sets(); + acc_cond::mark_t all_colors = a_->acc().all_sets(); + acc_cond::mark_t common = all_colors; acc_cond::mark_t union_ = {}; bool has_acc_self_loop = false; bool is_true_state = false; @@ -97,7 +98,7 @@ namespace spot std::get<2>(cache_[d]) &= t.acc; // an accepting self-loop? - if ((t.dst == s) && a_->acc().accepting(t.acc)) + if ((t.dst == s) && t.acc == all_colors) { has_acc_self_loop = true; if (t.cond == bddtrue) @@ -330,9 +331,10 @@ namespace spot bool skip_levels, bool ignaccsl, bool remove_extra_scc) { - if (!a->acc().is_generalized_buchi()) + bool input_is_gba = a->acc().is_generalized_buchi(); + if (!(input_is_gba || a->acc().is_generalized_co_buchi())) throw std::runtime_error - ("degeneralize() only works with generalized Büchi acceptance"); + ("degeneralize() only works with generalized (co)Büchi acceptance"); if (!a->is_existential()) throw std::runtime_error ("degeneralize() does not support alternation"); @@ -347,7 +349,11 @@ namespace spot // The result automaton is an SBA. auto res = make_twa_graph(dict); res->copy_ap_of(a); - res->set_buchi(); + if (input_is_gba) + res->set_buchi(); + else + res->set_co_buchi(); + acc_cond::mark_t all_colors = a->get_acceptance().used_sets(); if (want_sba) res->prop_state_acc(true); // Preserve determinism, weakness, and stutter-invariance @@ -396,9 +402,32 @@ namespace spot std::vector> lvl_cache(a->num_states()); // Compute SCCs in order to use any optimization. - std::unique_ptr m = use_scc - ? std::make_unique(a, scc_info_options::NONE) - : nullptr; + std::unique_ptr m = nullptr; + if (use_scc) + { + if (!input_is_gba) + { + // If the input is gen-co-Büchi, temporary pretend its + // generalized Büchi. + unsigned n = a->num_sets(); + twa_graph_ptr amut = std::const_pointer_cast(a); + amut->set_generalized_buchi(n); + try + { + m = std::make_unique(a, scc_info_options::NONE); + } + catch (...) + { + amut->set_generalized_co_buchi(n); + throw; + } + amut->set_generalized_co_buchi(n); + } + else + { + m = std::make_unique(a, scc_info_options::NONE); + } + } // Initialize scc_orders std::unique_ptr orders = use_cust_acc_orders @@ -674,7 +703,7 @@ namespace spot { d.second = 0; // Make it go to the first level. // Skip as many levels as possible. - if (!a->acc().accepting(acc) && skip_levels) + if (acc != all_colors && skip_levels) { if (use_cust_acc_orders) { @@ -723,9 +752,10 @@ namespace spot int use_lvl_cache, bool skip_levels, bool ignaccsl, bool remove_extra_scc) { - // If this already a degeneralized digraph, there is nothing we + // If this already a degeneralized twa, there is nothing we // can improve. - if (a->is_sba()) + if (const acc_cond& acc = a->acc(); + a->prop_state_acc() && (acc.is_buchi() || acc.is_co_buchi())) return std::const_pointer_cast(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, @@ -739,9 +769,9 @@ namespace spot int use_lvl_cache, bool skip_levels, bool ignaccsl, bool remove_extra_scc) { - // If this already a degeneralized digraph, there is nothing we + // If this already a degeneralized twa, there is nothing we // can improve. - if (a->acc().is_buchi()) + if (a->acc().is_buchi() || a->acc().is_co_buchi()) return std::const_pointer_cast(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 281ba2ef5..e9ae13021 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2015, 2017-2020 Laboratoire de +// Copyright (C) 2012-2015, 2017-2020, 2022 Laboratoire de // Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -26,33 +26,36 @@ namespace spot class scc_info; /// \ingroup twa_acc_transform - /// \brief Degeneralize a spot::tgba into an equivalent sba with - /// only one acceptance condition. + /// \brief Degeneralize a generalized (co)Büchi automaton into an + /// equivalent (co)Büchi automaton. /// - /// This algorithm will build a new explicit automaton that has - /// at most (N+1) times the number of states of the original automaton. + /// There are two variants of the function. If the generalizd + /// (co)Büchi acceptance uses N colors, degeneralize() algorithm + /// will builds a state-based (co)Büchi automaton that has at most + /// (N+1) times the number of states of the original automaton. + /// degeneralize_tba() builds a transition-based (co)Büchi automaton + /// that has at most N times the number of states of the original + /// automaton. /// - /// When \a use_z_lvl is set, the level of the degeneralized - /// automaton is reset everytime an SCC is exited. If \a - /// use_cust_acc_orders is set, the degeneralization will compute a - /// custom acceptance order for each SCC (this option is disabled by - /// default because our benchmarks show that it usually does more - /// harm than good). If \a use_lvl_cache is set, everytime an SCC - /// is entered on a state that as already been associated to some - /// level elsewhere, reuse that level (set it to 2 to keep the - /// smallest number, 3 to keep the largest level, and 1 to keep the - /// first level found). If \a ignaccsl is set, we do not directly - /// jump to the accepting level if the entering state has an - /// accepting self-loop. If \a remove_extra_scc is set (the default) - /// we ensure that the output automaton has as many SCCs as the input - /// by removing superfluous SCCs. + /// Additional options control optimizations described in + /// \cite babiak.13.spin . When \a use_z_lvl is set, the level of + /// the degeneralized automaton is reset everytime an SCC is exited. + /// If \a use_cust_acc_orders is set, the degeneralization will + /// compute a custom acceptance order for each SCC (this option is + /// disabled by default because our benchmarks show that it usually + /// does more harm than good). If \a use_lvl_cache is set, + /// everytime an SCC is entered on a state that as already been + /// associated to some level elsewhere, reuse that level (set it to + /// 2 to keep the smallest number, 3 to keep the largest level, and + /// 1 to keep the first level found). If \a ignaccsl is set, we do + /// not directly jump to the accepting level if the entering state + /// has an accepting self-loop. If \a remove_extra_scc is set (the + /// default) we ensure that the output automaton has as many SCCs as + /// the input by removing superfluous SCCs. /// /// Any of these three options will cause the SCCs of the automaton /// \a a to be computed prior to its actual degeneralization. /// - /// The degeneralize_tba() variant produce a degeneralized automaton - /// with transition-based acceptance. - /// /// The mapping between each state of the resulting automaton /// and the original state of the input automaton is stored in the /// "original-states" named property of the produced automaton. Call @@ -70,6 +73,14 @@ namespace spot /// Similarly, the property "degen-levels" keeps track of the degeneralization /// levels. To retrieve it, call /// `aut->get_named_prop>("degen-levels")`. + /// + /// As an alternative method to degeneralization, one may also + /// consider ACD transform. acd_transform() will never produce + /// larger automata than degenaralize_tba(), and + /// acd_transform_sbacc() produce smaller automata than + /// degeneralize() on the average. See \cite casares.22.tacas for + /// some comparisons. + /// /// \@{ SPOT_API twa_graph_ptr degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true, diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index a44ac3d52..39a6c0926 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -236,7 +236,8 @@ namespace spot if (COMP_) tmp = complete(tmp); bool want_parity = type_ & Parity; - if (want_parity && tmp->acc().is_generalized_buchi()) + if (want_parity && (tmp->acc().is_generalized_buchi() + || tmp->acc().is_generalized_co_buchi())) tmp = choose_degen(tmp); assert(!!SBACC_ == state_based_); if (state_based_) @@ -402,10 +403,19 @@ namespace spot if (PREF_ == Any) { - if (type_ == Buchi) - a = choose_degen(a); + if (type_ == Buchi + || (type_ == CoBuchi && a->acc().is_generalized_co_buchi())) + { + a = choose_degen(a); + } else if (type_ == CoBuchi) - a = to_nca(a); + { + a = to_nca(a); + if (state_based_ && a->prop_state_acc().is_true()) + a = do_sba_simul(a, simul_); + else + a = do_simul(a, simul_); + } return finalize(a); } @@ -699,6 +709,8 @@ namespace spot if (type_ == CoBuchi) { unsigned ns = sim->num_states(); + bool weak = sim->prop_weak().is_true(); + if (PREF_ == Deterministic) sim = to_dca(sim); else @@ -706,8 +718,13 @@ namespace spot // if the input of to_dca/to_nca was weak, the number of // states has not changed, and running simulation is useless. - if (level_ != Low && ns < sim->num_states()) - sim = do_simul(sim, simul_); + if (!weak || (level_ != Low && ns < sim->num_states())) + { + if (state_based_ && sim->prop_state_acc().is_true()) + sim = do_sba_simul(sim, simul_); + else + sim = do_simul(sim, simul_); + } } return finalize(sim); diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test index 9a9c74648..c2d6091c7 100755 --- a/tests/core/prodchain.test +++ b/tests/core/prodchain.test @@ -26,9 +26,7 @@ shift for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa -done -for i in *.hoa; do - set x "$@" --product $i + set x "$@" --product $i.hoa shift done shift @@ -41,8 +39,9 @@ test "4,7,16,1" = `autfilt --stats=%s,%e,%t,%a result` set x shift -for i in *.hoa; do - set x "$@" --product-or $i +for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ + 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do + set x "$@" --product-or $i.hoa shift done shift @@ -55,28 +54,30 @@ shift for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do ltl2tgba -D --cobuchi -S "{a[*$i]}<>->FGb" > $i.hoa -done -for i in *.hoa; do - set x "$@" --product $i + set x "$@" --product $i.hoa shift done shift -autfilt -D --cobuchi --low -S "$@" > result -test "85,170,174,1" = `autfilt --stats=%s,%e,%t,%a result` +autfilt --cobuchi --high -D -S "$@" > result +test "44,47,92,1" = `autfilt --stats=%s,%e,%t,%a result` +: > stats set x shift -for i in *.hoa; do - set x "$@" --product-or $i +for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ + 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do + ltl2tgba -D --cobuchi "{a[*$i]}<>->FGb" > $i.hoa + set x "$@" --product-or $i.hoa shift + test $i -eq 1 && shift # remove the first --product + test 2,3,6,1 = `autfilt --high --small --cobuchi "$@" --stats=%s,%e,%t,%a` + test 3,5,10,1 = \ + `autfilt --high --small --cobuchi "$@" | autfilt -S --stats=%s,%e,%t,%a` done -shift + if [ $MAX_ACCSETS -eq 32 ]; then - autfilt --cobuchi -S "$@" 2> error && exit 1 + autfilt "$@" 2> error && exit 1 grep 'Too many acceptance sets used' error fi -# FIXME: implement degeneralization for generalized-co-Büchi -# autfilt --cobuchi --low -S "$@" > result -# test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result` true diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 7df9f0878..00f3df7e0 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -149,6 +149,9 @@ tc.assertEqual(spot.is_partially_degeneralizable(de), []) df = spot.partial_degeneralize(f, [0, 1]) df.equivalent_to(f) tc.assertEqual(str(df.acc()), '(1, Fin(0))') +df2 = spot.degeneralize(f) +df.equivalent_to(f) +tc.assertEqual(str(df2.acc()), '(1, Fin(0))') try: df = spot.partial_degeneralize(f, [0, 1, 2]) @@ -206,6 +209,16 @@ pdaut7 = spot.partial_degeneralize(aut7, sets) tc.assertTrue(pdaut7.equivalent_to(aut7)) tc.assertEqual(daut7.num_states(), 10) tc.assertEqual(pdaut7.num_states(), 10) +ddaut7 = spot.dualize(aut7) +ddaut7a = spot.scc_filter(spot.dualize(spot.degeneralize_tba(ddaut7))) +tc.assertTrue(ddaut7a.equivalent_to(aut7)) +tc.assertEqual(ddaut7a.num_states(), daut7.num_states()) +ddaut7b = spot.scc_filter(spot.dualize(spot.to_nca(ddaut7))) +tc.assertTrue(ddaut7b.equivalent_to(aut7)) +tc.assertEqual(ddaut7b.num_states(), daut7.num_states()) +ddaut7c = spot.scc_filter(spot.dualize(spot.to_dca(ddaut7))) +tc.assertTrue(ddaut7c.equivalent_to(aut7)) +tc.assertEqual(ddaut7c.num_states(), daut7.num_states()) aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4) @@ -482,4 +495,4 @@ State: 1 [0] 0 {0} State: 2 [!0] 0 ---END--""") \ No newline at end of file +--END--""")