autfilt: add new option --accept-word

Suggested by Matthias Heizmann. Fixes #109.

* NEWS: notify the new option
* THANKS: add Matthias Heizmann
* bin/autfilt.cc: add new option --accept-word=WORD which filters
automata that accept WORD
* doc/org/autfilt.org: add an example of the new option
* tests/Makefile.am: add core/acc_word.test to the list of test files
* tests/core/acc_word.test: test some uses of the new option

NEWS

 New in spot 1.99.8a (not yet released)
 
+  Command-line tools:
+
+  * autfilt has a new option: --accept-word=WORD, that filters automata
+    that accept WORD.  This option can be used several times, and will
+    filter automata that accept all words.
+
   Library:
 
   * twa::ap_var() renamed to twa::ap_vars().

THANKS

@@ -19,6 +19,7 @@ Jean-Michel Ilié
 Joachim Klein
 Kristin Y. Rozier
 Martin Dieguez Lodeiro
+Matthias Heizmann
 Michael Tautschnig
 Michael Weber
 Ming-Hsien Tsai

bin/autfilt.cc

@@ -69,6 +69,7 @@ Exit status:\n\
 // Keep this list sorted
 enum {
   OPT_ACC_SETS = 256,
+  OPT_ACC_WORD,
   OPT_AP_N,
   OPT_ARE_ISOMORPHIC,
   OPT_CLEAN_ACC,
@@ -224,6 +225,8 @@ 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,
+      "keep automata that recognize WORD", 0 },
     RANGE_DOC_FULL,
     { nullptr, 0, nullptr, 0,
       "If any option among --small, --deterministic, or --any is given, "
@@ -293,6 +296,7 @@ static range opt_states = { 0, std::numeric_limits<int>::max() };
 static range opt_edges = { 0, std::numeric_limits<int>::max() };
 static range opt_accsets = { 0, std::numeric_limits<int>::max() };
 static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
+static std::vector<std::string> opt_acc_words;
 static int opt_max_count = -1;
 static bool opt_destut = false;
 static char opt_instut = 0;
@@ -361,6 +365,9 @@ 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:
+      opt_acc_words.push_back(arg);
+      break;
     case OPT_ARE_ISOMORPHIC:
       opt->are_isomorphic = read_automaton(arg, opt->dict);
       break;
@@ -652,6 +659,20 @@ namespace
 	matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
 	  && spot::product(dtwa_complement(ensure_deterministic(aut)),
 			   opt->equivalent_pos)->is_empty();
+      if (!opt_acc_words.empty())
+	{
+	  auto word_aut = spot::parse_word(opt_acc_words[0],
+				       opt->dict)->as_automaton();
+	  for (size_t i = 1; i < opt_acc_words.size(); ++i)
+	    {
+	      // Compose each additionnanl word with the first one
+	      word_aut = spot::product(word_aut,
+				       spot::parse_word(opt_acc_words[i],
+							opt->dict)
+				       ->as_automaton());
+	    }
+	  matched &= !spot::product(aut, word_aut)->is_empty();
+	}
 
       // Drop or keep matched automata depending on the --invert option
       if (matched == opt_invert)
@@ -812,6 +833,26 @@ main(int argc, char** argv)
       if (processor.run())
 	return 2;
     }
+  catch (const spot::parse_error& e)
+    {
+      auto is_several_lines =
+	[] (const char* err)
+	{
+	  for (;;)
+	    {
+	      if (*err == '\0')
+		return false;
+	      else if (*err == '\n')
+		return true;
+	      ++err;
+	    }
+	};
+      auto err = e.what();
+      if (is_several_lines(err))
+	error(2, 0, "\n%s", err);
+      else
+	error(2, 0, "%s", err);
+    }
   catch (const std::runtime_error& e)
     {
       error(2, 0, "%s", e.what());

doc/org/autfilt.org

@@ -700,25 +700,6 @@ autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a
 #+END_SRC
 
 #+RESULTS: autfilt-ex6c
-#+begin_example
-digraph G {
-  rankdir=LR
-  label=<(Fin(<font color="#F17CB0">❶</font>) &amp; Fin(<font color="#B276B2">❸</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&amp;Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#F17CB0">❶</font>)>
-  labelloc="t"
-  fontname="Lato"
-  node [fontname="Lato"]
-  edge [fontname="Lato"]
-  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
-  I [label="", style=invis, width=0]
-  I -> 0
-  0 [label="0"]
-  0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
-  0 -> 1 [label=<1<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
-  1 [label="1"]
-  1 -> 0 [label=<b<br/><font color="#B276B2">❸</font>>]
-  1 -> 1 [label=<b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
-}
-#+end_example
 
 #+BEGIN_SRC dot :file autfilt-ex6c.png :cmdline -Tpng :var txt=autfilt-ex6c :exports results
 $txt
@@ -730,3 +711,8 @@ $txt
 #+BEGIN_SRC sh :results silent :exports results
 rm -f example.hoa aut-ex1.hoa
 #+END_SRC
+
+#+BEGIN_SRC sh :results verbatim :exports code
+ltl2tgba 'a U b U c' | autfilt --accept-word 'b; cycle{c}' -q  &&
+echo "word accepted"
+#+END_SRC

tests/Makefile.am

@@ -277,7 +277,8 @@ TESTS_twa = \
   core/ltlcross2.test \
   core/complementation.test \
   core/randpsl.test \
-  core/cycles.test
+  core/cycles.test \
+  core/acc_word.test
 
 
 ############################## PYTHON ##############################

tests/core/acc_word.test

+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2016 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+# The --accept-word option filters automata that accept the given word
+# If several words are given, it filters automata that accept ALL words
+ltl2tgba 'G!a' | autfilt --accept-word 'b; cycle{!a}'
+ltl2tgba 'a U b' | autfilt --accept-word 'a; a; cycle{b}'
+ltl2tgba 'F(!a&b)' |
+    autfilt --accept-word 'b; cycle{b; !a&b}' --accept-word 'cycle{b}'