diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 9dcd33ce4..4f0a11d42 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -46,6 +46,7 @@ #include "tgbaalgos/randomize.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" +#include "tgbaalgos/mask.hh" static const char argp_program_doc[] ="\ @@ -72,6 +73,7 @@ Exit status:\n\ #define OPT_INSTUT 14 #define OPT_IS_EMPTY 15 #define OPT_INTERSECT 16 +#define OPT_MASK_ACC 17 static const argp_option options[] = { @@ -125,6 +127,8 @@ static const argp_option options[] = "keep automata whose number of edges are in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets are in RANGE", 0 }, + { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0, + "remove all transitions in specified acceptance sets", 0 }, RANGE_DOC_FULL, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, @@ -169,6 +173,7 @@ static bool opt_destut = false; static char opt_instut = 0; static bool opt_is_empty = false; static std::unique_ptr opt_uniq = nullptr; +static spot::acc_cond::mark_t opt_mask_acc = 0U; static int parse_opt(int key, char* arg, struct argp_state*) @@ -240,6 +245,28 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_MERGE: opt_merge = true; break; + case OPT_MASK_ACC: + { + while (*arg) + { + char* endptr; + long res = strtol(arg, &endptr, 10); + if (res < 0) + error(2, 0, "acceptance sets should be non-negative:" + " --mask-acc=%ld", res); + if (static_cast(res) + > sizeof(spot::acc_cond::mark_t::value_t)) + error(2, 0, "this implementation does not support that much" + " acceptance sets: --mask-acc=%ld", res); + opt_mask_acc.set(res); + if (endptr == arg) + error(2, 0, "failed to parse '%s' as an integer.", arg); + while (*endptr == ' ' || *endptr == ',') + ++endptr; + arg = endptr; + } + break; + } case OPT_PRODUCT: { auto a = read_automaton(arg, dict); @@ -359,6 +386,9 @@ namespace // Postprocessing. + if (opt_mask_acc) + aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); + if (opt_destut) aut = spot::closure(std::move(aut)); if (opt_instut == 1) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 52fc788ae..8af7e0646 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de // l'Epita. // // This file is part of Spot, a model checking library. @@ -96,6 +96,11 @@ namespace spot return id & (1U << u); } + void set(unsigned u) + { + id |= (1U << u); + } + mark_t& operator&=(mark_t r) { id &= r.id; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index afa45edd3..e80793e76 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -50,6 +50,7 @@ tgbaalgos_HEADERS = \ ltl2taa.hh \ ltl2tgba_fm.hh \ magic.hh \ + mask.hh \ minimize.hh \ neverclaim.hh \ postproc.hh \ @@ -100,6 +101,7 @@ libtgbaalgos_la_SOURCES = \ ltl2taa.cc \ ltl2tgba_fm.cc \ magic.cc \ + mask.cc \ minimize.cc \ ndfs_result.hxx \ neverclaim.cc \ diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc new file mode 100644 index 000000000..7d9e0f476 --- /dev/null +++ b/src/tgbaalgos/mask.cc @@ -0,0 +1,47 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// 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 "mask.hh" + +namespace spot +{ + tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, + acc_cond::mark_t to_remove) + { + auto& inacc = in->acc(); + auto res = make_tgba_digraph(in->get_dict()); + res->copy_ap_of(in); + res->prop_copy(in, { true, false, true, true }); + unsigned na = inacc.num_sets(); + unsigned tr = to_remove.count(); + assert(tr <= na); + res->set_acceptance_conditions(na - tr); + transform_mask(in, res, [&](bdd& cond, + acc_cond::mark_t& acc, + unsigned) + { + if (acc & to_remove) + cond = bddfalse; + else + acc = inacc.strip(acc, to_remove); + }); + return res; + } + +} diff --git a/src/tgbaalgos/mask.hh b/src/tgbaalgos/mask.hh new file mode 100644 index 000000000..6ae57fb3d --- /dev/null +++ b/src/tgbaalgos/mask.hh @@ -0,0 +1,93 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// 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_MASK_HH +# define SPOT_TGBAALGOS_MASK_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// \brief Clone and mask an automaton. + /// + /// Copy the transition of the automaton \a old, into the automaton + /// \a cpy, creating new states at the same time. The argument \a + /// trans should behave as a fonction with the following prototype: + /// + /// void (*trans) (bdd& cond, acc_cond::mark_t& acc, unsigned dst) + /// + /// It can modify either the condition or the acceptance sets of + /// the transitions. Set the condition to bddfalse to remove it + /// (this will also remove the destination state and its descendants + /// if they are not reachable by another transition). + + template + void transform_mask(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans) + { + std::vector todo; + std::vector seen(old->num_states(), -1U); + + auto new_state = + [&](unsigned old_state) -> unsigned + { + unsigned tmp = seen[old_state]; + if (tmp == -1U) + { + tmp = cpy->new_state(); + seen[old_state] = tmp; + todo.push_back(old_state); + } + return tmp; + }; + + new_state(old->get_init_state_number()); + while (!todo.empty()) + { + unsigned old_src = todo.back(); + todo.pop_back(); + + unsigned new_src = seen[old_src]; + assert(new_src != -1U); + + for (auto& t: old->out(old_src)) + { + bdd cond = t.cond; + acc_cond::mark_t acc = t.acc; + trans(cond, acc, t.dst); + + if (cond != bddfalse) + cpy->new_transition(new_src, + new_state(t.dst), + cond, acc); + } + } + } + + /// \brief Remove all transitions that are in some given acceptance sets. + SPOT_API + tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, + acc_cond::mark_t to_remove); + + +} + + +#endif // SPOT_TGBAALGOS_MASK_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 7f51380be..e93042392 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -40,7 +40,6 @@ check_PROGRAMS = \ intvcomp \ intvcmp2 \ ltlprod \ - maskacc \ readsat \ taatgba @@ -55,7 +54,6 @@ intvcomp_SOURCES = intvcomp.cc intvcmp2_SOURCES = intvcmp2.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc -maskacc_SOURCES = maskacc.cc randtgba_SOURCES = randtgba.cc readsat_SOURCES = readsat.cc taatgba_SOURCES = taatgba.cc diff --git a/src/tgbatest/maskacc.cc b/src/tgbatest/maskacc.cc deleted file mode 100755 index 875d27aad..000000000 --- a/src/tgbatest/maskacc.cc +++ /dev/null @@ -1,67 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 -#include -#include -#include "tgbaparse/public.hh" -#include "tgbaalgos/save.hh" -#include "tgba/tgbamask.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " file" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc != 2) - syntax(argv[0]); - - { - auto dict = spot::make_bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel; - auto aut = spot::tgba_parse(argv[1], pel, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel)) - return 2; - - unsigned nsets = aut->acc().num_sets(); - - for (unsigned n = 0; n < nsets; ++n) - { - auto masked = spot::build_tgba_mask_acc_ignore(aut, n); - spot::tgba_save_reachable(std::cout, masked); - } - } - - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::bunop::instance_count() == 0); - assert(spot::ltl::atomic_prop::instance_count() == 0); - return exit_code; -} diff --git a/src/tgbatest/maskacc.test b/src/tgbatest/maskacc.test index 01a65365a..586c60a93 100755 --- a/src/tgbatest/maskacc.test +++ b/src/tgbatest/maskacc.test @@ -24,28 +24,94 @@ set -e cat >input1 <expect1 <output +diff output expect1 + +cat >expect2 <output +diff output expect2 + +cat >expect3 <output +diff output expect3 + +run 0 ../../bin/autfilt --mask-acc=0 --mask-acc=1 input1 -H >output +diff output expect3 + +# Errors +run 2 ../../bin/autfilt --mask-acc=a3 input1 +run 2 ../../bin/autfilt --mask-acc=3-2 input1 +run 2 ../../bin/autfilt --mask-acc=0,9999,1 input1