diff --git a/NEWS b/NEWS index 3d6803e13..e16cb623c 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 20306d037..018086289 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -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); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 6a1798f0f..270ccd650 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -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 < ex8.dot +run 0 autfilt --has-exist-branch --dot='sbarf(Lato)' ex8 > ex8.dot cat >expect8.dot< ex9.dot +run 0 autfilt -v --has-exist-branch --dot='baryf(Lato)' ex9 > ex9.dot cat >expect9.dot <