ltlfilt: Fix handling --universal, --eventual, and --stutter-invariant.

* src/bin/ltlfilt.cc: Handle --universal and --eventual.  Match
only LTL formulas with --stutter-invariant.
* src/ltltest/ltlfilt.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.
* NEWS: Mention these bug fixes.

NEWS

@@ -27,6 +27,8 @@ New in spot 1.1a (not yet released):
   * Bug fixes:
 
     - genltl --gh-r generated the wrong formulas due to a typo.
+    - ltlfilt --eventual and --universal were not handled properly.
+    - ltlfilt --stutter-invariant would trigger an assert on PSL formulas.
 
 New in spot 1.1 (2013-04-28):
 

src/bin/ltlfilt.cc

@@ -273,6 +273,9 @@ parse_opt(int key, char* arg, struct argp_state*)
 	equivalent_to = parse_formula_arg(arg);
 	break;
       }
+    case OPT_EVENTUAL:
+      eventual = true;
+      break;
     case OPT_GUARANTEE:
       guarantee = obligation = true;
       break;
@@ -349,6 +352,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_SYNTACTIC_PERSISTENCE:
       syntactic_persistence = true;
       break;
+    case OPT_UNIVERSAL:
+      universal = true;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }
@@ -495,7 +501,8 @@ namespace
       matched &= !implied_by || simpl.implication(implied_by, f);
       matched &= !imply || simpl.implication(f, imply);
       matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to);
-      matched &= !stutter_insensitive || is_stutter_insensitive(f);
+      matched &= !stutter_insensitive || (f->is_ltl_formula()
+					  && is_stutter_insensitive(f));
 
       // Match obligations and subclasses using WDBA minimization.
       // Because this is costly, we compute it later, so that we don't

src/ltltest/Makefile.am

@@ -94,6 +94,7 @@ TESTS = \
   consterm.test \
   kind.test \
   remove_x.test \
+  ltlfilt.test \
   lbt.test \
   lenient.test \
   isop.test \

src/ltltest/ltlfilt.test

@@ -0,0 +1,138 @@
+#! /bin/sh
+# Copyright (C) 2013 Laboratoire de Recherche et Developement to
+# 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/>.
+
+
+# Check several options of ltlfilt
+
+. ./defs || exit 1
+
+set -e
+
+checkopt()
+{
+  cat >exp
+  run 0 ../../bin/ltlfilt "$@" formulas > out
+  diff exp out
+}
+
+
+cat >formulas <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+!{a;b*;c}!
+a U Fb
+G(a & Xb)
+Xa
+F(a & !Xa & Xb)
+{a & {b|c} }
+EOF
+
+checkopt --eventual <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+a U Fb
+F(a & !Xa & Xb)
+EOF
+
+checkopt --universal <<EOF
+GFa | FGb
+F(GFa | Gb)
+GFa | Gb
+G(a & Xb)
+EOF
+
+checkopt --eventual --universal <<EOF
+GFa | FGb
+F(GFa | Gb)
+EOF
+
+checkopt --stutter-invariant <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+a U Fb
+F(a & !Xa & Xb)
+a & (b | c)
+EOF
+
+checkopt --simplify <<EOF
+F(GFa | Gb)
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+!a | X(!b R !c)
+Fb
+G(a & Xb)
+Xa
+F(a & X(b & !a))
+a & (b | c)
+EOF
+
+checkopt --simplify --eventual --unique <<EOF
+F(GFa | Gb)
+F(b W GFa)
+Fb
+F(a & X(b & !a))
+EOF
+
+checkopt --safety <<EOF
+!({a;b[*];c}!)
+G(a & Xb)
+Xa
+a & (b | c)
+EOF
+
+checkopt --obligation <<EOF
+!({a;b[*];c}!)
+a U Fb
+G(a & Xb)
+Xa
+F(a & !Xa & Xb)
+a & (b | c)
+EOF
+
+checkopt --guarantee <<EOF
+a U Fb
+Xa
+F(a & !Xa & Xb)
+a & (b | c)
+EOF
+
+checkopt -v --ltl <<EOF
+!({a;b[*];c}!)
+EOF
+
+checkopt -v --stutter-invariant <<EOF
+!({a;b[*];c}!)
+G(a & Xb)
+Xa
+EOF
+
+checkopt --equivalent-to 'GFa | FGb' <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+EOF