alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

autfilt: implement an --ap=RANGE option

Browse source 
Fixes #130.

* bin/autfilt.cc: Implement the option.
* NEWS: Mention it.
* tests/core/readsave.test: Add a short test.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-15 14:29:00 +01:00
parent beb435ebd8
commit 199e5fd2e0
3 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -50,6 +50,9 @@ New in spot 1.99.7a (not yet released)
* ltlfilt's option --ap=N can now take a RANGE as parameter. * ltlfilt's option --ap=N can now take a RANGE as parameter.
* autfilt now has a --ap=RANGE option to filter automata by number
of atomic propositions.
Library: Library:
* Building products with different dictionaries now raise an * Building products with different dictionaries now raise an

8
bin/autfilt.cc
View file

@ -69,6 +69,7 @@ Exit status:\n\
// Keep this list sorted // Keep this list sorted
enum { enum {
OPT_ACC_SETS = 256, OPT_ACC_SETS = 256,
OPT_AP_N,
OPT_ARE_ISOMORPHIC, OPT_ARE_ISOMORPHIC,
OPT_CLEAN_ACC, OPT_CLEAN_ACC,
OPT_CNF_ACC, OPT_CNF_ACC,
@ -185,6 +186,8 @@ static const argp_option options[] =
" automata)", 0 }, " automata)", 0 },
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Filtering options:", 6 }, { nullptr, 0, nullptr, 0, "Filtering options:", 6 },
{ "ap", OPT_AP_N, "RANGE", 0,
"match automata with a number of atomic propositions in RANGE", 0 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
"keep automata that are isomorphic to the automaton in FILENAME", 0 }, "keep automata that are isomorphic to the automaton in FILENAME", 0 },
{ "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 }, { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
@ -289,6 +292,7 @@ static bool opt_invert = false;
static range opt_states = { 0, std::numeric_limits<int>::max() }; static range opt_states = { 0, std::numeric_limits<int>::max() };
static range opt_edges = { 0, std::numeric_limits<int>::max() }; static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() }; static range opt_accsets = { 0, std::numeric_limits<int>::max() };
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
static int opt_max_count = -1; static int opt_max_count = -1;
static bool opt_destut = false; static bool opt_destut = false;
static char opt_instut = 0; static char opt_instut = 0;
@ -351,6 +355,9 @@ parse_opt(int key, char* arg, struct argp_state*)
error(2, 0, "failed to parse --options near '%s'", opt); error(2, 0, "failed to parse --options near '%s'", opt);
} }
break; break;
case OPT_AP_N:
opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case OPT_ACC_SETS: case OPT_ACC_SETS:
opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max()); opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
break; break;
@ -618,6 +625,7 @@ namespace
matched &= opt_states.contains(aut->num_states()); matched &= opt_states.contains(aut->num_states());
matched &= opt_edges.contains(aut->num_edges()); matched &= opt_edges.contains(aut->num_edges());
matched &= opt_accsets.contains(aut->acc().num_sets()); matched &= opt_accsets.contains(aut->acc().num_sets());
matched &= opt_ap_n.contains(aut->ap().size());
if (opt_is_complete) if (opt_is_complete)
matched &= is_complete(aut); matched &= is_complete(aut);
if (opt_is_deterministic) if (opt_is_deterministic)

2
tests/core/readsave.test
View file

@ -1005,3 +1005,5 @@ digraph G {
} }
EOF EOF
diff output9 expected9 diff output9 expected9
test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`