From dcad10fc68de5a5f8c7f4672956a4963c33142c9 Mon Sep 17 00:00:00 2001 From: Alexandre Lewkowicz Date: Thu, 12 Feb 2015 14:49:37 +0100 Subject: [PATCH] maskkeep: Add a tgba_digraph version * src/bin/autfilt.cc: Add option --keep-states. * src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh: Keep the selected states and update the initial state. * src/tgbatest/Makefile.am: Adjust. * src/tgbatest/maskkeep.test: New file. --- src/bin/autfilt.cc | 36 +++++++++--- src/tgbaalgos/mask.cc | 21 +++++++ src/tgbaalgos/mask.hh | 22 +++++++- src/tgbatest/Makefile.am | 1 + src/tgbatest/maskkeep.test | 113 +++++++++++++++++++++++++++++++++++++ 5 files changed, 182 insertions(+), 11 deletions(-) create mode 100755 src/tgbatest/maskkeep.test diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 65297e239..e5559d653 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -78,6 +78,7 @@ Exit status:\n\ #define OPT_MASK_ACC 17 #define OPT_SBACC 18 #define OPT_STRIPACC 19 +#define OPT_KEEP_STATES 20 static const argp_option options[] = { @@ -114,6 +115,9 @@ static const argp_option options[] = { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, { "strip-acceptance", OPT_STRIPACC, 0, 0, "remove the acceptance conditions and all acceptance sets", 0 }, + { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0, + "only keep specified states. The first state will be the new "\ + "initial state", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -185,6 +189,8 @@ static bool opt_sbacc = false; static bool opt_stripacc = false; static std::unique_ptr opt_uniq = nullptr; static spot::acc_cond::mark_t opt_mask_acc = 0U; +static std::vector opt_keep_states = {}; +static unsigned int opt_keep_states_initial = 0; static int parse_opt(int key, char* arg, struct argp_state*) @@ -258,23 +264,33 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_MASK_ACC: { - while (*arg) + for (auto res : to_longs(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" + error(2, 0, "this implementation does not support that many" " 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_KEEP_STATES: + { + std::vector values = to_longs(arg); + if (!values.empty()) + opt_keep_states_initial = values[0]; + for (auto res : values) + { + if (res < 0) + error(2, 0, "state ids should be non-negative:" + " --mask-acc=%ld", res); + // We don't know yet how many states the automata contain. + if (opt_keep_states.size() <= static_cast(res)) + opt_keep_states.resize(res + 1, false); + opt_keep_states[res] = true; } break; } @@ -405,6 +421,8 @@ namespace // Postprocessing. + if (!opt_keep_states.empty()) + aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial); if (opt_mask_acc) aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index 7d9e0f476..a769f2d3a 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -44,4 +44,25 @@ namespace spot return res; } + tgba_digraph_ptr mask_keep_states(const const_tgba_digraph_ptr& in, + std::vector& to_keep, + unsigned int init) + { + if (to_keep.size() < in->num_states()) + to_keep.resize(in->num_states(), false); + + auto res = make_tgba_digraph(in->get_dict()); + res->copy_ap_of(in); + res->prop_copy(in, { true, true, true, true }); + res->copy_acceptance_conditions_of(in); + transform_mask(in, res, [&](bdd& cond, + acc_cond::mark_t&, + unsigned dst) + { + if (!to_keep[dst]) + cond = bddfalse; + }, init); + return res; + } + } diff --git a/src/tgbaalgos/mask.hh b/src/tgbaalgos/mask.hh index 6ae57fb3d..4e9eb42a0 100644 --- a/src/tgbaalgos/mask.hh +++ b/src/tgbaalgos/mask.hh @@ -36,11 +36,12 @@ namespace spot /// 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). + /// \param init The optional new initial state. template void transform_mask(const const_tgba_digraph_ptr& old, tgba_digraph_ptr& cpy, - Trans trans) + Trans trans, unsigned int init) { std::vector todo; std::vector seen(old->num_states(), -1U); @@ -58,7 +59,7 @@ namespace spot return tmp; }; - new_state(old->get_init_state_number()); + cpy->set_init_state(new_state(init)); while (!todo.empty()) { unsigned old_src = todo.back(); @@ -81,11 +82,28 @@ namespace spot } } + template + void transform_mask(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans) + { + transform_mask(old, cpy, trans, old->get_init_state_number()); + } + /// \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); + /// \brief Keep only the states as specified by \a to_keep. + /// + /// Each index in the vector \a to_keep specifies wether or not to keep that + /// state. The initial state will be set to \a init. + SPOT_API + tgba_digraph_ptr mask_keep_states(const const_tgba_digraph_ptr& in, + std::vector& to_keep, + unsigned int init); + } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index dd2307e65..2eed6c2da 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -76,6 +76,7 @@ TESTS = \ ltldo.test \ ltldo2.test \ maskacc.test \ + maskkeep.test \ simdet.test \ sim2.test \ ltl2tgba.test \ diff --git a/src/tgbatest/maskkeep.test b/src/tgbatest/maskkeep.test new file mode 100755 index 000000000..3ad825795 --- /dev/null +++ b/src/tgbatest/maskkeep.test @@ -0,0 +1,113 @@ +#!/bin/sh +# -*- 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 . + + +. ./defs + +set -e + +cat >input1 <expect1 <output +diff output expect1 + +run 0 ../../bin/autfilt --keep-states=1 input1 -H >output +diff output expect1 + +cat >expect3 <expect4 <output +diff output expect3 +run 0 ../../bin/autfilt --keep-states=0,9999,1,2 input1 -H >output +diff output expect3 + +run 0 ../../bin/autfilt --keep-states=1,2,0 input1 -H >output +diff output expect4 + +# Errors +run 2 ../../bin/autfilt --keep-states=a3 input1 +run 2 ../../bin/autfilt --keep-states=3-2 input1