From 77f3ba9478a199ee66bfbbdd923fa992ddfb939b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 7 Dec 2018 15:53:54 +0100
Subject: [PATCH] translate: fix stutter-invariant flag on leading Xs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Issue discovered by Mikuláš Klokočka and reported by František
Blahoudek.

* spot/twaalgos/translate.cc: Reset the stutter-invariant flag
when adding extra transitions for leading Xs.
* tests/core/stutter-tgba.test: New test case.
* NEWS: Mention the bug.
---
 NEWS                         |  4 ++++
 spot/twaalgos/translate.cc   |  4 ++++
 tests/core/stutter-tgba.test | 10 ++++++++++
 3 files changed, 18 insertions(+)

diff --git a/NEWS b/NEWS
index 2c1732adb..051aa9f4a 100644
--- a/NEWS
+++ b/NEWS
@@ -90,6 +90,10 @@ New in spot 2.6.3.dev (not yet released)
 
   Bugs fixed:
 
+  - translate() would incorrectly mark as stutter-invariant
+    some automata produced from formulas of the form X(f...)
+    where f... is syntactically stutter-invariant.
+
   - acc_cond::is_generalized_rabin() and
     acc_cond::is_generalized_streett() did not recognize the cases
     were a single generalized pair is used.
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index 4f50117a0..9fee4e847 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -313,6 +313,10 @@ namespace spot
               }
             while (--leading_x);
             aut->set_init_state(init);
+            // Adding initial edges is very likely to kill stutter
+            // invariance (and it certainly cannot fix it).
+            if (aut->prop_stutter_invariant().is_true())
+              aut->prop_stutter_invariant(trival::maybe());
           }
       }
     else
diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test
index 2d81b7778..fd3d26f1a 100755
--- a/tests/core/stutter-tgba.test
+++ b/tests/core/stutter-tgba.test
@@ -103,6 +103,16 @@ test `autfilt -c --is-stutter-invariant input` = 0
 grep '!deterministic' input.2
 grep '!stutter-invariant' input.2
 
+# From an email by František Blahoudek and Mikuláš Klokočka
+ltl2tgba 'X(a & GF(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
+test `autfilt -c --is-stutter-invariant input` = 0
+grep '!deterministic' input.2
+grep '!stutter-invariant' input.2
+
 
 # From an email by Anton Pirogov
 cat >pirogov <<EOF