autfilt: support -n,--max-count
* src/bin/autfilt.cc: Implement this new option. * src/tgbatest/readsave.test: Test it.
This commit is contained in:
parent
40c457b626
commit
56caacbf78
2 changed files with 25 additions and 5 deletions
|
|
@ -98,6 +98,8 @@ static const argp_option options[] =
|
||||||
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
|
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
|
||||||
"LBTT's format (add =t to force transition-based acceptance even"
|
"LBTT's format (add =t to force transition-based acceptance even"
|
||||||
" on Büchi automata)", 0 },
|
" on Büchi automata)", 0 },
|
||||||
|
{ "max-count", 'n', "NUM", 0,
|
||||||
|
"output at most NUM automata", 0 },
|
||||||
{ "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL,
|
{ "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL,
|
||||||
"set the name of the output automaton (default: %M)", 0 },
|
"set the name of the output automaton (default: %M)", 0 },
|
||||||
{ "quiet", 'q', 0, 0, "suppress all normal output", 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 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 const char* opt_name = nullptr;
|
static const char* opt_name = nullptr;
|
||||||
|
static int opt_max_count = -1;
|
||||||
|
|
||||||
static int
|
static int
|
||||||
to_int(const char* s)
|
to_int(const char* s)
|
||||||
|
|
@ -204,6 +207,15 @@ to_int(const char* s)
|
||||||
return res;
|
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
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state*)
|
parse_opt(int key, char* arg, struct argp_state*)
|
||||||
{
|
{
|
||||||
|
|
@ -229,6 +241,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
case 'M':
|
case 'M':
|
||||||
type = spot::postprocessor::Monitor;
|
type = spot::postprocessor::Monitor;
|
||||||
break;
|
break;
|
||||||
|
case 'n':
|
||||||
|
opt_max_count = to_pos_int(arg);
|
||||||
|
break;
|
||||||
case 'q':
|
case 'q':
|
||||||
format = Quiet;
|
format = Quiet;
|
||||||
break;
|
break;
|
||||||
|
|
@ -550,6 +565,10 @@ namespace
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
flush_cout();
|
flush_cout();
|
||||||
|
|
||||||
|
if (opt_max_count >= 0 && match_count >= opt_max_count)
|
||||||
|
abort_run = true;
|
||||||
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -568,7 +587,7 @@ namespace
|
||||||
|
|
||||||
int err = 0;
|
int err = 0;
|
||||||
|
|
||||||
for (;;)
|
while (!abort_run)
|
||||||
{
|
{
|
||||||
pel.clear();
|
pel.clear();
|
||||||
auto haut = hp.parse(pel, dict);
|
auto haut = hp.parse(pel, dict);
|
||||||
|
|
|
||||||
|
|
@ -106,12 +106,13 @@ run 0 $autfilt --hoa stdout > stdout2
|
||||||
diff stdout stdout2
|
diff stdout stdout2
|
||||||
|
|
||||||
# Find formula that can be translated into a 3-state automaton, and
|
# 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 |
|
$randltl -n -1 a b |
|
||||||
$ltl2tgba -H -F - |
|
$ltl2tgba -H -F - |
|
||||||
$autfilt --states=3 --name='%M, %S states' --stats='<%m>, %t' |
|
$autfilt -F- -F nonexistant --states=3 \
|
||||||
head -n 10 > output
|
--name='%M, %S states' --stats='<%m>, %t' -n 10 > output
|
||||||
cat output
|
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
<F(b | GF!a), 3 states>, 13
|
<F(b | GF!a), 3 states>, 13
|
||||||
<XFb, 3 states>, 6
|
<XFb, 3 states>, 6
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue