autfilt: add a --reject-word option

* bin/autfilt.cc: Implement --reject-word.
* NEWS, doc/org/autfilt.org: More doc.
* tests/core/acc_word.test: More tests.

NEWS

@@ -2,12 +2,15 @@ New in spot 1.99.8a (not yet released)
 
   Command-line tools:
 
-  * autfilt has a new option: --accept-word=WORD, that filters automata
+  * autfilt has two new options: --accept-word=WORD and
-    that accept WORD.  This option can be used several times, and will
+    --reject-word=WORD for filtering automata that accept or reject
-    filter automata that accept all words.
+    some word.  The option may be used multiple times.
 
   Library:
 
+  * The parse_word() function can be used to parse a lasso-shaped
+    word and build a twa_word.  The twa_word::as_automaton()
+    method can be used to create an automaton out of that.
   * twa::ap_var() renamed to twa::ap_vars().
   * emptiness_check_instantiator::min_acceptance_conditions() and
     emptiness_check_instantiator::max_acceptance_conditions() renamed

bin/autfilt.cc

@@ -70,7 +70,7 @@ Exit status:\n\
 // Keep this list sorted
 enum {
   OPT_ACC_SETS = 256,
-  OPT_ACC_WORD,
+  OPT_ACCEPT_WORD,
   OPT_AP_N,
   OPT_ARE_ISOMORPHIC,
   OPT_CLEAN_ACC,
@@ -101,6 +101,7 @@ enum {
   OPT_PRODUCT_AND,
   OPT_PRODUCT_OR,
   OPT_RANDOMIZE,
+  OPT_REJECT_WORD,
   OPT_REM_AP,
   OPT_REM_DEAD,
   OPT_REM_UNREACH,
@@ -226,9 +227,15 @@ static const argp_option options[] =
       "keep automata whose number of edges are in RANGE", 0 },
     { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
       "keep automata whose number of acceptance sets are in RANGE", 0 },
-    { "accept-word", OPT_ACC_WORD, "WORD", 0,
+    { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
-      "keep automata that recognize WORD", 0 },
+      "keep automata that accept WORD", 0 },
+    { "reject-word", OPT_REJECT_WORD, "WORD", 0,
+      "keep automata that reject WORD", 0 },
     RANGE_DOC_FULL,
+    { nullptr, 0, nullptr, 0,
+      "WORD is lasso-shaped and written as 'BF;BF;...;BF;cycle{BF;...;BF}' "
+      "where BF are arbitrary Boolean formulas.  The 'cycle{...}' part is "
+      "mandatory, but the prefix can be omitted.", 0 },
     { nullptr, 0, nullptr, 0,
       "If any option among --small, --deterministic, or --any is given, "
       "then the simplification level defaults to --high unless specified "
@@ -284,6 +291,7 @@ static struct opt_t
   spot::exclusive_ap excl_ap;
   spot::remove_ap rem_ap;
   std::vector<spot::twa_graph_ptr> acc_words;
+  std::vector<spot::twa_graph_ptr> rej_words;
 }* opt;
 
 static bool opt_merge = false;
@@ -366,7 +374,7 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_ACC_SETS:
       opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
-    case OPT_ACC_WORD:
+    case OPT_ACCEPT_WORD:
       try
 	{
 	  opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
@@ -537,6 +545,18 @@ parse_opt(int key, char* arg, struct argp_state*)
 	  randomize_st = true;
 	}
       break;
+    case OPT_REJECT_WORD:
+      try
+	{
+	  opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
+				   ->as_automaton());
+	}
+      catch (const spot::parse_error& e)
+	{
+	  error(2, 0, "failed to parse the argument of --reject-word:\n%s",
+		e.what());
+	}
+      break;
     case OPT_REM_AP:
       opt->rem_ap.add_ap(arg);
       break;
@@ -677,6 +697,13 @@ namespace
 	      matched = false;
 	      break;
 	    }
+      if (matched && !opt->rej_words.empty())
+	for (auto& word_aut: opt->rej_words)
+	  if (!spot::product(aut, word_aut)->is_empty())
+	    {
+	      matched = false;
+	      break;
+	    }
 
       // Drop or keep matched automata depending on the --invert option
       if (matched == opt_invert)

doc/org/autfilt.org

@@ -163,9 +163,16 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
 #+begin_example
       --acc-sets=RANGE       keep automata whose number of acceptance sets are
                              in RANGE
+      --accept-word=WORD     keep automata that accept WORD
+      --ap=RANGE             match automata with a number of atomic
+                             propositions in RANGE
       --are-isomorphic=FILENAME   keep automata that are isomorphic to the
                              automaton in FILENAME
       --edges=RANGE          keep automata whose number of edges are in RANGE
+      --equivalent-to=FILENAME   keep automata thare are equivalent
+                             (language-wise) to the automaton in FILENAME
+      --included-in=FILENAME keep automata whose languages are included in that
+                             of the automaton from FILENAME
       --intersect=FILENAME   keep automata whose languages have an non-empty
                              intersection with the automaton from FILENAME
       --is-complete          keep complete automata
@@ -175,6 +182,7 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
       --is-terminal          keep only terminal automata
       --is-unambiguous       keep only unambiguous automata
       --is-weak              keep only weak automata
+      --reject-word=WORD     keep automata that reject WORD
       --states=RANGE         keep automata whose number of states are in RANGE
   -u, --unique               do not output the same automaton twice (same in
                              the sense that they are isomorphic)
@@ -716,3 +724,31 @@ rm -f example.hoa aut-ex1.hoa
 ltl2tgba 'a U b U c' | autfilt --accept-word 'b; cycle{c}' -q  &&
 echo "word accepted"
 #+END_SRC
+
+
+Here is an example where we generate an infinite stream of random LTL
+formulas using [[file:randltl.org][=randltl=]], convert them all to automata using
+[[file:ltl2tgba.org][=ltl2tgba=]], filter out the first 10 automata that accept both the
+words =a&!b;cycle{!a&!b}= and =!a&!b;cycle{a&b}= yet reject any word
+of the form =cycle{b}=, and display the associated formula (which was
+stored as the name of the automaton by =ltl2tgba=).
+
+#+BEGIN_SRC sh :results verbatim :export both
+randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- |
+  autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \
+          --reject-word='cycle{b}' --stats=%M -n 10
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+F!b
+!b
+F(!a & !b)
+(!a & (XX!a | (!a W F!b))) R !b
+F(Fb R !b)
+Fa R F!b
+Fa U !b
+!b & X(!b W Ga)
+Fb R F!b
+XF!b U (!b & (!a | G!b))
+#+end_example

tests/core/acc_word.test

@@ -18,6 +18,7 @@
 # You should have received a copy of the GNU General Public License
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+. ./defs
 
 # The --accept-word option filters automata that accept the given word
 # If several words are given, it filters automata that accept ALL words
@@ -29,4 +30,32 @@ ltl2tgba -f 'a U b' |
     autfilt --accept-word='cycle{!a}' --accept-word='a;cycle{b}' -q
 
 ltl2tgba -f 'a U b' | autfilt --accept-word='cycle{!b}' -q && exit 1
-:
+
+# An example from the documentation:
+randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- |
+  autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \
+          --reject-word='cycle{b}' --stats=%M -n 3 > out
+cat >expect <<EOF
+F!b
+!b
+F(!a & !b)
+EOF
+diff out expect
+
+# Test syntax errors
+autfilt --reject='foobar' </dev/null 2>error && exit 1
+autfilt --accept='cycle{foo' </dev/null 2>>error && exit 1
+cat error
+cat >expect <<EOF
+autfilt: failed to parse the argument of --reject-word:
+>>> foobar
+          ^
+A twa_word must contain a cycle
+
+autfilt: failed to parse the argument of --accept-word:
+>>> cycle{foo
+             ^
+Missing ';' or '}' after formula
+
+EOF
+diff expect error