diff --git a/NEWS b/NEWS index 0d7060529..347f44488 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,10 @@ New in spot 2.11.6.dev (not yet released) the automaton using a basis of disjoint labels. See https://spot.lre.epita.fr/tut25.html for some motivation. + - autfilt learned --reduce-acceptance-set/--enlarge-acceptance-set + to heurisitcally remove/add to unnecessary acceptance marks in + Büchi automata. (Issue #570) + - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. @@ -142,6 +146,11 @@ New in spot 2.11.6.dev (not yet released) The above also impacts autfilt --included-in option. + - spot::reduce_buchi_acceptance_set_here() and + spot::enlarge_buchi_acceptance_set_here() will heuristically + remove/add unnecessary acceptance marks in Büchi automata. + (Issue #570.) + - Given a twa_word_ptr W and a twa_ptr A both sharing the same alphabet, one can now write W->intersects(A) or A->intersects(W) instead of the longuer W->as_automaton()->intersects(A) or diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 08b17df99..420bf2867 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -102,6 +102,7 @@ enum { OPT_DUALIZE, OPT_DNF_ACC, OPT_EDGES, + OPT_ENLARGE_ACCEPTANCE_SET, OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, OPT_GENERALIZED_RABIN, @@ -139,6 +140,7 @@ enum { OPT_PRODUCT_AND, OPT_PRODUCT_OR, OPT_RANDOMIZE, + OPT_REDUCE_ACCEPTANCE_SET, OPT_REJ_SCCS, OPT_REJECT_WORD, OPT_REM_AP, @@ -278,6 +280,12 @@ static const argp_option options[] = { "nth", 'N', "RANGE", 0, "assuming input automata are numbered from 1, keep only those in RANGE", 0 }, + { "enlarge-acceptance-set", OPT_ENLARGE_ACCEPTANCE_SET, nullptr, 0, + "enlarge the number of accepting transitions (or states if -S) in a " + "Büchi automaton", 0 }, + { "reduce-acceptance-set", OPT_REDUCE_ACCEPTANCE_SET, nullptr, 0, + "reduce the number of accepting transitions (or states if -S) in a " + "Büchi automaton", 0 }, /**************************************************/ RANGE_DOC_FULL, WORD_DOC, @@ -705,6 +713,8 @@ static int opt_highlight_accepting_run = -1; static bool opt_highlight_languages = false; static bool opt_dca = false; static bool opt_streett_like = false; +static bool opt_enlarge_acceptance_set = false; +static bool opt_reduce_acceptance_set = false; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) @@ -899,12 +909,12 @@ parse_opt(int key, char* arg, struct argp_state*) opt_dnf_acc = true; opt_cnf_acc = false; break; - case OPT_STREETT_LIKE: - opt_streett_like = true; - break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_ENLARGE_ACCEPTANCE_SET: + opt_enlarge_acceptance_set = true; + break; case OPT_EXCLUSIVE_AP: opt->excl_ap.add_group(arg); break; @@ -1164,6 +1174,9 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_REDUCE_ACCEPTANCE_SET: + opt_reduce_acceptance_set = true; + break; case OPT_REJ_SCCS: opt_rej_sccs = parse_range(arg, 0, std::numeric_limits::max()); opt_art_sccs_set = true; @@ -1215,6 +1228,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STATES: opt_states = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_STREETT_LIKE: + opt_streett_like = true; + break; case OPT_STRIPACC: opt_stripacc = true; break; @@ -1670,6 +1686,11 @@ namespace else if (opt_rem_unused_ap) // constrain(aut, true) already does that aut->remove_unused_ap(); + if (opt_enlarge_acceptance_set) + spot::enlarge_buchi_acceptance_set_here(aut, sbacc); + if (opt_reduce_acceptance_set) + spot::reduce_buchi_acceptance_set_here(aut, sbacc); + if (opt_split_edges) aut = spot::split_edges(aut); else if (opt_separate_edges) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 26f6f834f..4bb96e44a 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -18,6 +18,8 @@ #include "config.h" #include +#include +#include namespace spot { @@ -668,4 +670,135 @@ namespace spot { return simplify_acceptance_here(make_twa_graph(aut, twa::prop_set::all())); } + + twa_graph_ptr + reduce_buchi_acceptance_set_here(twa_graph_ptr& aut, bool preserve_sbacc) + { + if (!aut->acc().is_buchi()) + throw std::invalid_argument + ("reduce_buchi_acceptance_set_here() expects a Büchi automaton"); + + if (!preserve_sbacc) + aut->prop_state_acc(trival::maybe()); + aut->prop_weak(trival::maybe()); // issue #562 + + // For each accepting edge in the automaton, we will test if the + // acceptance mark can be removed. To test this, we have to make + // sure that no accepting cycle depends exclusively on this mark. + // We do so by temporary changing the mark of the current edge to + // {1}, and then using the following acceptance condition to + // ensure that there is no cycle that pass through {1} when we + // ignore all other edges with {0}. + acc_cond testacc = acc_cond(2, (acc_cond::acc_code::fin({0}) & + acc_cond::acc_code::inf({1}))); + + acc_cond::mark_t one{1}; + acc_cond::mark_t zero{0}; + acc_cond::mark_t none{}; + scc_info si(aut, scc_info_options::TRACK_STATES); + + if (!preserve_sbacc || !aut->prop_state_acc()) + // transition-based version + for (auto& e: aut->edges()) + { + if (e.acc == none) // nothing to remove + continue; + unsigned srcscc = si.scc_of(e.src); + if (srcscc != si.scc_of(e.dst)) // transient edge + { + e.acc = none; + } + else + { + e.acc = one; + if (generic_emptiness_check_for_scc(si, srcscc, testacc)) + e.acc = none; + else + e.acc = zero; + } + } + else + // state-based version + for (unsigned s = 0, ns = aut->num_states(); s < ns; ++s) + { + acc_cond::mark_t acc = aut->state_acc_sets(s); + if (acc == none) // nothing to remove + continue; + for (auto& e: aut->out(s)) + e.acc = one; + if (generic_emptiness_check_for_scc(si, si.scc_of(s), testacc)) + acc = none; + for (auto& e: aut->out(s)) + e.acc = acc; + } + return aut; + } + + twa_graph_ptr + enlarge_buchi_acceptance_set_here(twa_graph_ptr& aut, bool preserve_sbacc) + { + if (!aut->acc().is_buchi()) + throw std::invalid_argument + ("enlarge_buchi_acceptance_set_here() expects a Büchi automaton"); + + if (!preserve_sbacc) + aut->prop_state_acc(trival::maybe()); + aut->prop_weak(trival::maybe()); // issue #562 + + // For each edge not marked as accepting will test if an + // acceptance mark can be added. To test this, we have to make + // sure that no rejecting cycle goes through this edge. + // We do so my temporary changing the mark of the current edge to + // {1}, and then using the following acceptance condition to + // ensure that there is no accepting cycle that pass through {1} + // when we ignore all other edges with {0}. + acc_cond testacc = + acc_cond(2, acc_cond::acc_code::fin({0}) & acc_cond::acc_code::inf({1})); + + acc_cond::mark_t one{1}; + acc_cond::mark_t zero{0}; + acc_cond::mark_t none{}; + scc_info si(aut, scc_info_options::TRACK_STATES); + + if (!preserve_sbacc || !aut->prop_state_acc()) + // transition-based version + for (auto& e: aut->edges()) + { + if (e.acc == zero) // nothing to add + continue; + unsigned srcscc = si.scc_of(e.src); + if (si.is_rejecting_scc(srcscc)) // nothing to add + continue; + if (srcscc != si.scc_of(e.dst)) // transient edge + { + e.acc = zero; + } + else + { + e.acc = one; + if (generic_emptiness_check_for_scc(si, srcscc, testacc)) + e.acc = zero; + else + e.acc = none; + } + } + else + // state-based version + for (unsigned s = 0, ns = aut->num_states(); s < ns; ++s) + { + acc_cond::mark_t acc = aut->state_acc_sets(s); + if (acc == zero) // nothing to add + continue; + unsigned srcscc = si.scc_of(s); + if (si.is_rejecting_scc(srcscc)) // nothing to add + continue; + for (auto& e: aut->out(s)) + e.acc = one; + if (generic_emptiness_check_for_scc(si, srcscc, testacc)) + acc = zero; + for (auto& e: aut->out(s)) + e.acc = acc; + } + return aut; + } } diff --git a/spot/twaalgos/cleanacc.hh b/spot/twaalgos/cleanacc.hh index 3c2c38070..a3055c1eb 100644 --- a/spot/twaalgos/cleanacc.hh +++ b/spot/twaalgos/cleanacc.hh @@ -70,4 +70,32 @@ namespace spot SPOT_API twa_graph_ptr simplify_acceptance(const_twa_graph_ptr aut); /// @} + + /// \ingroup twa_acc_transform + /// \brief Reduce the acceptance set of a Büchi automaton + /// + /// Iterate over all accepting transitions, and remove them from the + /// acceptance set if this does not change the language. + /// + /// This modifies the automaton in place. + /// + /// If the input has state-based acceptance, it might lose it, + /// unless \a preserve_sbacc is set. + SPOT_API twa_graph_ptr + reduce_buchi_acceptance_set_here(twa_graph_ptr& aut, + bool preserve_sbacc = false); + + /// \ingroup twa_acc_transform + /// \brief Enlarge the acceptance set of a Büchi automaton + /// + /// Iterate over all accepting transitions, and add them to the + /// acceptance set if this cannot change the language. + /// + /// This modifies the automaton in place. + /// + /// If the input has state-based acceptance, it might lose it, + /// unless \a preserve_sbacc is set. + SPOT_API twa_graph_ptr + enlarge_buchi_acceptance_set_here(twa_graph_ptr& aut, + bool preserve_sbacc = false); } diff --git a/tests/Makefile.am b/tests/Makefile.am index ebee91fa9..0c3c995c5 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -224,6 +224,7 @@ TESTS_twa = \ core/568.test \ core/acc.test \ core/acc2.test \ + core/basetred.test \ core/bdddict.test \ core/cube.test \ core/alternating.test \ diff --git a/tests/core/basetred.test b/tests/core/basetred.test new file mode 100755 index 000000000..a7f07d872 --- /dev/null +++ b/tests/core/basetred.test @@ -0,0 +1,116 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +set -e + +genaut --cycle-log-nba=3 > in1.hoa +test 3 -eq `grep -c '{0}' in1.hoa` +autfilt --reduce-acceptance-set in1.hoa > out1.hoa +autfilt --enlarge-acceptance-set in1.hoa > out1l.hoa +autfilt --reduce-acceptance-set out1l.hoa > out1r.hoa +autfilt --enlarge-acceptance-set out1r.hoa > out1rl.hoa +test 1 -eq `grep -c '{0}' out1.hoa` +test 9 -eq `grep -c '{0}' out1l.hoa` +test 1 -eq `grep -c '{0}' out1r.hoa` +diff out1l.hoa out1rl.hoa +autfilt --reduce-acceptance-set -S in1.hoa > out1b.hoa +autfilt --enlarge-acceptance-set -S in1.hoa > out1lb.hoa +autfilt --enlarge-acceptance-set -S out1b.hoa > out1lbb.hoa +test 1 -eq `grep -c '{0}' out1b.hoa` +test 3 -eq `grep -c '{0}' out1lb.hoa` +test 3 -eq `grep -c '{0}' out1lbb.hoa` +diff out1.hoa out1b.hoa +diff out1lb.hoa out1lbb.hoa + +cat >in2.hoa < out2.hoa +autfilt --reduce-acceptance-set -S in2.hoa > out2b.hoa +autfilt --enlarge-acceptance-set out2.hoa > out2l.hoa +autfilt --enlarge-acceptance-set -S out2b.hoa > out2bl.hoa + +cat >ex2.hoa <ex2b.hoa <