diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index acd9bf9f7..336d66828 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -50,6 +50,7 @@ #include "tgbaalgos/sbacc.hh" #include "tgbaalgos/stripacc.hh" #include "tgbaalgos/remfin.hh" +#include "tgbaalgos/cleanacc.hh" static const char argp_program_doc[] ="\ @@ -82,6 +83,7 @@ Exit status:\n\ #define OPT_KEEP_STATES 20 #define OPT_DNF_ACC 21 #define OPT_REM_FIN 22 +#define OPT_CLEAN_ACC 23 static const argp_option options[] = { @@ -125,6 +127,8 @@ static const argp_option options[] = "put the acceptance condition in Disjunctive Normal Form", 0 }, { "remove-fin", OPT_REM_FIN, 0, 0, "rewrite the automaton without using Fin acceptance", 0 }, + { "cleanup-acceptance", OPT_CLEAN_ACC, 0, 0, + "remove unused acceptance sets from the automaton", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -206,6 +210,7 @@ static bool opt_sbacc = false; static bool opt_stripacc = false; static bool opt_dnf_acc = false; static bool opt_rem_fin = false; +static bool opt_clean_acc = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -251,6 +256,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ARE_ISOMORPHIC: opt->are_isomorphic = read_automaton(arg, opt->dict); break; + case OPT_CLEAN_ACC: + opt_clean_acc = true; + break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -421,6 +429,8 @@ namespace if (opt_dnf_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().to_dnf()); + if (opt_clean_acc && !opt_rem_fin) + cleanup_acceptance(aut); if (opt_rem_fin) aut = remove_fin(aut); diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 80699c87a..596fa8de0 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -585,7 +585,7 @@ namespace spot uses_fin_acceptance_ = check_fin_acceptance(); } - acc_code get_acceptance() const + const acc_code& get_acceptance() const { return code_; } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index ffd1561c7..e3d1541d0 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -639,7 +639,7 @@ namespace spot acc_cond acc_; public: - acc_cond::acc_code get_acceptance() const + const acc_cond::acc_code& get_acceptance() const { return acc_.get_acceptance(); } diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 9d32fd470..43234d711 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -31,6 +31,7 @@ tgbaalgos_HEADERS = \ are_isomorphic.hh \ bfssteps.hh \ canonicalize.hh \ + cleanacc.hh \ complete.hh \ compsusp.hh \ cycles.hh \ @@ -84,6 +85,7 @@ libtgbaalgos_la_SOURCES = \ are_isomorphic.cc \ bfssteps.cc \ canonicalize.cc \ + cleanacc.cc \ complete.cc \ compsusp.cc \ cycles.cc \ diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc new file mode 100644 index 000000000..15afecc16 --- /dev/null +++ b/src/tgbaalgos/cleanacc.cc @@ -0,0 +1,135 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita. +// +// 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 . + +#include "tgbaalgos/cleanacc.hh" + +namespace spot +{ + namespace + { + acc_cond::acc_code strip(const acc_cond& acc, + const acc_cond::acc_word* pos, + acc_cond::mark_t useless) + { + auto start = pos - pos->size; + switch (pos->op) + { + case acc_cond::acc_op::And: + { + --pos; + acc_cond::acc_code res; + do + { + auto tmp = strip(acc, pos, useless); + tmp.append_and(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + acc_cond::acc_code res = acc.fin(0); // f + do + { + auto tmp = strip(acc, pos, useless); + tmp.append_or(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + if (pos[-1].mark & useless) + return acc.inf(0U); // t + return acc.fin(acc.strip(pos[-1].mark, useless)); + case acc_cond::acc_op::Inf: + if (pos[-1].mark & useless) + return acc.fin(0U); // f + return acc.inf(acc.strip(pos[-1].mark, useless)); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return acc_cond::acc_code{}; + } + SPOT_UNREACHABLE(); + return acc_cond::acc_code{}; + } + } + + void cleanup_acceptance(tgba_digraph_ptr& aut) + { + auto& acc = aut->acc(); + if (acc.num_sets() == 0) + return; + + auto& c = aut->get_acceptance(); + acc_cond::mark_t used_in_cond = 0U; + if (!c.is_true()) + { + auto pos = &c.back(); + auto end = &c.front(); + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + used_in_cond |= pos[-1].mark; + pos -= 2; + break; + } + } + } + + acc_cond::mark_t used_in_aut = 0U; + for (auto& t: aut->transitions()) + used_in_aut |= t.acc; + + auto useful = used_in_aut & used_in_cond; + + auto useless = acc.comp(useful); + + if (!useless) + return; + + // Remove useless marks from the automaton + for (auto& t: aut->transitions()) + t.acc = acc.strip(t.acc, useless); + + // Remove useless marks from the acceptance condition + acc_cond::acc_code newc; + if (c.is_true() || c.is_false()) + newc = c; + else + newc = strip(acc, &c.back(), useless); + + aut->set_acceptance(useful.count(), newc); + } + +} diff --git a/src/tgbaalgos/cleanacc.hh b/src/tgbaalgos/cleanacc.hh new file mode 100644 index 000000000..c7496d221 --- /dev/null +++ b/src/tgbaalgos/cleanacc.hh @@ -0,0 +1,32 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita. +// +// 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 . + +#ifndef SPOT_TGBAALGOS_CLEANACC_HH +# define SPOT_TGBAALGOS_CLEANACC_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// \brief Remove useless acceptance sets + SPOT_API void + cleanup_acceptance(tgba_digraph_ptr& aut); +} + +#endif // SPOT_TGBAALGOS_CLEANACC_HH diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 03a693360..39dba36d7 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -1394,48 +1394,48 @@ State: 0 EOF -# FIXME: Test removal of useless acceptance sets -# -# # The mapping of acceptance sets for the second automaton is -# # input -> output -# # 0 -> 0 -# # 1 -> removed -# # 2 -> 1 -# # 3 -> removed -# # 4 -> 2 -# # !2 -> 3 -# expectok input < output +# 0 -> 0 +# 1 -> removed +# 2 -> 1 +# 3 -> removed +# 4 -> 2 +# !2 -> 3 +expectok input --cleanup-acc <