From 69a3e8486eb8c3d0e0c16ab4339720f7626cde04 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Mar 2018 18:20:35 +0100
Subject: [PATCH] stutter: fix closure() on Fin-acceptance

From a report by Anton Pirogov.

* NEWS: Mention the bug.
* spot/twaalgos/stutter.cc: Fix it.
* tests/core/stutter-tgba.test: Test it.
* THANKS: Add Anton.
---
 NEWS                         |  8 ++++++++
 THANKS                       |  1 +
 spot/twaalgos/stutter.cc     |  7 ++++++-
 tests/core/stutter-tgba.test | 27 ++++++++++++++++++++++++++-
 4 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 146c46a0c..54247730c 100644
--- a/NEWS
+++ b/NEWS
@@ -42,6 +42,14 @@ New in spot 2.5.1.dev (not yet released)
   - twa_run methods will now diagnose cases where the cycle is
     unexpectedly empty instead of segfaulting.
 
+  - spot::closure(), used by default for testing stutter-invariance,
+    was using an optimization incorrect if the acceptance condition
+    had some Fin(x).  Consequently stutter-invariance tests for
+    automata, for instance with "autfilt --is-stutter-invariant",
+    could be to be wrong (even if the input does not use Fin(x), its
+    complement, used in the stutter-invariance test likely will).
+    Stutter-invariance checks of LTL formulas are not affected.
+
 New in spot 2.5.1 (2018-02-20)
 
   Library:
diff --git a/THANKS b/THANKS
index 9001306dc..5c6151aee 100644
--- a/THANKS
+++ b/THANKS
@@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or
 suggestions.
 
 Akim Demaille
+Anton Pirogov
 Ayrat Khalimov
 Caroline Lemieux
 Christian Dax
diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc
index abfd956e6..47a09454f 100644
--- a/spot/twaalgos/stutter.cc
+++ b/spot/twaalgos/stutter.cc
@@ -410,6 +410,11 @@ namespace spot
   twa_graph_ptr
   closure_inplace(twa_graph_ptr a)
   {
+    // In the fin-less version of the closure, we can merge edges that
+    // have the same src, letter, and destination by taking the union
+    // of their marks.  If some Fin() is used, we cannot do that.
+    bool fin_less = !a->acc().uses_fin_acceptance();
+
     a->prop_keep({false,        // state_based
                   false,        // inherently_weak
                   false, false, // deterministic
@@ -458,7 +463,7 @@ namespace spot
                             need_new_trans = false;
                             break;
                           }
-                        else if (cond == ts.cond)
+                        else if (fin_less && cond == ts.cond)
                           {
                             acc |= ts.acc;
                             if (ts.acc != acc)
diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test
index 90d0c8e65..05a81e51a 100755
--- a/tests/core/stutter-tgba.test
+++ b/tests/core/stutter-tgba.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014-2017 Laboratoire de Recherche et
+# Copyright (C) 2014-2018 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -102,3 +102,28 @@ 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
+HOA: v1
+name: "Evil(1)"
+States: 2
+Start: 0
+AP: 1 "p"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[t] 0
+[0] 1
+State: 1 {0}
+[0] 0
+--END--
+EOF
+
+for i in 1 2 3 4 5 6 7 8; do
+    test 0 = `SPOT_STUTTER_CHECK=$i \
+              autfilt pirogov --is-stutter-invariant -c` || exit 1
+done