From 47974cd00464dc37313e003aef49de41cd5d69a2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 18 May 2018 17:57:24 +0200 Subject: [PATCH] autfilt: support --is-colored This also improve the coverage of the is_colored() function, because it was not used in negative cases so far. * bin/autfilt.cc: Implement it. * tests/core/satmin2.test: Test it. * NEWS: Mention it. --- NEWS | 3 +++ bin/autfilt.cc | 13 ++++++++++++- tests/core/satmin2.test | 7 +++++-- 3 files changed, 20 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index b86947f70..e5ec1d5c5 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,9 @@ New in spot 2.5.3.dev (not yet released) - autcross' tool specifications now have %M replaced by the name of the input automaton. + - autfilt learned --is-colored to filter automata that use + exactly one acceptance set per mark or transition. + Library: - Option "a" of print_dot(), for printing the acceptance condition, diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 2f376afac..1b57691ac 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -54,6 +54,7 @@ #include #include #include +#include #include #include #include @@ -112,6 +113,7 @@ enum { OPT_INHERENTLY_WEAK_SCCS, OPT_INTERSECT, OPT_IS_ALTERNATING, + OPT_IS_COLORED, OPT_IS_COMPLETE, OPT_IS_DETERMINISTIC, OPT_IS_EMPTY, @@ -182,8 +184,11 @@ static const argp_option options[] = "keep automata that are isomorphic to the automaton in FILENAME", 0 }, { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 }, { "unique", 'u', nullptr, 0, - "do not output the same automaton twice (same in the sense that they "\ + "do not output the same automaton twice (same in the sense that they " "are isomorphic)", 0 }, + { "is-colored", OPT_IS_COLORED, nullptr, 0, + "keep colored automata (i.e., exactly one acceptance mark per " + "transition or state)", 0 }, { "is-complete", OPT_IS_COMPLETE, nullptr, 0, "keep complete automata", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0, @@ -555,6 +560,7 @@ static struct opt_t static bool opt_merge = false; static bool opt_is_alternating = false; +static bool opt_is_colored = false; static bool opt_is_complete = false; static bool opt_is_deterministic = false; static bool opt_is_semi_deterministic = false; @@ -862,6 +868,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_IS_ALTERNATING: opt_is_alternating = true; break; + case OPT_IS_COLORED: + opt_is_colored = true; + break; case OPT_IS_COMPLETE: opt_is_complete = true; break; @@ -1263,6 +1272,8 @@ namespace } if (matched && opt_is_alternating) matched &= !aut->is_existential(); + if (matched && opt_is_colored) + matched &= is_colored(aut); if (matched && opt_is_complete) matched &= is_complete(aut); diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test index d7c7e0b27..42f9958e9 100755 --- a/tests/core/satmin2.test +++ b/tests/core/satmin2.test @@ -206,8 +206,8 @@ test `cat output` = 1 # How about a state-based DPA? -autfilt -S --sat-minimize='acc="parity max even 3",colored' -H test.hoa \ - > output +autfilt -S --sat-minimize='acc="parity max even 3",colored' -H test.hoa | + autfilt --is-colored > output cat output grep 'properties:.*colored' output grep 'States: 3' output @@ -384,6 +384,9 @@ State: 0 0 {2 1} /*{b, a}*/ --END-- EOF + +autfilt -q --is-colored foo.hoa && exit 1 + autfilt --sat-minimize='acc="Streett 1",max-states=2' foo.hoa \ --stats=%s >out test "`cat out`" = 1