From d2316b14287d3136338690cbd091ebf578610e36 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 15 Oct 2018 21:17:18 +0200
Subject: [PATCH] fix ltlfilt --accept-word and --reject-word

* NEWS: Mention the issue.
* bin/ltlfilt.cc: Fix test.
* tests/core/acc_word.test: Test this.
---
 NEWS                     | 3 +++
 bin/ltlfilt.cc           | 9 ++++++++-
 tests/core/acc_word.test | 6 +++++-
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index be11c488d..f9f2098c8 100644
--- a/NEWS
+++ b/NEWS
@@ -74,6 +74,9 @@ New in spot 2.6.2.dev (not yet released)
   - ltl2tgba --low now disables the "gf-guarantee" feature, as
     documented.
 
+  - ltlfilt's --accept-word and --reject-word options were ignored
+    unless used together.
+
 New in spot 2.6.2 (2018-09-28)
 
   Build:
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index 460d31c13..626f59da4 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -83,6 +83,7 @@ enum {
   OPT_IGNORE_ERRORS,
   OPT_IMPLIED_BY,
   OPT_IMPLY,
+  OPT_LIVENESS,
   OPT_LTL,
   OPT_NEGATE,
   OPT_NNF,
@@ -183,6 +184,8 @@ static const argp_option options[] =
     { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0,
       "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 },
     { "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
+    { "liveness", OPT_LIVENESS, nullptr, 0,
+      "match liveness properties", 0 },
     { "safety", OPT_SAFETY, nullptr, 0,
       "match safety formulas (even pathological)", 0 },
     { "guarantee", OPT_GUARANTEE, nullptr, 0,
@@ -281,6 +284,7 @@ static bool negate = false;
 static bool boolean_to_isop = false;
 static bool unique = false;
 static bool psl = false;
+static bool liveness = false;
 static bool ltl = false;
 static bool invert = false;
 static bool boolean = false;
@@ -432,6 +436,9 @@ parse_opt(int key, char* arg, struct argp_state*)
         opt->imply = spot::formula::And({opt->imply, i});
         break;
       }
+    case OPT_LIVENESS:
+      liveness = true;
+      break;
     case OPT_LTL:
       ltl = true;
       break;
@@ -697,7 +704,7 @@ namespace
         {
           spot::twa_graph_ptr aut = nullptr;
 
-          if (!opt->acc_words.empty() && !opt->rej_words.empty())
+          if (!opt->acc_words.empty() || !opt->rej_words.empty())
             {
               aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
 
diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test
index 9c8e46d64..47c09d611 100644
--- a/tests/core/acc_word.test
+++ b/tests/core/acc_word.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -137,3 +137,7 @@ done
 ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1
 test $? -eq 2
 grep 'highlight-word.*Fin' stderr
+
+
+ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1
+ltlfilt -f 'GF!a' --accept-word 'cycle{!a}'