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

@@ -15,6 +15,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:

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

spot/twaalgos/stutter.cc

@@ -409,6 +409,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
@@ -457,7 +462,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)

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