remove_x: Implement detection of stutter-invariant LTL formulas.

* src/bin/ltlfilt.cc: Add options --remove-x and --stutter-invariant.
* src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltltest/remove_x.test: New file.
* src/ltltest/Makefile.am: Add it.
* NEWS: Mention the new algorithms.

NEWS

@@ -29,6 +29,17 @@ New in spot 1.0.2a (not released):
       of out-of-SCC transitions as "don't care".  It is not
       enabled by default because it currently is very slow.
 
+    - remove_x() is a function that take a formula, and rewrite it
+      without the X operator.  The rewriting is only correct for
+      stutter-insensitive LTL formulas (See K. Etessami's paper in IFP
+      vol. 75(6). 2000) This algorithm is accessible from the
+      command-line using ltlfilt's --remove-x option.
+
+    - is_stutter_insensitive() takes any LTL formula, and check
+      whether it is stutter-insensitive.  This algorithm is accessible
+      from the command-line using ltlfilt's --stutter-insensitive
+      option.
+
   * Command-line tools
 
     - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x)

src/bin/ltlfilt.cc

@@ -38,6 +38,7 @@
 #include "ltlvisit/length.hh"
 #include "ltlvisit/relabel.hh"
 #include "ltlvisit/wmunabbrev.hh"
+#include "ltlvisit/remove_x.hh"
 #include "ltlast/unop.hh"
 #include "ltlast/multop.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
@@ -77,6 +78,8 @@ Exit status:\n\
 #define OPT_RELABEL 26
 #define OPT_REMOVE_WM 27
 #define OPT_BOOLEAN_TO_ISOP 28
+#define OPT_REMOVE_X 29
+#define OPT_STUTTER_INSENSITIVE 30
 
 static const argp_option options[] =
   {
@@ -99,6 +102,9 @@ static const argp_option options[] =
     { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0,
       "rewrite Boolean subformulas as irredundant sum of products "
       "(implies at least -r1)", 0 },
+    { "remove-x", OPT_REMOVE_X, 0, 0,
+      "remove X operators (valid only for stutter-insensitive properties)",
+      0 },
     DECLARE_OPT_R,
     LEVEL_DOC(4),
     /**************************************************/
@@ -139,6 +145,9 @@ static const argp_option options[] =
       "match formulas implying FORMULA", 0 },
     { "equivalent-to", OPT_EQUIVALENT_TO, "FORMULA", 0,
       "match formulas equivalent to FORMULA", 0 },
+    { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, 0, 0,
+      "match stutter-insensitive LTL formulas", 0 },
+    { "stutter-invariant", 0, 0, OPTION_ALIAS, 0, 0 },
     { "invert-match", 'v', 0, 0, "select non-matching formulas", 0},
     { "unique", 'u', 0, 0,
       "drop formulas that have already been output (not affected by -v)", 0 },
@@ -187,6 +196,8 @@ static int bsize_max = -1;
 static bool relabeling = false;
 static spot::ltl::relabeling_style style = spot::ltl::Abc;
 static bool remove_wm = false;
+static bool remove_x = false;
+static bool stutter_insensitive = false;
 
 static const spot::ltl::formula* implied_by = 0;
 static const spot::ltl::formula* imply = 0;
@@ -305,6 +316,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_REMOVE_WM:
       remove_wm = true;
       break;
+    case OPT_REMOVE_X:
+      remove_x = true;
+      break;
     case OPT_SAFETY:
       safety = obligation = true;
       break;
@@ -317,6 +331,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_SKIP_ERRORS:
       error_style = skip_errors;
       break;
+    case OPT_STUTTER_INSENSITIVE:
+      stutter_insensitive = true;
+      break;
     case OPT_SYNTACTIC_SAFETY:
       syntactic_safety = true;
       break;
@@ -404,6 +421,21 @@ namespace
       if (negate)
 	f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
 
+      if (remove_x)
+	{
+	  // If simplification are enabled, we do them before and after.
+	  if (simplification_level)
+	    {
+	      const spot::ltl::formula* res = simpl.simplify(f);
+	      f->destroy();
+	      f = res;
+	    }
+
+	  const spot::ltl::formula* res = spot::ltl::remove_x(f);
+	  f->destroy();
+	  f = res;
+	}
+
       if (simplification_level || boolean_to_isop)
 	{
 	  const spot::ltl::formula* res = simpl.simplify(f);
@@ -463,6 +495,7 @@ 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);
 
       // Match obligations and subclasses using WDBA minimization.
       // Because this is costly, we compute it later, so that we don't
@@ -522,6 +555,8 @@ main(int argc, char** argv)
   if (jobs.empty())
     jobs.push_back(job("-", 1));
 
+  // --stutter-insensitive implies --ltl
+  ltl |= stutter_insensitive;
   if (boolean_to_isop && simplification_level == 0)
     simplification_level = 1;
   spot::ltl::ltl_simplifier_options opt = simplifier_options();

src/ltltest/Makefile.am

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

src/ltltest/remove_x.test

+#! /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/>.
+
+. ./defs
+
+run 0 ../../bin/ltlfilt --remove-x -f 'Xa' --equivalent-to 'Ga | (!a & Fa)'
+
+run 1 ../../bin/ltlfilt --stutter-invariant -f 'Xa'
+
+run 0 ../../bin/ltlfilt --stutter-invariant -f 'F(!a & Xa & Xb)'
+
+run 1 ../../bin/ltlfilt --stutter-invariant -f 'F(Xa & Xb)'
+

src/ltlvisit/Makefile.am

 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+## Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
 ## Developpement de l'Epita (LRDE).
 ## Copyright (C) 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -41,6 +41,7 @@ ltlvisit_HEADERS = \
   randomltl.hh \
   reduce.hh \
   relabel.hh \
+  remove_x.hh \
   simpfg.hh \
   simplify.hh \
   snf.hh \
@@ -65,6 +66,7 @@ libltlvisit_la_SOURCES = \
   randomltl.cc \
   reduce.cc \
   relabel.cc \
+  remove_x.cc \
   simpfg.cc \
   simplify.cc \
   snf.cc \

src/ltlvisit/remove_x.cc

+// Copyright (C) 2013 Laboratoire de Recherche et Developpement 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/>.
+
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/simplify.hh"
+#include "ltlvisit/clone.hh"
+#include "ltlvisit/apcollect.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    namespace
+    {
+
+#define AND(x, y) multop::instance(multop::And, (x), (y))
+#define OR(x, y)  multop::instance(multop::Or, (x), (y))
+#define NOT(x)    unop::instance(unop::Not, (x))
+#define G(x)      unop::instance(unop::G, (x))
+#define U(x, y)   binop::instance(binop::U, (x), (y))
+
+      class remove_x_visitor : public clone_visitor
+      {
+	typedef clone_visitor super;
+	atomic_prop_set aps;
+
+      public:
+	remove_x_visitor(const formula* f)
+	{
+	  atomic_prop_collect(f, &aps);
+	}
+
+	virtual
+	~remove_x_visitor()
+	{
+	}
+
+	using super::visit;
+	void visit(const unop* uo)
+	{
+	  const formula* c = recurse(uo->child());
+
+	  unop::type op = uo->op();
+	  if (op != unop::X)
+	    {
+	      result_ = unop::instance(op, c);
+	      return;
+	    }
+	  multop::vec* vo = new multop::vec;
+	  for (atomic_prop_set::const_iterator i = aps.begin();
+	       i != aps.end(); ++i)
+	    {
+	      // First line
+	      multop::vec* va1 = new multop::vec;
+	      const formula* npi = NOT((*i)->clone());
+	      va1->push_back((*i)->clone());
+	      va1->push_back(U((*i)->clone(), AND(npi, c->clone())));
+	      for (atomic_prop_set::const_iterator j = aps.begin();
+		   j != aps.end(); ++j)
+		if (*j != *i)
+		  va1->push_back(OR(U((*j)->clone(), npi->clone()),
+				    U(NOT((*j)->clone()), npi->clone())));
+	      vo->push_back(multop::instance(multop::And, va1));
+	      // Second line
+	      multop::vec* va2 = new multop::vec;
+	      va2->push_back(npi->clone());
+	      va2->push_back(U(npi->clone(), AND((*i)->clone(), c->clone())));
+	      for (atomic_prop_set::const_iterator j = aps.begin();
+		   j != aps.end(); ++j)
+		if (*j != *i)
+		  va2->push_back(OR(U((*j)->clone(), (*i)->clone()),
+				    U(NOT((*j)->clone()), (*i)->clone())));
+	      vo->push_back(multop::instance(multop::And, va2));
+	    }
+	  const formula* l12 = multop::instance(multop::Or, vo);
+	  // Third line
+	  multop::vec* va3 = new multop::vec;
+	  for (atomic_prop_set::const_iterator i = aps.begin();
+	       i != aps.end(); ++i)
+	    {
+	      va3->push_back(OR(G((*i)->clone()),
+				G(NOT((*i)->clone()))));
+	    }
+	  result_ = OR(l12, AND(multop::instance(multop::And, va3), c));
+	  return;
+	}
+
+	virtual const formula* recurse(const formula* f)
+	{
+	  if (f->is_X_free())
+	    return f->clone();
+	  f->accept(*this);
+	  return this->result();
+	}
+      };
+
+    }
+
+    const formula* remove_x(const formula* f)
+    {
+      remove_x_visitor v(f);
+      return v.recurse(f);
+    }
+
+    bool is_stutter_insensitive(const formula* f)
+    {
+      assert(f->is_ltl_formula());
+      if (f->is_X_free())
+	return true;
+      const formula* g = remove_x(f);
+      ltl_simplifier ls;
+      bool res = ls.are_equivalent(f, g);
+      g->destroy();
+      return res;
+    }
+
+  }
+}

src/ltlvisit/remove_x.hh

+// Copyright (C) 2013 Laboratoire de Recherche et Developpement 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/>.
+
+#ifndef SPOT_LTLVISIT_REMOVE_X_HH
+# define SPOT_LTLVISIT_REMOVE_X_HH
+
+namespace spot
+{
+  namespace ltl
+  {
+    class formula;
+
+    /// \brief Rewrite a stutter-insensitive formula \a f without
+    /// using the X operator.
+    ///
+    /// This function may also be applied to stutter-sensitive formulas,
+    /// but in that case the resulting formula is not equivalent.
+    ///
+    /// \verbatim
+    /// @Article{         etessami.00.ipl,
+    ///   author        = {Kousha Etessami},
+    ///   title         = {A note on a question of {P}eled and {W}ilke regarding
+    ///                   stutter-invariant {LTL}},
+    ///   journal       = {Information Processing Letters},
+    ///   volume        = {75},
+    ///   number        = {6},
+    ///   year          = {2000},
+    ///   pages         = {261--263}
+    /// }
+    /// \endverbatim
+    const formula* remove_x(const formula* f);
+
+    /// \brief Whether an LTL formula \a f is stutter-insensitive.
+    ///
+    /// This is simply achieved by checking whether the output of
+    /// <code>remove_x(f)</code> is equivalent to \a f.  This only
+    /// works for LTL formulas, not PSL formulas.
+    ///
+    /// \verbatim
+    /// @Article{         etessami.00.ipl,
+    ///   author        = {Kousha Etessami},
+    ///   title         = {A note on a question of {P}eled and {W}ilke regarding
+    ///                   stutter-invariant {LTL}},
+    ///   journal       = {Information Processing Letters},
+    ///   volume        = {75},
+    ///   number        = {6},
+    ///   year          = {2000},
+    ///   pages         = {261--263}
+    /// }
+    /// \endverbatim
+    bool is_stutter_insensitive(const formula* f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_ETESSAMI00_HH