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

autfilt: implement --has-univ-branching and --has-exist-branching

Browse source 
Fixes #352.

* bin/autfilt.cc: Add the options.
* tests/core/alternating.test: Test them.
* NEWS: Mention them.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-03 19:21:15 +02:00
parent 939f63eec9
commit 2e50f9e986
3 changed files with 28 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -12,6 +12,10 @@ New in spot 2.5.3.dev (not yet released)
- autfilt learned --is-colored to filter automata that use
exactly one acceptance set per mark or transition.
- autfilt learned --has-univ-branching and --has-exist-branching
to keep automata that have universal branching, or that make
non-deterministic choices.
- ltlcross, ltldo, and autcross learned shorthands to call
delag, ltl2dra, ltl2dgra, and nba2dpa.

19
bin/autfilt.cc
View file

@ -104,6 +104,8 @@ enum {
OPT_EXCLUSIVE_AP,
OPT_GENERALIZED_RABIN,
OPT_GENERALIZED_STREETT,
OPT_HAS_EXIST_BRANCHING,
OPT_HAS_UNIV_BRANCHING,
OPT_HIGHLIGHT_NONDET,
OPT_HIGHLIGHT_NONDET_EDGES,
OPT_HIGHLIGHT_NONDET_STATES,
@ -187,6 +189,11 @@ static const argp_option options[] =
{ "unique", 'u', nullptr, 0,
"do not output the same automaton twice (same in the sense that they "
"are isomorphic)", 0 },
{ "has-exist-branching", OPT_HAS_EXIST_BRANCHING, nullptr, 0,
"keep automata that use existential branching (i.e., make "
"non-deterministic choices)", 0 },
{ "has-univ-branching", OPT_HAS_UNIV_BRANCHING, nullptr, 0,
"keep alternating automata that use universal branching", 0 },
{ "is-colored", OPT_IS_COLORED, nullptr, 0,
"keep colored automata (i.e., exactly one acceptance mark per "
"transition or state)", 0 },
@ -560,6 +567,8 @@ static struct opt_t
}* opt;
static bool opt_merge = false;
static bool opt_has_univ_branching = false;
static bool opt_has_exist_branching = false;
static bool opt_is_alternating = false;
static bool opt_is_colored = false;
static bool opt_is_complete = false;
@ -829,6 +838,12 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_gsa = GSA_UNIQUE_FIN;
opt_gra = GRA_NO;
break;
case OPT_HAS_EXIST_BRANCHING:
opt_has_exist_branching = true;
break;
case OPT_HAS_UNIV_BRANCHING:
opt_has_univ_branching = true;
break;
case OPT_HIGHLIGHT_NONDET:
{
int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1;
@ -1363,6 +1378,10 @@ namespace
}
if (opt_nondet_states_set)
matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
if (opt_has_univ_branching)
matched &= !aut->is_existential();
if (opt_has_exist_branching)
matched &= !is_universal(aut);
if (opt_is_deterministic)
{
matched &= is_deterministic(aut);

8
tests/core/alternating.test
View file

@ -53,7 +53,7 @@ State: 6 "t"
--END--
EOF
autfilt --dot=bans alt.hoa >alt.dot
autfilt --has-univ-branch --has-exist-branch --dot=bans alt.hoa >alt.dot
cat >expect.dot <<EOF
digraph "" {
@ -267,6 +267,8 @@ State: 2
--END--
EOF
autfilt --has-exist-branch ex3 && exit 1
autfilt -q --equivalent-to=ex1 ex2
autfilt -q --included-in=ex1 ex2
autfilt -q --equivalent-to=ex1 ex3 && exit 1
@ -654,7 +656,7 @@ State: 4 "t"
--END--
EOF
run 0 autfilt --dot='sbarf(Lato)' ex8 > ex8.dot
run 0 autfilt --has-exist-branch --dot='sbarf(Lato)' ex8 > ex8.dot
cat >expect8.dot<<EOF
digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" {
@ -734,7 +736,7 @@ State: 2
--END--
EOF
run 0 autfilt --dot='baryf(Lato)' ex9 > ex9.dot
run 0 autfilt -v --has-exist-branch --dot='baryf(Lato)' ex9 > ex9.dot
cat >expect9.dot <<EOF
digraph "" {