Adding tgba-based stutter-invariance checking

* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
Add closure function.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
Add two implementations of "self-loopize" function.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
self-loopize.
* src/tgba/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
closure and sl.
* src/tgbatest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Modify stutter-invariant option to use
automaton-based checking rather than syntactic-based checking.
* src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
Remove is_stutter_insensitive function.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Check if a formula is
stutter-invariant using closure and sl.
* wrap/python/spot.i: Add closure and sl bindings.
* bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
given formulas.
* bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
from random automata.
* bench/stutter/Makefile.am: Add them.
* configure.ac: Add bench/stutter/Makefile.
* bench/Makefile.am: Add stutter subdirectory.
* README: Document bench/stutter directory.

README

@@ -174,6 +174,7 @@ bench/            Benchmarks for ...
    ltlclasses/    ... translation of more classes of LTL formulae,
    spin13/        ... compositional suspension and other improvements,
    wdba/          ... WDBA minimization (for obligation properties).
+   stutter/       ... stutter-invariance checking algorithms
 wrap/             Wrappers for other languages.
    python/        Python bindings for Spot and BuDDy
       tests/      Tests for these bindings

bench/Makefile.am

@@ -19,4 +19,4 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat
+SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat stutter

bench/stutter/Makefile.am

@@ -0,0 +1,31 @@
+## -*- coding: utf-8 -*-
+## Copyright (C) 2014 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/>.
+
+SUBDIRS = .
+
+AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+LDADD = $(top_builddir)/src/bin/libcommon.a ../../lib/libgnu.la ../../src/libspot.la
+
+bin_PROGRAMS = stutter_invariance_randomgraph \
+	       stutter_invariance_formulas
+
+stutter_invariance_randomgraph_SOURCES = stutter_invariance_randomgraph.cc
+stutter_invariance_formulas_SOURCES = stutter_invariance_formulas.cc

bench/stutter/stutter_invariance_formulas.cc

@@ -0,0 +1,128 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 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/>.
+
+#include "bin/common_sys.hh"
+#include "bin/common_setup.hh"
+#include "bin/common_finput.hh"
+#include "bin/common_output.hh"
+#include "tgbaalgos/translate.hh"
+#include "tgbaalgos/stutter_invariance.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/apcollect.hh"
+#include "ltlvisit/length.hh"
+#include "misc/timer.hh"
+#include <argp.h>
+#include "error.h"
+
+#include "tgbaalgos/closure.hh"
+#include "tgbaalgos/stutterize.hh"
+#include "tgbaalgos/dotty.hh"
+#include "tgba/tgbaproduct.hh"
+
+static unsigned n = 10;
+
+const char argp_program_doc[] ="";
+
+const struct argp_child children[] =
+  {
+    { &finput_argp, 0, 0, 1 },
+    { &output_argp, 0, 0, -20 },
+    { &misc_argp, 0, 0, -1 },
+    { 0, 0, 0, 0 }
+  };
+
+namespace
+{
+  class stut_processor: public job_processor
+  {
+  public:
+    spot::translator& trans;
+    std::string formula;
+
+    stut_processor(spot::translator& trans) : trans(trans)
+    {
+    }
+
+    int
+    process_string(const std::string& input,
+                   const char* filename, int linenum)
+    {
+      formula = input;
+      return job_processor::process_string(input, filename, linenum);
+    }
+
+    int
+    process_formula(const spot::ltl::formula* f,
+                    const char*, int)
+    {
+      const spot::ltl::formula* nf =
+	spot::ltl::unop::instance(spot::ltl::unop::Not,
+				  f->clone());
+      spot::const_tgba_digraph_ptr a = trans.run(f);
+      spot::const_tgba_digraph_ptr na = trans.run(nf);
+      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
+      bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a);
+      bool res;
+      bool prev = true;
+      for (char algo = '1'; algo <= '8'; ++algo)
+        {
+          // set SPOT_STUTTER_CHECK environment variable
+          char algostr[2] = { 0 };
+          algostr[0] = algo;
+          setenv("SPOT_STUTTER_CHECK", algostr, true);
+
+          spot::stopwatch sw;
+          sw.start();
+          for (unsigned i = 0; i < n; ++i)
+            res = spot::is_stutter_invariant(a, na, apdict);
+          const double time = sw.stop();
+
+          std::cout << formula << ", " << algo << ", " << ap->size() << ", "
+		    << a->num_states() << ", " << res << ", " << time << std::endl;
+
+          if (algo > '1')
+            assert(res == prev);
+          prev = res;
+        }
+      f->destroy();
+      nf->destroy();
+      delete(ap);
+      return 0;
+    }
+  };
+}
+
+int
+main(int argc, char** argv)
+{
+  setup(argv);
+
+  const argp ap = { 0, 0, "[FILENAME[/COL]...]",
+                    argp_program_doc, children, 0, 0 };
+
+  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
+    exit(err);
+
+  spot::translator trans;
+  stut_processor processor(trans);
+  if (processor.run())
+    return 2;
+
+  return 0;
+}

bench/stutter/stutter_invariance_randomgraph.cc

@@ -0,0 +1,100 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 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/>.
+
+#include "misc/timer.hh"
+#include "ltlast/atomic_prop.hh"
+#include "tgbaalgos/dtgbacomp.hh"
+#include "tgbaalgos/stutter_invariance.hh"
+#include "tgbaalgos/randomgraph.hh"
+#include "tgbaalgos/dotty.hh"
+#include "tgbaalgos/product.hh"
+#include "tgbaalgos/stutterize.hh"
+#include "tgbaalgos/closure.hh"
+#include "tgba/tgbagraph.hh"
+#include "tgba/bdddict.hh"
+#include <cstdio>
+#include <cstring>
+#include <vector>
+
+int
+main()
+{
+  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
+  spot::tgba_digraph_ptr a;
+  spot::tgba_digraph_ptr na;
+  unsigned n = 10;
+  for (unsigned states_n = 1; states_n <= 50; ++states_n)
+    for (float d = 0; d <= 1; d += 0.1)
+      {
+        for (unsigned props_n = 1; props_n <= 4; ++props_n)
+          {
+            // random ap set
+            auto ap = new spot::ltl::atomic_prop_set();
+            spot::ltl::default_environment& e =
+              spot::ltl::default_environment::instance();
+            for (unsigned i = 1; i < props_n; ++i)
+              {
+                std::ostringstream p;
+                p << 'p' << i;
+                ap->insert(static_cast<const spot::ltl::atomic_prop*>
+                           (e.require(p.str())));
+              }
+
+            // ap set as bdd
+            bdd apdict = bddtrue;
+            for (auto& i: *ap)
+              apdict &= bdd_ithvar(dict->register_proposition(i, a));
+
+            // generate n random automata
+            typedef std::pair<spot::tgba_digraph_ptr, spot::tgba_digraph_ptr>
+              aut_pair_t;
+            std::vector<aut_pair_t> vec;
+            for (unsigned i = 0; i < n; ++i)
+              {
+                a = spot::random_graph(states_n, d, ap, dict, 2, 0.1, 0.5,
+                                       true);
+                na = spot::dtgba_complement(a);
+                vec.push_back(aut_pair_t(a, na));
+              }
+
+            for (char algo = '1'; algo <= '8'; ++algo)
+              {
+                // set SPOT_STUTTER_CHECK environment variable
+                char algostr[2] = { 0 };
+                algostr[0] = algo;
+                setenv("SPOT_STUTTER_CHECK", algostr, true);
+
+                spot::stopwatch sw;
+                sw.start();
+                bool res;
+                for (auto& a: vec)
+                  res = spot::is_stutter_invariant(a.first, a.second, apdict);
+                const double time = sw.stop();
+
+                std::cout << algo << ", " << props_n << ", " << states_n
+                          << ", " << res << ", " << time << std::endl;
+              }
+            spot::ltl::destroy_atomic_prop_set(*ap);
+            delete(ap);
+          }
+      }
+
+
+  return 0;
+}

configure.ac

@@ -164,6 +164,7 @@ AC_CONFIG_FILES([
   bench/ltl2tgba/defs
   bench/spin13/Makefile
   bench/wdba/Makefile
+  bench/stutter/Makefile
   doc/Doxyfile
   doc/Makefile
   doc/tl/Makefile

src/bin/ltlfilt.cc

@@ -45,6 +45,7 @@
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/minimize.hh"
 #include "tgbaalgos/safety.hh"
+#include "tgbaalgos/stutter_invariance.hh"
 
 const char argp_program_doc[] ="\
 Read a list of formulas and output them back after some optional processing.\v\
@@ -550,8 +551,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 || (f->is_ltl_formula()
+      matched &= !stutter_insensitive || spot::is_stutter_invariant(f);
-					  && is_stutter_insensitive(f));
 
       // Match obligations and subclasses using WDBA minimization.
       // Because this is costly, we compute it later, so that we don't
@@ -609,8 +609,6 @@ main(int argc, char** argv)
   if (jobs.empty())
     jobs.emplace_back("-", 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/ltlvisit/remove_x.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -117,18 +117,5 @@ namespace spot
       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

@@ -48,27 +48,6 @@ namespace spot
         \endverbatim */
     SPOT_API
     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 */
-    SPOT_API
-    bool is_stutter_insensitive(const formula* f);
   }
 }
 

src/tgba/Makefile.am

@@ -37,7 +37,8 @@ tgba_HEADERS = \
   tgbamask.hh \
   tgbaproxy.hh \
   tgbaproduct.hh \
-  tgbasafracomplement.hh
+  tgbasafracomplement.hh \
+  tgbasl.hh
 
 noinst_LTLIBRARIES = libtgba.la
 libtgba_la_SOURCES = \
@@ -50,4 +51,5 @@ libtgba_la_SOURCES = \
   tgbaproduct.cc \
   tgbamask.cc \
   tgbaproxy.cc \
-  tgbasafracomplement.cc
+  tgbasafracomplement.cc \
+  tgbasl.cc

src/tgba/tgbasl.cc

@@ -0,0 +1,234 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2011, 2012, 2014 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/>.
+
+#include "tgbasl.hh"
+#include "bddprint.hh"
+
+namespace spot
+{
+  namespace
+  {
+    class state_tgbasl: public state
+    {
+    public:
+      state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond)
+      {
+      }
+
+      virtual
+      ~state_tgbasl()
+      {
+        s_->destroy();
+      }
+
+      virtual int
+      compare(const state* other) const
+      {
+        const state_tgbasl* o =
+          down_cast<const state_tgbasl*>(other);
+        assert(o);
+        int res = s_->compare(o->real_state());
+        if (res != 0)
+          return res;
+        return cond_.id() - o->cond_.id();
+      }
+
+      virtual size_t
+      hash() const
+      {
+        return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
+      }
+
+      virtual
+      state_tgbasl* clone() const
+      {
+        return new state_tgbasl(*this);
+      }
+
+      state*
+      real_state() const
+      {
+        return s_;
+      }
+
+      bdd
+      cond() const
+      {
+        return cond_;
+      }
+
+    private:
+      state* s_;
+      bdd cond_;
+    };
+
+    class tgbasl_succ_iterator : public tgba_succ_iterator
+    {
+    public:
+      tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state,
+			   bdd_dict_ptr d, bdd atomic_propositions)
+        : it_(it), state_(state), aps_(atomic_propositions), d_(d)
+      {
+      }
+
+      virtual
+      ~tgbasl_succ_iterator()
+      {
+        delete it_;
+      }
+
+      // iteration
+
+      bool
+      first()
+      {
+        loop_ = false;
+        done_ = false;
+        need_loop_ = true;
+        if (it_->first())
+          {
+            cond_ = it_->current_condition();
+            next_edge();
+          }
+        return true;
+      }
+
+      bool
+      next()
+      {
+        if (cond_ != bddfalse)
+          {
+            next_edge();
+            return true;
+          }
+        if (!it_->next())
+          {
+            if (loop_ || !need_loop_)
+              done_ = true;
+            loop_ = true;
+            return !done_;
+          }
+        else
+          {
+            cond_ = it_->current_condition();
+            next_edge();
+            return true;
+          }
+      }
+
+      bool
+      done() const
+      {
+        return it_->done() && done_;
+      }
+
+      // inspection
+
+      state_tgbasl*
+      current_state() const
+      {
+        if (loop_)
+          return new state_tgbasl(state_->real_state(), state_->cond());
+        return new state_tgbasl(it_->current_state(), one_);
+      }
+
+      bdd
+      current_condition() const
+      {
+        if (loop_)
+          return state_->cond();
+        return one_;
+      }
+
+      acc_cond::mark_t
+      current_acceptance_conditions() const
+      {
+        if (loop_)
+          return 0U;
+        return it_->current_acceptance_conditions();
+      }
+
+    private:
+      void
+      next_edge()
+      {
+        one_ = bdd_satoneset(cond_, aps_, bddtrue);
+        cond_ -= one_;
+        if (need_loop_ && (state_->cond() == one_)
+            && (state_ == it_->current_state()))
+          need_loop_ = false;
+      }
+
+      tgba_succ_iterator* it_;
+      const state_tgbasl* state_;
+      bdd cond_;
+      bdd one_;
+      bdd aps_;
+      bdd_dict_ptr d_;
+      bool loop_;
+      bool need_loop_;
+      bool done_;
+    };
+  }
+
+  tgbasl::tgbasl(const const_tgba_ptr& a, bdd atomic_propositions)
+    : tgba(a->get_dict()), a_(a), aps_(atomic_propositions)
+  {
+    auto d = get_dict();
+    d->register_all_propositions_of(&a_, this);
+    assert(acc_.num_sets() == 0);
+    acc_.add_sets(a_->acc().num_sets());
+  }
+
+  tgbasl::~tgbasl()
+  {
+    get_dict()->unregister_all_my_variables(this);
+  }
+
+  state*
+  tgbasl::get_init_state() const
+  {
+    return new state_tgbasl(a_->get_init_state(), bddfalse);
+  }
+
+  tgba_succ_iterator*
+  tgbasl::succ_iter(const state* state) const
+  {
+    const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
+    assert(s);
+    return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s,
+				    a_->get_dict(), aps_);
+  }
+
+  bdd
+  tgbasl::compute_support_conditions(const state*) const
+  {
+    return bddtrue;
+  }
+
+  std::string
+  tgbasl::format_state(const state* state) const
+  {
+    const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
+    assert(s);
+    return (a_->format_state(s->real_state())
+            + ", "
+            + bdd_format_formula(a_->get_dict(), s->cond()));
+  }
+}

src/tgba/tgbasl.hh

@@ -0,0 +1,49 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013, 2014 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/>.
+
+#ifndef SPOT_TGBA_TGBASL_HH
+# define SPOT_TGBA_TGBASL_HH
+
+#include "tgba.hh"
+
+namespace spot
+{
+  class SPOT_API tgbasl : public tgba
+  {
+  public:
+    tgbasl(const const_tgba_ptr& a, bdd ap);
+
+    virtual ~tgbasl();
+
+    virtual state* get_init_state() const;
+
+    virtual tgba_succ_iterator* succ_iter(const state* state) const;
+
+    virtual std::string format_state(const state* state) const;
+
+  protected:
+    virtual bdd compute_support_conditions(const state* state) const;
+
+  private:
+    const_tgba_ptr a_;
+    bdd aps_;
+  };
+}
+
+#endif

src/tgbaalgos/Makefile.am

@@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
 
 tgbaalgos_HEADERS = \
   bfssteps.hh \
+  closure.hh \
   complete.hh \
   compsusp.hh \
   cycles.hh \
@@ -69,6 +70,8 @@ tgbaalgos_HEADERS = \
   simulation.hh \
   stats.hh \
   stripacc.hh \
+  stutter_invariance.hh \
+  stutterize.hh \
   tau03.hh \
   tau03opt.hh \
   translate.hh \
@@ -77,6 +80,7 @@ tgbaalgos_HEADERS = \
 noinst_LTLIBRARIES = libtgbaalgos.la
 libtgbaalgos_la_SOURCES = \
   bfssteps.cc \
+  closure.cc \
   complete.cc \
   compsusp.cc \
   cycles.cc \
@@ -117,6 +121,8 @@ libtgbaalgos_la_SOURCES = \
   simulation.cc \
   stats.cc \
   stripacc.cc \
+  stutter_invariance.cc \
+  stutterize.cc \
   tau03.cc \
   tau03opt.cc \
   translate.cc \

src/tgbaalgos/closure.cc

@@ -0,0 +1,121 @@
+// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// 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 <unordered_set>
+#include <deque>
+#include "closure.hh"
+#include "dupexp.hh"
+
+namespace spot
+{
+  namespace
+  {
+    struct transition
+    {
+      unsigned dst;
+      acc_cond::mark_t acc;
+      transition(unsigned dst, acc_cond::mark_t acc) :
+	dst(dst), acc(acc)
+      {
+      }
+    };
+
+    struct transition_hash
+    {
+      size_t
+      operator()(const transition& t) const
+      {
+	return wang32_hash(t.dst) ^ wang32_hash(t.acc);
+      }
+    };
+
+    struct transition_equal
+    {
+      bool
+      operator()(const transition& left, const transition& right) const
+      {
+	return left.dst == right.dst
+	  && left.acc == right.acc;
+      }
+    };
+
+    typedef std::unordered_map<transition, unsigned, transition_hash,
+			       transition_equal> tmap_t;
+    typedef std::set<unsigned> tset_t;
+  }
+
+  tgba_digraph_ptr
+  closure(const const_tgba_digraph_ptr& a)
+  {
+    tgba_digraph_ptr res = tgba_dupexp_dfs(a);
+    unsigned n = res->num_states();
+    tset_t todo;
+
+    for (unsigned state = 0; state < n; ++state)
+      {
+	tmap_t uniq;
+	auto trans = res->out(state);
+
+	for (auto it = trans.begin(); it != trans.end(); ++it)
+	  {
+	    todo.insert(it.trans());
+	    uniq.emplace(transition(it->dst, it->acc), it.trans());
+	  }
+
+	while (!todo.empty())
+	  {
+	    unsigned t1 = *todo.begin();
+	    todo.erase(t1);
+	    tgba_graph_trans_data td = res->trans_data(t1);
+	    unsigned dst = res->trans_storage(t1).dst;
+
+	    for (auto& t2 : res->out(dst))
+	      {
+		bdd cond = td.cond & t2.cond;
+		if (cond != bddfalse)
+		  {
+		    acc_cond::mark_t acc = td.acc | t2.acc;
+		    transition jump(t2.dst, acc);
+		    unsigned i;
+		    auto u = uniq.find(jump);
+
+		    if (u == uniq.end())
+		      {
+			i = res->new_transition(state, t2.dst, cond, acc);
+			uniq.emplace(jump, i);
+			todo.insert(i);
+		      }
+
+		    else
+		      {
+			bdd old_cond = res->trans_data(u->second).cond;
+			if (!bdd_implies(cond, old_cond))
+			  {
+			    res->trans_data(u->second).cond = cond | old_cond;
+			    todo.insert(u->second);
+			  }
+		      }
+		  }
+	      }
+	  }
+	uniq.clear();
+      }
+    return res;
+  }
+}

src/tgbaalgos/closure.hh

@@ -0,0 +1,31 @@
+// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// 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_TGBAALGOS_CLOSURE_HH
+# define SPOT_TGBAALGOS_CLOSURE_HH
+
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+  SPOT_API tgba_digraph_ptr
+  closure(const const_tgba_digraph_ptr&);
+}
+
+#endif

src/tgbaalgos/stutter_invariance.cc

@@ -0,0 +1,126 @@
+// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// 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 <iostream>
+#include "tgba/tgbagraph.hh"
+#include "closure.hh"
+#include "stutterize.hh"
+#include "ltlvisit/remove_x.hh"
+#include "tgbaalgos/translate.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/apcollect.hh"
+#include "stutter_invariance.hh"
+#include "tgba/tgbasl.hh"
+#include "tgba/tgbaproduct.hh"
+#include "tgbaalgos/dupexp.hh"
+
+namespace spot
+{
+  bool
+  is_stutter_invariant(const ltl::formula* f)
+    {
+      const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
+      char algo = stutter_check ? stutter_check[0] : '1';
+      if (f->is_ltl_formula() && f->is_X_free())
+        return true;
+
+      if (algo == '0')
+        {
+          // Syntactic checking.
+          if (f->is_ltl_formula())
+            {
+              const ltl::formula* g = remove_x(f);
+              ltl::ltl_simplifier ls;
+              bool res = ls.are_equivalent(f, g);
+              g->destroy();
+              return res;
+            }
+          else
+            {
+              throw std::runtime_error("Cannot use the syntactic-based " \
+                                       "approach to stutter-invariance " \
+                                       "checking on non-ltl formula");
+            }
+        }
+      const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
+      translator trans;
+      auto aut_f = trans.run(f);
+      auto aut_nf = trans.run(nf);
+      bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
+      nf->destroy();
+      return is_stutter_invariant(aut_f, aut_nf, aps);
+    }
+
+  bool
+  is_stutter_invariant(const const_tgba_digraph_ptr& aut_f,
+                       const const_tgba_digraph_ptr& aut_nf, bdd aps)
+    {
+      const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
+      char algo = stutter_check ? stutter_check[0] : '8';
+
+      switch (algo)
+        {
+          // sl(aut_f) x sl(aut_nf)
+        case '1':
+            {
+              return product(sl(aut_f, aps), sl(aut_nf, aps))->is_empty();
+            }
+          // sl(cl(aut_f)) x aut_nf
+        case '2':
+            {
+              return product(sl(closure(aut_f), aps), aut_nf)->is_empty();
+            }
+          // (cl(sl(aut_f)) x aut_nf
+        case '3':
+            {
+              return product(closure(sl(aut_f, aps)), aut_nf)->is_empty();
+            }
+          // sl2(aut_f) x sl2(aut_nf)
+        case '4':
+            {
+              return product(sl2(aut_f, aps), sl2(aut_nf, aps))->is_empty();
+            }
+          // sl2(cl(aut_f)) x aut_nf
+        case '5':
+            {
+              return product(sl2(closure(aut_f), aps), aut_nf)->is_empty();
+            }
+          // (cl(sl2(aut_f)) x aut_nf
+        case '6':
+            {
+              return product(closure(sl2(aut_f, aps)), aut_nf)->is_empty();
+            }
+          // on-the-fly sl(aut_f) x sl(aut_nf)
+        case '7':
+            {
+              auto slf = std::make_shared<tgbasl>(aut_f, aps);
+              auto slnf = std::make_shared<tgbasl>(aut_nf, aps);
+              return product(slf, slnf)->is_empty();
+            }
+          // cl(aut_f) x cl(aut_nf)
+        case '8':
+            {
+              return product(closure(aut_f), closure(aut_nf))->is_empty();
+            }
+        default:
+          throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
+          break;
+        }
+    }
+}

src/tgbaalgos/stutter_invariance.hh

@@ -0,0 +1,36 @@
+// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// 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_TGBAALGOS_STUTTER_INVARIANCE_HH
+# define SPOT_TGBAALGOS_STUTTER_INVARIANCE_HH
+
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+  // TODO doc
+  SPOT_API bool
+  is_stutter_invariant(const ltl::formula* f);
+
+  SPOT_API bool
+  is_stutter_invariant(const const_tgba_digraph_ptr& aut_f,
+		       const const_tgba_digraph_ptr& aut_nf, bdd aps);
+}
+
+#endif

src/tgbaalgos/stutterize.cc

@@ -0,0 +1,170 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
+// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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 "stutterize.hh"
+#include "tgba/tgba.hh"
+#include "dupexp.hh"
+#include "misc/hash.hh"
+#include "misc/hashfunc.hh"
+#include "ltlvisit/apcollect.hh"
+#include <deque>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace spot
+{
+  namespace
+  {
+    typedef std::pair<unsigned, bdd> stutter_state;
+
+    struct stutter_state_hash
+    {
+      size_t
+      operator()(const stutter_state& s) const
+      {
+	return wang32_hash(s.first) ^ wang32_hash(s.second.id());
+      }
+    };
+
+    // Associate the stutter state to its number.
+    typedef std::unordered_map<stutter_state, unsigned,
+			       stutter_state_hash> ss2num_map;
+
+    // Queue of state to be processed.
+    typedef std::deque<stutter_state> queue_t;
+  }
+
+  tgba_digraph_ptr
+  sl(const const_tgba_digraph_ptr& a, const ltl::formula* f)
+  {
+    bdd aps = atomic_prop_collect_as_bdd(f, a);
+    return sl(a, aps);
+  }
+
+  tgba_digraph_ptr
+  sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f)
+  {
+    bdd aps = atomic_prop_collect_as_bdd(f, a);
+    return sl2(a, aps);
+  }
+
+  tgba_digraph_ptr
+  sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
+  {
+    // The result automaton uses numbered states.
+    tgba_digraph_ptr res = make_tgba_digraph(a->get_dict());
+    // We use the same BDD variables as the input.
+    res->copy_ap_of(a);
+    res->copy_acceptance_conditions_of(a);
+    // These maps make it possible to convert stutter_state to number
+    // and vice-versa.
+    ss2num_map ss2num;
+
+    queue_t todo;
+
+    unsigned s0 = a->get_init_state_number();
+    stutter_state s(s0, bddfalse);
+    ss2num[s] = 0;
+    res->new_state();
+    todo.push_back(s);
+
+    while (!todo.empty())
+      {
+	s = todo.front();
+	todo.pop_front();
+	unsigned src = ss2num[s];
+
+	bool self_loop_needed = true;
+
+	for (auto& t : a->out(s.first))
+	  {
+	    bdd all = t.cond;
+	    while (all != bddfalse)
+	      {
+		bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
+		all -= one;
+
+		stutter_state d(t.dst, one);
+
+		auto r = ss2num.emplace(d, ss2num.size());
+		unsigned dest = r.first->second;
+
+		if (r.second)
+		  {
+		    todo.push_back(d);
+		    unsigned u = res->new_state();
+		    assert(u == dest);
+		    (void)u;
+		  }
+
+		// Create the transition.
+		res->new_transition(src, dest, one, t.acc);
+
+		if (src == dest)
+		  self_loop_needed = false;
+	      }
+	  }
+
+	if (self_loop_needed && s.second != bddfalse)
+	  res->new_transition(src, src, s.second, 0U);
+      }
+    res->merge_transitions();
+    return res;
+  }
+
+  tgba_digraph_ptr
+  sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
+  {
+    tgba_digraph_ptr res = tgba_dupexp_dfs(a);
+    unsigned num_states = res->num_states();
+    for (unsigned state = 0; state < num_states; ++state)
+      {
+	std::vector<unsigned> out;
+	auto trans = res->out(state);
+
+	for (auto it = trans.begin(); it != trans.end(); ++it)
+	  out.push_back(it.trans());
+	for (auto it: out)
+	  {
+	    if (res->trans_storage(it).dst != state)
+	      {
+		bdd all = res->trans_storage(it).cond;
+		while (all != bddfalse)
+		  {
+		    unsigned dst = res->trans_storage(it).dst;
+		    bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
+		    unsigned tmp = res->new_state();
+		    res->new_transition(state, tmp, one,
+					res->trans_storage(it).acc);
+		    res->new_transition(tmp, tmp, one, 0U);
+		    res->new_transition(tmp, dst, one,
+					res->trans_storage(it).acc);
+		    all -= one;
+		  }
+	      }
+	  }
+      }
+    res->merge_transitions();
+    return res;
+  }
+}

src/tgbaalgos/stutterize.hh

@@ -0,0 +1,43 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
+// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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_TGBAALGOS_STUTTERIZE_HH
+# define SPOT_TGBAALGOS_STUTTERIZE_HH
+
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+  SPOT_API tgba_digraph_ptr
+  sl(const const_tgba_digraph_ptr&, const ltl::formula*);
+
+  SPOT_API tgba_digraph_ptr
+  sl(const const_tgba_digraph_ptr&, bdd);
+
+  SPOT_API tgba_digraph_ptr
+  sl2(const const_tgba_digraph_ptr&, const ltl::formula*);
+
+  SPOT_API tgba_digraph_ptr
+  sl2(const const_tgba_digraph_ptr&, bdd);
+}
+
+#endif

src/tgbatest/Makefile.am

@@ -121,6 +121,7 @@ TESTS = \
   emptchk.test \
   emptchke.test \
   dfs.test \
+  stutter_invariant.test \
   ltlcrossce.test \
   emptchkr.test \
   ltlcounter.test \

src/tgbatest/ltl2tgba.cc

@@ -69,6 +69,8 @@
 #include "tgbaalgos/complete.hh"
 #include "tgbaalgos/dtbasat.hh"
 #include "tgbaalgos/dtgbasat.hh"
+#include "tgbaalgos/closure.hh"
+#include "tgbaalgos/stutterize.hh"
 
 #include "taalgos/tgba2ta.hh"
 #include "taalgos/dotty.hh"
@@ -376,6 +378,8 @@ checked_main(int argc, char** argv)
   bool reject_bigger = false;
   bool opt_monitor = false;
   bool containment = false;
+  bool opt_closure = false;
+  bool opt_stutterize = false;
   bool spin_comments = false;
   const char* hoaf_opt = 0;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
@@ -790,6 +794,14 @@ checked_main(int argc, char** argv)
 	{
 	  dupexp = BFS;
 	}
+      else if (!strcmp(argv[formula_index], "-CL"))
+	{
+	  opt_closure = true;
+	}
+      else if (!strcmp(argv[formula_index], "-ST"))
+	{
+	  opt_stutterize = true;
+	}
       else if (!strcmp(argv[formula_index], "-t"))
 	{
 	  output = 6;
@@ -1395,6 +1407,16 @@ checked_main(int argc, char** argv)
 	    }
 	}
 
+      if (opt_closure)
+	{
+	  a = closure(ensure_digraph(a));
+	}
+
+      if (opt_stutterize)
+	{
+	  a = sl(ensure_digraph(a), f);
+	}
+
       if (opt_monitor)
 	{
 	  tm.start("Monitor minimization");

src/tgbatest/stutter_invariant.test

@@ -0,0 +1,47 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2008, 2009, 2010, 2014 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
+# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
+# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+# Université Pierre et Marie Curie.
+#
+# 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
+
+set -e
+
+check_stutter()
+{
+  FORMULAS=$1
+  SPOT_STUTTER_CHECK=$2
+  run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >exp
+  for i in `seq $3 $4`
+  do
+    SPOT_STUTTER_CHECK=$i
+    run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >out
+    diff out exp
+  done
+}
+
+cat >ltl <<EOF
+Fp0 R Fp2
+G(p1 xor Xp2)
+EOF
+
+check_stutter ltl 0 1 8

wrap/python/spot.i

@@ -130,6 +130,8 @@ namespace std {
 #include "tgbaalgos/isdet.hh"
 #include "tgbaalgos/simulation.hh"
 #include "tgbaalgos/postproc.hh"
+#include "tgbaalgos/closure.hh"
+#include "tgbaalgos/stutterize.hh"
 
 #include "tgbaparse/public.hh"
 
@@ -260,6 +262,8 @@ namespace spot {
 %include "tgbaalgos/isdet.hh"
 %include "tgbaalgos/simulation.hh"
 %include "tgbaalgos/postproc.hh"
+%include "tgbaalgos/closure.hh"
+%include "tgbaalgos/stutterize.hh"
 
 %include "tgbaparse/public.hh"