From 897a6ddc04c69fa6abf9cf2b4cb61df44e536924 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Mar 2016 21:38:59 +0100
Subject: [PATCH] autfilt: fix --accept-word

* bin/autfilt.cc: Translate each word as an automaton once,
and do not make a global product of all of them.
* spot/twaalgos/word.cc: Register the atomic propositions used by the
word when converting it into an automaton.
* tests/core/acc_word.test: Add a test case that used to fail, and
another test that make sure some words are not accepted.
---
 bin/autfilt.cc           | 38 +++++++++++---------------------------
 spot/twaalgos/word.cc    | 15 +++++++++++++++
 tests/core/acc_word.test | 11 ++++++++---
 3 files changed, 34 insertions(+), 30 deletions(-)

diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index a4b070b0c..35686fc88 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -58,6 +58,7 @@
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/hoa.hh>
 
 static const char argp_program_doc[] ="\
 Convert, transform, and filter omega-automata.\v\
@@ -282,6 +283,7 @@ static struct opt_t
   std::unique_ptr<unique_aut_t> uniq = nullptr;
   spot::exclusive_ap excl_ap;
   spot::remove_ap rem_ap;
+  std::vector<spot::twa_graph_ptr> acc_words;
 }* opt;
 
 static bool opt_merge = false;
@@ -296,7 +298,6 @@ 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;
@@ -366,7 +367,8 @@ parse_opt(int key, char* arg, struct argp_state*)
       opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
     case OPT_ACC_WORD:
-      opt_acc_words.push_back(arg);
+      opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
+			       ->as_automaton());
       break;
     case OPT_ARE_ISOMORPHIC:
       opt->are_isomorphic = read_automaton(arg, opt->dict);
@@ -659,20 +661,14 @@ 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)
+
+      if (matched && !opt->acc_words.empty())
+	for (auto& word_aut: opt->acc_words)
+	  if (spot::product(aut, word_aut)->is_empty())
 	    {
-	      // 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 = false;
+	      break;
 	    }
-	  matched &= !spot::product(aut, word_aut)->is_empty();
-	}
 
       // Drop or keep matched automata depending on the --invert option
       if (matched == opt_invert)
@@ -835,20 +831,8 @@ main(int argc, char** argv)
     }
   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))
+      if (strchr(err, '\n'))
 	error(2, 0, "\n%s", err);
       else
 	error(2, 0, "%s", err);
diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc
index b81a509d2..61a005264 100644
--- a/spot/twaalgos/word.cc
+++ b/spot/twaalgos/word.cc
@@ -227,6 +227,21 @@ namespace spot
     aut->prop_weak(true);
     aut->prop_deterministic(true);
 
+    // Register the atomic propositions used in the word.
+    {
+      bdd support = bddtrue;
+      for (auto b: prefix)
+	support &= bdd_support(b);
+      for (auto b: cycle)
+	support &= bdd_support(b);
+      while (support != bddtrue)
+	{
+	  int v = bdd_var(support);
+	  support = bdd_high(support);
+	  aut->register_ap(dict_->bdd_map[v].f);
+	}
+    }
+
     size_t i = 0;
     aut->new_states(prefix.size() + cycle.size());
     for (auto b: prefix)
diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test
index 7b7869462..87c759faf 100644
--- a/tests/core/acc_word.test
+++ b/tests/core/acc_word.test
@@ -21,7 +21,12 @@
 
 # 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 'G!a' | autfilt --accept-word 'b; cycle{!a}' -q
+ltl2tgba 'a U b' | autfilt --accept-word 'a; a; cycle{b}' -q
 ltl2tgba 'F(!a&b)' |
-    autfilt --accept-word 'b; cycle{b; !a&b}' --accept-word 'cycle{b}'
+    autfilt --accept-word 'b; cycle{b; !a&b}' --accept-word 'cycle{b}' -q
+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
+: