diff --git a/NEWS b/NEWS index 9406f3253..854efcb38 100644 --- a/NEWS +++ b/NEWS @@ -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. + * autfilt now has a --ap=RANGE option to filter automata by number + of atomic propositions. + Library: * Building products with different dictionaries now raise an diff --git a/bin/autfilt.cc b/bin/autfilt.cc index af81f5fd8..e0f20d125 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -69,6 +69,7 @@ Exit status:\n\ // Keep this list sorted enum { OPT_ACC_SETS = 256, + OPT_AP_N, OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, OPT_CNF_ACC, @@ -185,6 +186,8 @@ static const argp_option options[] = " automata)", 0 }, /**************************************************/ { 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, "keep automata that are isomorphic to the automaton in FILENAME", 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::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; +static range opt_ap_n = { 0, std::numeric_limits::max() }; static int opt_max_count = -1; static bool opt_destut = false; 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); } break; + case OPT_AP_N: + opt_ap_n = parse_range(arg, 0, std::numeric_limits::max()); + break; case OPT_ACC_SETS: opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -618,6 +625,7 @@ namespace matched &= opt_states.contains(aut->num_states()); matched &= opt_edges.contains(aut->num_edges()); matched &= opt_accsets.contains(aut->acc().num_sets()); + matched &= opt_ap_n.contains(aut->ap().size()); if (opt_is_complete) matched &= is_complete(aut); if (opt_is_deterministic) diff --git a/tests/core/readsave.test b/tests/core/readsave.test index a0eb63e59..83617a021 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1005,3 +1005,5 @@ digraph G { } EOF diff output9 expected9 + +test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`