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

autfilt: --edges --acc-sets

Browse source 
* src/bin/autfilt.cc: Add these new options.
* src/tgbatest/readsave.test: Test them.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-16 15:57:44 +01:00
parent 56caacbf78
commit b8a38915e5
2 changed files with 28 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/bin/autfilt.cc
View file

@ -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<int>::max() };
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::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<int>::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<int>::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)

24
src/tgbatest/readsave.test
View file

@ -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 <<EOF
<F(b | GF!a), 3 states>, 13
<XFb, 3 states>, 6
<XF!b, 3 states>, 6
<G!b & XF!a, 3 states>, 6
<F(b | GFa), 3 states>, 13
<F(Ga | XG(!a & Fb)), 3 states>, 14
<FG!b & F(b | GFb), 3 states>, 6
<Ga | G!a, 3 states>, 4
<a | G((!a & !b) | (a & b)), 3 states>, 9
<Fb U G!a, 3 states>, 13
<F(b | GF!a), 3 states>, 6, 1
<XFb, 3 states>, 4, 1
<XF!b, 3 states>, 4, 1
<G!b & XF!a, 3 states>, 4, 1
<F(b | GFa), 3 states>, 6, 1
<F(Ga | XG(!a & Fb)), 3 states>, 6, 1
<FG!b & F(b | GFb), 3 states>, 5, 1
<Ga | G!a, 3 states>, 4, 1
<a | G((!a & !b) | (a & b)), 3 states>, 4, 1
<Fb U G!a, 3 states>, 7, 1
EOF
diff output expected