ltlfilt: implement --reject-word and --accept-word

* bin/common_range.hh: Store the common definition of words.
* bin/autfilt.cc: Use it.
* bin/ltlfilt.cc: Likewise, and implement those two options.
* tests/core/acc_word.test: Test them.
* doc/org/autfilt.org: Augment the last example to point out
that it can now be done with ltlfilt.
* NEWS: Mention the new options.

NEWS

@@ -1,6 +1,10 @@
 New in spot 1.99.9a (not yet released)
 
-  Nothing yet.
+  Command-line tools:
+
+  * ltlfilt now also support the --accept-word=WORD and
+  --reject-word=WORD options that were introduced in autfilt in the
+  previous version.
 
 New in spot 1.99.9 (2016-03-14)
 

bin/autfilt.cc

@@ -232,10 +232,7 @@ static const argp_option options[] =
     { "reject-word", OPT_REJECT_WORD, "WORD", 0,
       "keep automata that reject WORD", 0 },
     RANGE_DOC_FULL,
-    { nullptr, 0, nullptr, 0,
+    WORD_DOC,
-      "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 "

bin/common_range.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,17 +19,23 @@
 
 #pragma once
 
-#define RANGE_DOC                                                        \
+#define RANGE_DOC                                                       \
-    { nullptr, 0, nullptr, 0,                                                \
+    { nullptr, 0, nullptr, 0,                                           \
-      "RANGE may have one of the following forms: 'INT', "                \
+      "RANGE may have one of the following forms: 'INT', "              \
       "'INT..INT', or '..INT'.\nIn the latter case, the missing number " \
       "is assumed to be 1.", 0 }
 
-#define RANGE_DOC_FULL                                                \
+#define RANGE_DOC_FULL                                          \
-    { nullptr, 0, nullptr, 0,                                        \
+    { nullptr, 0, nullptr, 0,                                   \
-      "RANGE may have one of the following forms: 'INT', "        \
+      "RANGE may have one of the following forms: 'INT', "      \
       "'INT..INT', '..INT', or 'INT..'", 0 }
 
+#define WORD_DOC                                                        \
+    { 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 }
+
 struct range
 {
   int min;

bin/ltlfilt.cc

@@ -48,6 +48,8 @@
 #include <spot/twaalgos/minimize.hh>
 #include <spot/twaalgos/strength.hh>
 #include <spot/twaalgos/stutter.hh>
+#include <spot/twaalgos/word.hh>
+#include <spot/twaalgos/product.hh>
 
 const char argp_program_doc[] ="\
 Read a list of formulas and output them back after some optional processing.\v\
@@ -57,7 +59,8 @@ Exit status:\n\
   2  if any error has been reported";
 
 enum {
-  OPT_AP_N = 256,
+  OPT_ACCEPT_WORD = 256,
+  OPT_AP_N,
   OPT_BOOLEAN,
   OPT_BOOLEAN_TO_ISOP,
   OPT_BSIZE,
@@ -76,6 +79,7 @@ enum {
   OPT_NEGATE,
   OPT_NNF,
   OPT_OBLIGATION,
+  OPT_REJECT_WORD,
   OPT_RELABEL,
   OPT_RELABEL_BOOL,
   OPT_REMOVE_WM,
@@ -199,7 +203,12 @@ static const argp_option options[] =
     { "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
     { "unique", 'u', nullptr, 0,
       "drop formulas that have already been output (not affected by -v)", 0 },
+    { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
+      "keep formulas that accept WORD", 0 },
+    { "reject-word", OPT_REJECT_WORD, "WORD", 0,
+      "keep formulas that reject WORD", 0 },
     RANGE_DOC_FULL,
+    WORD_DOC,
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output options:", -20 },
     { "count", 'c', nullptr, 0, "print only a count of matched formulas", 0 },
@@ -275,11 +284,14 @@ static long int match_count = 0;
 // accessing deleted stuff.
 static struct opt_t
 {
+  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
   spot::exclusive_ap excl_ap;
   std::unique_ptr<output_file> output_define = nullptr;
   spot::formula implied_by = nullptr;
   spot::formula imply = nullptr;
   spot::formula equivalent_to = nullptr;
+  std::vector<spot::twa_graph_ptr> acc_words;
+  std::vector<spot::twa_graph_ptr> rej_words;
 }* opt;
 
 static std::string unabbreviate;
@@ -322,6 +334,18 @@ parse_opt(int key, char* arg, struct argp_state*)
       // FIXME: use stat() to distinguish filename from string?
       jobs.emplace_back(arg, true);
       break;
+    case OPT_ACCEPT_WORD:
+      try
+        {
+          opt->acc_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 --accept-word:\n%s",
+                e.what());
+        }
+      break;
     case OPT_BOOLEAN:
       boolean = true;
       break;
@@ -388,6 +412,18 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_OBLIGATION:
       obligation = 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_RELABEL:
     case OPT_RELABEL_BOOL:
       relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling);
@@ -603,24 +639,46 @@ namespace
         || simpl.are_equivalent(f, opt->equivalent_to);
       matched &= !stutter_insensitive || spot::is_stutter_invariant(f);
 
-      // Match obligations and subclasses using WDBA minimization.
+      if (matched && (obligation
-      // Because this is costly, we compute it later, so that we don't
+                      || !opt->acc_words.empty()
-      // have to compute it on formulas that have been discarded for
+                      || !opt->rej_words.empty()))
-      // other reasons.
-      if (matched && obligation)
         {
           auto aut = ltl_to_tgba_fm(f, simpl.get_dict());
-          auto min = minimize_obligation(aut, f);
+
-          assert(min);
+          if (matched && !opt->acc_words.empty())
-          if (aut == min)
+            for (auto& word_aut: opt->acc_words)
+              if (spot::product(aut, word_aut)->is_empty())
+                {
+                  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;
+                }
+
+          // Match obligations and subclasses using WDBA minimization.
+          // Because this is costly, we compute it later, so that we don't
+          // have to compute it on formulas that have been discarded for
+          // other reasons.
+          if (matched && obligation)
             {
-              // Not an obligation
+              auto min = minimize_obligation(aut, f);
-              matched = false;
+              assert(min);
-            }
+              if (aut == min)
-          else
+                {
-            {
+                  // Not an obligation
-              matched &= !guarantee || is_terminal_automaton(min);
+                  matched = false;
-              matched &= !safety || is_safety_mwdba(min);
+                }
+              else
+                {
+                  matched &= !guarantee || is_terminal_automaton(min);
+                  matched &= !safety || is_safety_mwdba(min);
+                }
             }
         }
 
@@ -676,9 +734,9 @@ main(int argc, char** argv)
 
       if (boolean_to_isop && simplification_level == 0)
         simplification_level = 1;
-      spot::tl_simplifier_options opt(simplification_level);
+      spot::tl_simplifier_options tlopt(simplification_level);
-      opt.boolean_to_isop = boolean_to_isop;
+      tlopt.boolean_to_isop = boolean_to_isop;
-      spot::tl_simplifier simpl(opt);
+      spot::tl_simplifier simpl(tlopt, opt->dict);
 
       ltl_processor processor(simpl);
       if (processor.run())

doc/org/autfilt.org

@@ -756,3 +756,25 @@ Fa U !b
 Fb R F!b
 XF!b U (!b & (!a | G!b))
 #+end_example
+
+Note that the above example could be simplified using the
+=--accept-word= and =--reject-word= options of =ltlfilt= directly.
+However this demonstrates that using =--stats=%M=, it is possible to
+filter formulas based on some properties of automata that have been
+generated by from them.  The translator needs not be =ltl2tgba=: other
+tools can be wrapped with [[file:ltldo.org][=ltldo --name=%f=]] to ensure they work well
+in a pipeline and preserve the formula name in the HOA output.  For
+example Here is a list of 5 LTL formulas that =ltl2dstar= converts to
+Rabin automata that have exactly 4 states:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+randltl -n -1 a b | ltlfilt --simplify --remove-wm |
+  ltldo ltl2dstar --name=%f | autfilt --states=4 --stats=%M -n 5
+#+END_SRC
+
+#+RESULTS:
+: Gb | G!b
+: b R (a | b)
+: (a & !b & (b | (F!a U (!b & F!a)))) | (!a & (b | (!b & (Ga R (b | Ga)))))
+: (a & (a U !b)) | (!a & (!a R b))
+: a | G((a & GFa) | (!a & FG!a))

tests/core/acc_word.test

@@ -42,6 +42,12 @@ F(!a & !b)
 EOF
 diff out expect
 
+# The same, without using automata explicitly
+randltl -n -1 a b | ltlfilt --simplify --uniq \
+  --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \
+  --reject-word='cycle{b}' -n 3 > out
+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