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

autfilt: --count

Browse source 
* src/bin/autfilt.cc: Add a --count option.
* src/tgbatest/randaut.test: Test autfilt's --count and --states.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-15 12:06:34 +01:00
parent cad4d94cc2
commit 0d710f969b
2 changed files with 22 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/bin/autfilt.cc
View file

@ -88,6 +88,7 @@ static const argp_option options[] =
"of the given property)", 0 }, "of the given property)", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 }, { 0, 0, 0, 0, "Output format:", 3 },
{ "count", 'c', 0, 0, "print only a count of matched automata", 0 },
{ "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
{ "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format. Add letters to select " "Output the automaton in HOA format. Add letters to select "
@ -169,9 +170,9 @@ static const struct argp_child children[] =
{ 0, 0, 0, 0 } { 0, 0, 0, 0 }
}; };
static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, Quiet } static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa,
format = Dot; Quiet, Count } format = Dot;
static bool one_match = false; static long int match_count = 0;
static const char* stats = ""; static const char* stats = "";
static const char* hoa_opt = 0; static const char* hoa_opt = 0;
static spot::option_map extra_options; static spot::option_map extra_options;
@ -209,6 +210,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'B': case 'B':
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
break; break;
case 'c':
format = Count;
break;
case 'F': case 'F':
jobs.emplace_back(arg, true); jobs.emplace_back(arg, true);
break; break;
@ -459,7 +463,7 @@ namespace
if (matched == opt_invert) if (matched == opt_invert)
return 0; return 0;
one_match = true; ++match_count;
// Postprocessing. // Postprocessing.
@ -475,6 +479,10 @@ namespace
switch (format) switch (format)
{ {
case Count:
case Quiet:
// Do not output anything.
break;
case Dot: case Dot:
spot::dotty_reachable(std::cout, aut, spot::dotty_reachable(std::cout, aut,
(type == spot::postprocessor::BA) (type == spot::postprocessor::BA)
@ -489,9 +497,6 @@ namespace
case Hoa: case Hoa:
spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
break; break;
case Quiet:
// Do not output anything.
break;
case Spot: case Spot:
spot::tgba_save_reachable(std::cout, aut); spot::tgba_save_reachable(std::cout, aut);
break; break;
@ -579,5 +584,8 @@ main(int argc, char** argv)
{ {
error(2, 0, "%s", e.what()); error(2, 0, "%s", e.what());
} }
return one_match ? 0 : 1;
if (format == Count)
std::cout << match_count << std::endl;
return !match_count;
} }

6
src/tgbatest/randaut.test
View file

@ -23,6 +23,7 @@
set -e set -e
randaut=../../bin/randaut randaut=../../bin/randaut
autfilt=../../bin/autfilt
$randaut --spin -S4 a b | ../ltl2tgba -H -XN - >out $randaut --spin -S4 a b | ../ltl2tgba -H -XN - >out
grep 'States: 4' out grep 'States: 4' out
@ -46,3 +47,8 @@ grep 'ba.*incompatible' stderr
$randaut --ba -A0 3 2>stderr && exit 1 $randaut --ba -A0 3 2>stderr && exit 1
grep 'ba.*incompatible' stderr grep 'ba.*incompatible' stderr
$randaut --states 10..20 2 -n 100 -H > aut.hoa
a=`$autfilt --states=..14 -c <aut.hoa`
b=`$autfilt aut.hoa --states=15.. -c`
test `expr $a + $b` = 100