diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d3e66a4e3..9e99356ad 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -73,6 +73,8 @@ Exit status:\n\ #define OPT_STATES 17 #define OPT_COUNT 18 #define OPT_NAME 19 +#define OPT_EDGES 20 +#define OPT_ACC_SETS 21 static const argp_option options[] = { @@ -160,6 +162,10 @@ static const argp_option options[] = { "invert-match", 'v', 0, 0, "select non-matching automata", 0 }, { "states", OPT_STATES, "RANGE", 0, "keep automata whose number of states are in RANGE", 0 }, + { "edges", OPT_EDGES, "RANGE", 0, + "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 }, RANGE_DOC_FULL, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, @@ -194,6 +200,8 @@ static bool opt_is_complete = false; static bool opt_is_deterministic = false; 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 const char* opt_name = nullptr; static int opt_max_count = -1; @@ -265,6 +273,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_DOT: format = Dot; break; + case OPT_ACC_SETS: + opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); + break; case OPT_ARE_ISOMORPHIC: { spot::hoa_parse_error_list pel; @@ -275,6 +286,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_are_isomorphic = std::move(p->aut); break; } + case OPT_EDGES: + opt_edges = parse_range(arg, 0, std::numeric_limits::max()); + break; case OPT_IS_COMPLETE: opt_is_complete = true; break; @@ -500,6 +514,8 @@ namespace bool matched = true; matched &= opt_states.contains(aut->num_states()); + matched &= opt_edges.contains(aut->num_transitions()); + matched &= opt_accsets.contains(aut->acc().num_sets()); if (opt_is_complete) matched &= is_complete(aut); if (opt_is_deterministic) diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 3683cf2ba..cb1331c7e 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -111,18 +111,18 @@ diff stdout stdout2 # stop after 10 automata. $randltl -n -1 a b | $ltl2tgba -H -F - | - $autfilt -F- -F nonexistant --states=3 \ - --name='%M, %S states' --stats='<%m>, %t' -n 10 > output + $autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \ + --name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output cat >expected <, 13 -, 6 -, 6 -, 6 -, 13 -, 14 -, 6 -, 4 -, 9 -, 13 +, 6, 1 +, 4, 1 +, 4, 1 +, 4, 1 +, 6, 1 +, 6, 1 +, 5, 1 +, 4, 1 +, 4, 1 +, 7, 1 EOF diff output expected