stutter: complement non-det automata via determinization

Fixes #164.

* spot/twaalgos/stutter.hh, spot/twaalgos/stutter.cc: Implement
the determinization, while keeping it optional.
* NEWS: Mention the change.
* tests/core/ltl2dstar.test, tests/core/stutter-tgba.test: Add
test cases.
* tests/core/readsave.test: Adjust.

NEWS

@@ -103,9 +103,14 @@ New in spot 2.0.3a (not yet released)
     the two others, is currently restricted to automata with Fin-less
     acceptance.
 
+  * spot::check_stutter_invariance() can now work on non-deterministic
+    automata for which no corresponding formula is known.  This
+    implies that "autfilt --check=stutter" will now label all
+    automata, not just deterministic automata.
+
   Python:
 
-  * The __format__() method for formula support the same
+  * The __format__() method for formula supports the same
     operator-rewritting feature introduced in ltldo and ltlcross.
     So "{:[i]s}".format(f) is the same as
     "{:s}".format(f.unabbreviate("i")).
@@ -114,7 +119,7 @@ New in spot 2.0.3a (not yet released)
 
   * Bindings for randomize() were added.
 
-  * Under IPython the spot.ltsmin modules now offers a
+  * Under IPython the spot.ltsmin module now offers a
     %%pml magic to define promela models, compile them
     with spins, and dynamically load them.   This is
     akin to the %%dve magic that was already supported.

spot/twaalgos/stutter.cc

@@ -29,6 +29,7 @@
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/postproc.hh>
 #include <spot/twa/twaproduct.hh>
 #include <spot/twa/bddprint.hh>
 #include <deque>
@@ -606,7 +607,8 @@ namespace spot
   }
 
   trival
-  check_stutter_invariance(const twa_graph_ptr& aut, formula f)
+  check_stutter_invariance(const twa_graph_ptr& aut, formula f,
+                           bool do_not_determinize)
   {
     trival is_stut = aut->prop_stutter_invariant();
     if (is_stut.is_known())
@@ -619,12 +621,18 @@ namespace spot
       }
     else
       {
-        // If the automaton is deterministic, we
+        twa_graph_ptr tmp = aut;
-        // know how to complement it.
+        if (!is_deterministic(aut))
-        aut->prop_deterministic(is_deterministic(aut));
+          {
-        if (!aut->prop_deterministic())
+            if (do_not_determinize)
               return trival::maybe();
-        neg = remove_fin(dtwa_complement(aut));
+            spot::postprocessor p;
+            p.set_type(spot::postprocessor::Generic);
+            p.set_pref(spot::postprocessor::Deterministic);
+            p.set_level(spot::postprocessor::Low);
+            tmp = p.run(aut);
+          }
+        neg = dtwa_complement(tmp);
       }
 
     is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),

spot/twaalgos/stutter.hh

@@ -60,13 +60,17 @@ namespace spot
 
   /// \brief Check whether \a aut is stutter-invariant
   ///
-  /// This procedure only works if \a aut is deterministic, or if the
+  /// This procedure requires the negation of \a aut to
-  /// equivalent formula \a f is given.  The stutter-invariant property
+  /// be computed.  This is easily done of \a aut is deterministic
-  /// of the automaton is updated and also returned.
+  /// or if a formula represented by \a aut is known.  Otherwise
+  /// \a aut will be complemented by determinization, which can
+  /// be expansive.   The determinization can be forbidden using
+  /// the \a do_not_determinize flag.
   ///
-  /// If no formula is given and the automaton is not deterministic,
+  /// If no complemented automaton could be constructed, the
   /// the result will be returned as trival::maybe().
   SPOT_API trival
   check_stutter_invariance(const twa_graph_ptr& aut,
-                           formula f = nullptr);
+                           formula f = nullptr,
+                           bool do_not_determinize = false);
 }

tests/core/ltl2dstar.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -95,3 +95,7 @@ State: 4 {0}
 --END--
 EOF
 diff out.hoa expected
+
+# Test the stutter-invariant check on Rabin
+autfilt --trust-hoa=no --check=stutter out.hoa -H1.1 |
+    grep ' stutter-invariant'

tests/core/readsave.test

@@ -938,7 +938,8 @@ Start: 1
 AP: 0
 acc-name: generalized-Buchi 2
 Acceptance: 2 Inf(0)&Inf(1)
-properties: trans-labels explicit-labels trans-acc inherently-weak
+properties: trans-labels explicit-labels trans-acc stutter-invariant
+properties: inherently-weak
 --BODY--
 State: 0
 [t] 1 {0}

tests/core/stutter-tgba.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
-# de l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -42,7 +42,7 @@ $autfilt --states=12 prod.hoa -q
 #
 # We just run those without checking the output, it is enough to
 # trigger assertions in the HOA output routines.
-run 0 $ltl2tgba -H 'X(a U b)' > det.hoa
+$ltl2tgba -H 'X(a U b)' > det.hoa
 run 0 $autfilt --destut det.hoa -H
 run 0 $autfilt --instut=1 det.hoa -H
 run 0 $autfilt --instut=2 det.hoa -H
@@ -72,16 +72,33 @@ EOF
 
 diff output expected
 
-run 0 $ltl2tgba -H 'F(a & X(!a & b))' > input
+$ltl2tgba -H 'F(a & X(!a & b))' > input
-grep stutter-invariant input && exit 1
+grep ' stutter-invariant' input && exit 1
 run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
-grep stutter-invariant input.2
+grep ' stutter-invariant' input.2
 run 0 $autfilt --check=stutter input > input.2
-grep stutter-invariant input.2
+grep ' stutter-invariant' input.2
 
-run 0 $ltl2tgba -H 'F(a & X(a & b))' > input
+$ltl2tgba 'F(a & X(a & b))' > input
 grep stutter-invariant input && exit 1
-run 0 $ltl2tgba --check=stutter 'F(a & X(a & b))' > input.2
+# HOA v1.1 calls it "!stutter-invariant"
-grep stutter-sensitive input.2
+run 0 $ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
+grep '!stutter-invariant' input.2
+# HOA v1 has no name, so we use "stutter-sensitive"
 run 0 $autfilt --check=stutter input > input.2
 grep stutter-sensitive input.2
+
+$ltl2tgba 'F(a & X(!a & Gb))' > input
+grep stutter-invariant input && exit 1
+grep deterministic input && exit 1
+# This will involve a complementation
+run 0 $autfilt --check=stutter input > input.2
+grep ' stutter-invariant' input.2
+
+$ltl2tgba 'F(a & X(a & Gb))' > input
+grep stutter input && exit 1
+grep deterministic input && exit 1
+# This will involve a complementation
+run 0 $autfilt -H1.1 --check=stutter input > input.2
+grep '!deterministic' input.2
+grep '!stutter-invariant' input.2