diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 1a22f2b11..d3e66a4e3 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -98,6 +98,8 @@ static const argp_option options[] = { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, + { "max-count", 'n', "NUM", 0, + "output at most NUM automata", 0 }, { "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL, "set the name of the output automaton (default: %M)", 0 }, { "quiet", 'q', 0, 0, "suppress all normal output", 0 }, @@ -193,6 +195,7 @@ static bool opt_is_deterministic = false; static bool opt_invert = false; static range opt_states = { 0, std::numeric_limits::max() }; static const char* opt_name = nullptr; +static int opt_max_count = -1; static int to_int(const char* s) @@ -204,6 +207,15 @@ to_int(const char* s) return res; } +static int +to_pos_int(const char* s) +{ + int res = to_int(s); + if (res < 0) + error(2, 0, "%d is not positive", res); + return res; +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -229,6 +241,9 @@ parse_opt(int key, char* arg, struct argp_state*) case 'M': type = spot::postprocessor::Monitor; break; + case 'n': + opt_max_count = to_pos_int(arg); + break; case 'q': format = Quiet; break; @@ -550,6 +565,10 @@ namespace break; } flush_cout(); + + if (opt_max_count >= 0 && match_count >= opt_max_count) + abort_run = true; + return 0; } @@ -568,7 +587,7 @@ namespace int err = 0; - for (;;) + while (!abort_run) { pel.clear(); auto haut = hp.parse(pel, dict); diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 4e74b73f9..3683cf2ba 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -106,12 +106,13 @@ run 0 $autfilt --hoa stdout > stdout2 diff stdout stdout2 # Find formula that can be translated into a 3-state automaton, and -# exercise both %M and %m. +# exercise both %M and %m. The nonexistant file should never be +# open, because the input stream is infinite and autfilt should +# stop after 10 automata. $randltl -n -1 a b | $ltl2tgba -H -F - | - $autfilt --states=3 --name='%M, %S states' --stats='<%m>, %t' | - head -n 10 > output -cat output + $autfilt -F- -F nonexistant --states=3 \ + --name='%M, %S states' --stats='<%m>, %t' -n 10 > output cat >expected <, 13 , 6