stutter: detect stutter-invariance at the state level

* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
stutter-invariance detection at the state level.
* python/spot/impl.i: Instantiate std::vector<bool>
* tests/python/stutter-inv-states.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.

NEWS

@@ -113,6 +113,12 @@ New in spot 2.4.1.dev (not yet released)
     can be passed to disable this behavior (or use -x degen-remscc=0
     from the command-line).
 
+  - In addition to detecting stutter-invariant formulas/automata, some
+    can now study a stutter-sensitive automaton and detect the subset
+    of states that are stutter-invariant.  See
+    https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html for
+    examples.
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)

doc/org/tut.org

@@ -83,3 +83,4 @@ real notebooks instead.
 - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
 - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
 - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata.
+- [[https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html][=stutter-inv-states.ipynb=]] detecting stutter-invariant formulas and states.

python/spot/impl.i

@@ -430,6 +430,7 @@ namespace std {
   %template(liststr) list<std::string>;
   %template(vectorformula) vector<spot::formula>;
   %template(vectorunsigned) vector<unsigned>;
+  %template(vectorbool) vector<bool>;
   %template(vectorstring) vector<string>;
   %template(atomic_prop_set) set<spot::formula>;
   %template(relabeling_map) map<spot::formula, spot::formula>;

spot/twaalgos/stutter.cc

@@ -30,12 +30,16 @@
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/dualize.hh>
 #include <spot/twa/twaproduct.hh>
 #include <spot/twa/bddprint.hh>
 #include <deque>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
+#include <numeric>
 
 namespace spot
 {
@@ -639,4 +643,117 @@ namespace spot
     aut->prop_stutter_invariant(is_stut);
     return is_stut;
   }
+
+  std::vector<bool>
+  stutter_invariant_states(const const_twa_graph_ptr& pos, formula f,
+                           bool local)
+  {
+    if (f.is_syntactic_stutter_invariant()
+        || pos->prop_stutter_invariant().is_true())
+      return std::vector<bool>(pos->num_states(), true);
+    auto neg = translator(pos->get_dict()).run(formula::Not(f));
+    return stutter_invariant_states(pos, neg, local);
+  }
+
+  // Based on an idea by Joachim Klein.
+  std::vector<bool>
+  stutter_invariant_states(const const_twa_graph_ptr& pos,
+                           const_twa_graph_ptr neg,
+                           bool local)
+  {
+    std::vector<bool> res(pos->num_states(), true);
+    if (pos->prop_stutter_invariant().is_true())
+      return res;
+
+    if (neg == nullptr)
+      {
+        spot::postprocessor p;
+        p.set_type(spot::postprocessor::Generic);
+        p.set_pref(spot::postprocessor::Deterministic);
+        p.set_level(spot::postprocessor::Low);
+        neg = dualize(p.run(std::const_pointer_cast<twa_graph>(pos)));
+      }
+
+    auto product_states = [](const const_twa_graph_ptr& a)
+      {
+        return (a->get_named_prop<std::vector<std::pair<unsigned, unsigned>>>
+                ("product-states"));
+      };
+
+    // Get the set of states (x,y) that appear in the product P1=pos*neg.
+    std::set<std::pair<unsigned, unsigned>> pairs = [&]()
+      {
+        twa_graph_ptr prod = spot::product(pos, neg);
+        auto goodstates = product_states(prod);
+        std::set<std::pair<unsigned, unsigned>> pairs(goodstates->begin(),
+                                                      goodstates->end());
+        return pairs;
+      }();
+
+    // Compute P2=cl(pos)*cl(neg).  A state x of pos is stutter-sensitive
+    // if there exists a state (x,y) in both P1 and P2 that as a successor
+    // in the useful part of P2 and that is not in P1.
+    twa_graph_ptr prod = spot::product(closure(pos), closure(neg));
+    auto prod_pairs = product_states(prod);
+    scc_info si(prod, scc_info_options::TRACK_SUCCS
+                | scc_info_options::TRACK_STATES_IF_FIN_USED);
+    si.determine_unknown_acceptance();
+    unsigned n = prod->num_states();
+    bool sinv = true;
+
+    for (unsigned s = 0; s < n; ++s)
+      {
+        if (!si.is_useful_scc(si.scc_of(s)))
+          continue;
+        if (pairs.find((*prod_pairs)[s]) == pairs.end())
+          continue;
+        for (auto& e: prod->out(s))
+          if (si.is_useful_scc(si.scc_of(e.dst)))
+            if (!local || pairs.find((*prod_pairs)[e.dst]) == pairs.end())
+              res[(*prod_pairs)[s].first] = sinv = false;
+      }
+    std::const_pointer_cast<twa_graph>(pos)->prop_stutter_invariant(sinv);
+    std::const_pointer_cast<twa_graph>(neg)->prop_stutter_invariant(sinv);
+    return res;
+  }
+
+  namespace
+  {
+    static
+    void highlight_vector(const twa_graph_ptr& aut,
+                          const std::vector<bool>& v,
+                          unsigned color)
+    {
+      // Create the highlight-states property only if it does not
+      // exist already.
+      auto hs =
+        aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states");
+      if (!hs)
+        {
+          hs = new std::map<unsigned, unsigned>;
+          aut->set_named_prop("highlight-states", hs);
+        }
+
+      unsigned n = v.size();
+      for (unsigned i = 0; i < n; ++i)
+        if (v[i])
+          hs->emplace(i, color);
+    }
+  }
+
+  void
+  highlight_stutter_invariant_states(const twa_graph_ptr& pos,
+                                     formula f, unsigned color,
+                                     bool local)
+  {
+    highlight_vector(pos, stutter_invariant_states(pos, f, local), color);
+  }
+
+  void
+  highlight_stutter_invariant_states(const twa_graph_ptr& pos,
+                                     const_twa_graph_ptr neg,
+                                     unsigned color, bool local)
+  {
+    highlight_vector(pos, stutter_invariant_states(pos, neg, local), color);
+  }
 }

spot/twaalgos/stutter.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2014-2017 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -73,4 +73,44 @@ namespace spot
   check_stutter_invariance(const twa_graph_ptr& aut,
                            formula f = nullptr,
                            bool do_not_determinize = false);
+
+
+  ///@{
+  /// \brief Determinate the states that are stutter-invariant in \a pos.
+  ///
+  /// The algorithm needs to compute the complement of \a pos. You can
+  /// avoid that costly operation by either supplying the complement
+  /// automaton, or supplying a formula for the (positive) automaton.
+  SPOT_API std::vector<bool>
+  stutter_invariant_states(const const_twa_graph_ptr& pos,
+                           const_twa_graph_ptr neg = nullptr,
+                           bool local = false);
+
+  SPOT_API std::vector<bool>
+  stutter_invariant_states(const const_twa_graph_ptr& pos, formula f_pos,
+                           bool local = false);
+  ///@}
+
+  ///@{
+  /// \brief Highlight the states of \a pos that are stutter-invariant.
+  ///
+  /// The algorithm needs to compute the complement of \a pos. You can
+  /// avoid that costly operation by either supplying the complement
+  /// automaton, or supplying a formula for the (positive) automaton.
+  ///
+  /// The \a color argument is an index in a predefined set of colors.
+  ///
+  /// This function simply works by calling
+  /// stutter_invariant_states(), and using the resulting vector to
+  /// setup the "highlight-states" property of the automaton.
+  SPOT_API void
+  highlight_stutter_invariant_states(const twa_graph_ptr& pos,
+                                     formula f_pos, unsigned color = 0,
+                                     bool local = false);
+  SPOT_API void
+  highlight_stutter_invariant_states(const twa_graph_ptr& pos,
+                                     const_twa_graph_ptr neg = nullptr,
+                                     unsigned color = 0,
+                                     bool local = false);
+  ///@}
 }

tests/Makefile.am

@@ -332,6 +332,7 @@ TESTS_ipython = \
   python/product.ipynb \
   python/randaut.ipynb \
   python/randltl.ipynb \
+  python/stutter-inv-states.ipynb \
   python/testingaut.ipynb \
   python/word.ipynb