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

@@ -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,

bin/autfilt.cc

@@ -54,6 +54,7 @@
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/gtec/gtec.hh>
 #include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/iscolored.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/isweakscc.hh>
@@ -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);
 

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