Commit 77ce4170 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

autfilt: add --is-alternating

* bin/autfilt.cc: Implement --is-alternating.
* tests/core/complete.test: Test it.
* NEWS: Mention it.
parent 6a11e149
...@@ -11,7 +11,7 @@ New in spot 2.2.2.dev (Not yet released) ...@@ -11,7 +11,7 @@ New in spot 2.2.2.dev (Not yet released)
alternating automata, but in any case they should display a alternating automata, but in any case they should display a
diagnostic: if you see a crash, please report it. diagnostic: if you see a crash, please report it.
* autfilt has a new --is-very-weak filter. * autfilt has two new filters: --is-very-weak and --is-alternating.
Library: Library:
......
...@@ -102,15 +102,16 @@ enum { ...@@ -102,15 +102,16 @@ enum {
OPT_INCLUDED_IN, OPT_INCLUDED_IN,
OPT_INHERENTLY_WEAK_SCCS, OPT_INHERENTLY_WEAK_SCCS,
OPT_INTERSECT, OPT_INTERSECT,
OPT_IS_ALTERNATING,
OPT_IS_COMPLETE, OPT_IS_COMPLETE,
OPT_IS_DETERMINISTIC, OPT_IS_DETERMINISTIC,
OPT_IS_EMPTY, OPT_IS_EMPTY,
OPT_IS_INHERENTLY_WEAK,
OPT_IS_STUTTER_INVARIANT, OPT_IS_STUTTER_INVARIANT,
OPT_IS_TERMINAL, OPT_IS_TERMINAL,
OPT_IS_UNAMBIGUOUS, OPT_IS_UNAMBIGUOUS,
OPT_IS_WEAK,
OPT_IS_INHERENTLY_WEAK,
OPT_IS_VERY_WEAK, OPT_IS_VERY_WEAK,
OPT_IS_WEAK,
OPT_KEEP_STATES, OPT_KEEP_STATES,
OPT_MASK_ACC, OPT_MASK_ACC,
OPT_MERGE, OPT_MERGE,
...@@ -182,6 +183,8 @@ static const argp_option options[] = ...@@ -182,6 +183,8 @@ static const argp_option options[] =
"keep only inherently weak automata", 0 }, "keep only inherently weak automata", 0 },
{ "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0, { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
"keep only very-weak automata", 0 }, "keep only very-weak automata", 0 },
{ "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
"keep only automata using universal branching", 0 },
{ "intersect", OPT_INTERSECT, "FILENAME", 0, { "intersect", OPT_INTERSECT, "FILENAME", 0,
"keep automata whose languages have an non-empty intersection with" "keep automata whose languages have an non-empty intersection with"
" the automaton from FILENAME", 0 }, " the automaton from FILENAME", 0 },
...@@ -409,6 +412,7 @@ static struct opt_t ...@@ -409,6 +412,7 @@ static struct opt_t
}* opt; }* opt;
static bool opt_merge = false; static bool opt_merge = false;
static bool opt_is_alternating = false;
static bool opt_is_complete = false; static bool opt_is_complete = false;
static bool opt_is_deterministic = false; static bool opt_is_deterministic = false;
static bool opt_is_unambiguous = false; static bool opt_is_unambiguous = false;
...@@ -650,6 +654,9 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -650,6 +654,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_INTERSECT: case OPT_INTERSECT:
opt->intersect = read_automaton(arg, opt->dict); opt->intersect = read_automaton(arg, opt->dict);
break; break;
case OPT_IS_ALTERNATING:
opt_is_alternating = true;
break;
case OPT_IS_COMPLETE: case OPT_IS_COMPLETE:
opt_is_complete = true; opt_is_complete = true;
break; break;
...@@ -1016,6 +1023,8 @@ namespace ...@@ -1016,6 +1023,8 @@ namespace
matched &= opt_unused_ap_n.contains(unused); matched &= opt_unused_ap_n.contains(unused);
matched &= opt_used_ap_n.contains(aut->ap().size() - unused); matched &= opt_used_ap_n.contains(aut->ap().size() - unused);
} }
if (matched && opt_is_alternating)
matched &= aut->is_alternating();
if (matched && opt_is_complete) if (matched && opt_is_complete)
matched &= is_complete(aut); matched &= is_complete(aut);
if (matched && (opt_sccs_set | opt_art_sccs_set)) if (matched && (opt_sccs_set | opt_art_sccs_set))
......
...@@ -227,3 +227,36 @@ EOF ...@@ -227,3 +227,36 @@ EOF
run 0 autfilt -CH automaton >out run 0 autfilt -CH automaton >out
cat out cat out
diff out expected diff out expected
autfilt --is-alternating automaton >out
cat out
cat >expected <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels state-acc
properties: deterministic very-weak
--BODY--
State: 0
[!0 | 1] 0
[0&!1] 0&1
State: 1 {0}
[0&!1] 1
--END--
HOA: v1
States: 2
Start: 0&1
AP: 0
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels state-acc
properties: deterministic
--BODY--
State: 0
State: 1
--END--
EOF
diff out expected
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment