Commit dcad10fc authored by Alexandre Lewkowicz's avatar Alexandre Lewkowicz Committed by Alexandre Duret-Lutz

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.
parent 727c3516
...@@ -78,6 +78,7 @@ Exit status:\n\ ...@@ -78,6 +78,7 @@ Exit status:\n\
#define OPT_MASK_ACC 17 #define OPT_MASK_ACC 17
#define OPT_SBACC 18 #define OPT_SBACC 18
#define OPT_STRIPACC 19 #define OPT_STRIPACC 19
#define OPT_KEEP_STATES 20
static const argp_option options[] = static const argp_option options[] =
{ {
...@@ -114,6 +115,9 @@ static const argp_option options[] = ...@@ -114,6 +115,9 @@ static const argp_option options[] =
{ "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
{ "strip-acceptance", OPT_STRIPACC, 0, 0, { "strip-acceptance", OPT_STRIPACC, 0, 0,
"remove the acceptance conditions and all acceptance sets", 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 }, { 0, 0, 0, 0, "Filtering options:", 6 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
...@@ -185,6 +189,8 @@ static bool opt_sbacc = false; ...@@ -185,6 +189,8 @@ static bool opt_sbacc = false;
static bool opt_stripacc = false; static bool opt_stripacc = false;
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr; static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
static spot::acc_cond::mark_t opt_mask_acc = 0U; static spot::acc_cond::mark_t opt_mask_acc = 0U;
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
static int static int
parse_opt(int key, char* arg, struct argp_state*) parse_opt(int key, char* arg, struct argp_state*)
...@@ -258,23 +264,33 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -258,23 +264,33 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case OPT_MASK_ACC: case OPT_MASK_ACC:
{ {
while (*arg) for (auto res : to_longs(arg))
{ {
char* endptr;
long res = strtol(arg, &endptr, 10);
if (res < 0) if (res < 0)
error(2, 0, "acceptance sets should be non-negative:" error(2, 0, "acceptance sets should be non-negative:"
" --mask-acc=%ld", res); " --mask-acc=%ld", res);
if (static_cast<unsigned long>(res) if (static_cast<unsigned long>(res)
> sizeof(spot::acc_cond::mark_t::value_t)) > 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); " acceptance sets: --mask-acc=%ld", res);
opt_mask_acc.set(res); opt_mask_acc.set(res);
if (endptr == arg) }
error(2, 0, "failed to parse '%s' as an integer.", arg); break;
while (*endptr == ' ' || *endptr == ',') }
++endptr; case OPT_KEEP_STATES:
arg = endptr; {
std::vector<long> 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<unsigned long>(res))
opt_keep_states.resize(res + 1, false);
opt_keep_states[res] = true;
} }
break; break;
} }
...@@ -405,6 +421,8 @@ namespace ...@@ -405,6 +421,8 @@ namespace
// Postprocessing. // Postprocessing.
if (!opt_keep_states.empty())
aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
if (opt_mask_acc) if (opt_mask_acc)
aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
......
...@@ -44,4 +44,25 @@ namespace spot ...@@ -44,4 +44,25 @@ namespace spot
return res; return res;
} }
tgba_digraph_ptr mask_keep_states(const const_tgba_digraph_ptr& in,
std::vector<bool>& 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;
}
} }
...@@ -36,11 +36,12 @@ namespace spot ...@@ -36,11 +36,12 @@ namespace spot
/// the transitions. Set the condition to bddfalse to remove it /// the transitions. Set the condition to bddfalse to remove it
/// (this will also remove the destination state and its descendants /// (this will also remove the destination state and its descendants
/// if they are not reachable by another transition). /// if they are not reachable by another transition).
/// \param init The optional new initial state.
template<typename Trans> template<typename Trans>
void transform_mask(const const_tgba_digraph_ptr& old, void transform_mask(const const_tgba_digraph_ptr& old,
tgba_digraph_ptr& cpy, tgba_digraph_ptr& cpy,
Trans trans) Trans trans, unsigned int init)
{ {
std::vector<unsigned> todo; std::vector<unsigned> todo;
std::vector<unsigned> seen(old->num_states(), -1U); std::vector<unsigned> seen(old->num_states(), -1U);
...@@ -58,7 +59,7 @@ namespace spot ...@@ -58,7 +59,7 @@ namespace spot
return tmp; return tmp;
}; };
new_state(old->get_init_state_number()); cpy->set_init_state(new_state(init));
while (!todo.empty()) while (!todo.empty())
{ {
unsigned old_src = todo.back(); unsigned old_src = todo.back();
...@@ -81,11 +82,28 @@ namespace spot ...@@ -81,11 +82,28 @@ namespace spot
} }
} }
template<typename Trans>
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. /// \brief Remove all transitions that are in some given acceptance sets.
SPOT_API SPOT_API
tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in,
acc_cond::mark_t to_remove); 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<bool>& to_keep,
unsigned int init);
} }
......
...@@ -76,6 +76,7 @@ TESTS = \ ...@@ -76,6 +76,7 @@ TESTS = \
ltldo.test \ ltldo.test \
ltldo2.test \ ltldo2.test \
maskacc.test \ maskacc.test \
maskkeep.test \
simdet.test \ simdet.test \
sim2.test \ sim2.test \
ltl2tgba.test \ ltl2tgba.test \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
cat >input1 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0}
[1] 2 {1}
State: 1
[0] 2
[0] 3 {1}
State: 2
[1] 1
[1] 3 {0}
State: 3
[0] 3 {0 1}
--END--
EOF
cat >expect1 <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
--END--
EOF
run 0 ../../bin/autfilt --keep-states=0 input1 -H >output
diff output expect1
run 0 ../../bin/autfilt --keep-states=1 input1 -H >output
diff output expect1
cat >expect3 <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0}
[1] 2 {1}
State: 1
[0] 2
State: 2
[1] 1
--END--
EOF
cat >expect4 <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0] 1
State: 1
[1] 0
--END--
EOF
run 0 ../../bin/autfilt --keep-states=0,1,2 input1 -H >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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment