stutter: fix sl, sl2 to never accept on added self-loop

Fixes #401, reported by Victor Khomenko.

* spot/twaalgos/stutter.cc (sl, sl2): If {} is accepting, upgrade the
acceptance condition.
* tests/core/stutter-tgba.test, tests/python/stutter.py: Add test cases.

spot/twaalgos/stutter.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement de
+// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -277,6 +277,19 @@ namespace spot
     // We use the same BDD variables as the input.
     res->copy_ap_of(a);
     res->copy_acceptance_of(a);
+
+    // We are going to create self-loop labeled by {},
+    // and those should not be accepting.  If they are,
+    // we need to upgrade the acceptance condition.
+    acc_cond::mark_t toadd = {};
+    if (res->acc().accepting({}))
+      {
+        unsigned ns = res->num_sets();
+        auto na = res->get_acceptance() & acc_cond::acc_code::inf({ns});
+        res->set_acceptance(ns + 1, na);
+        toadd = {ns};
+      }
+
     // These maps make it possible to convert stutter_state to number
     // and vice-versa.
     ss2num_map ss2num;
@@ -319,7 +332,7 @@ namespace spot
                   }
 
                 // Create the edge.
-                res->new_edge(src, dest, one, t.acc);
+                res->new_edge(src, dest, one, t.acc | toadd);
 
                 if (src == dest)
                   self_loop_needed = false;
@@ -336,6 +349,36 @@ namespace spot
   twa_graph_ptr
   sl2_inplace(twa_graph_ptr a)
   {
+    // We are going to create self-loop labeled by {},
+    // and those should not be accepting.  If they are,
+    // we need to upgrade the acceptance condition.
+    if (a->acc().accepting({}))
+      {
+        unsigned ns = a->num_sets();
+        auto na = a->get_acceptance() & acc_cond::acc_code::inf({ns});
+        a->set_acceptance(ns + 1, na);
+        acc_cond::mark_t toadd = {ns};
+        for (auto& e: a->edges())
+          e.acc |= toadd;
+      }
+
+    // The self-loops we add should not be accepting, so try to find
+    // an unsat mark, and upgrade the acceptance condition if
+    // necessary.
+    //
+    // UM is a pair (bool, mark).  If the Boolean is false, the
+    // acceptance is always satisfiable.  Otherwise, MARK is an
+    // example of unsatisfiable mark.
+    auto um = a->acc().unsat_mark();
+    if (!um.first)
+      {
+        auto m = a->set_buchi();
+        for (auto& e: a->edges())
+          e.acc = m;
+        um.second = {};
+      }
+    acc_cond::mark_t unsat = um.second;
+
     bdd atomic_propositions = a->ap_vars();
     unsigned num_states = a->num_states();
     unsigned num_edges = a->num_edges();
@@ -379,10 +422,10 @@ namespace spot
                 unsigned tmp = p.first->second; // intermediate state
                 unsigned i = a->new_edge(src, tmp, one, acc);
                 assert(i > num_edges);
-                i = a->new_edge(tmp, tmp, one, {});
+                i = a->new_edge(tmp, tmp, one, unsat);
                 assert(i > num_edges);
-                // No acceptance here to preserve the state-based property.
+                // unsat acceptance here to preserve the state-based property.
-                i = a->new_edge(tmp, dst, one, {});
+                i = a->new_edge(tmp, dst, one, unsat);
                 assert(i > num_edges);
                 (void)i;
               }
@@ -704,7 +747,7 @@ namespace spot
     else
       {
         rword = aword;
-        aword = sl2(aaut)->intersecting_word(neg);
+        aword = sl2(aaut)->intersecting_word(aut);
         aword->simplify();
       }
     std::ostringstream os;

tests/core/stutter-tgba.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014-2019 Laboratoire de Recherche et
+# Copyright (C) 2014-2020 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -156,4 +156,12 @@ grep ' stutter-invariant' out
 grep -q '^spot.accepted-word: "' out && exit 1
 grep -q '^spot.rejected-word: "' out && exit 1
 
+
+ltl2tgba 'G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))' \
+         --check=stutter-sensitive-example > out
+grep ' stutter-sensitive' out
+grep -F 'spot-accepted-word: "cycle{!Y1 & !Y2 & x; Y1 & Y2 & x;' out
+grep -F 'spot-rejected-word: "cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}' out
+
+
 :

tests/python/stutter.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2019, 2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -47,3 +47,16 @@ def explain_stut(f):
 w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc')
 assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}'
 assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}'
+
+# Test from issue #401
+w1, w2 = explain_stut('G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))')
+assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}'
+assert str(w2) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}'
+
+# Related to issue #401 as well.  sl() and sl2() should upgrade
+# the t acceptance condition into inf(0).
+pos = spot.translate('Xa & XXb')
+w = pos.accepting_word().as_automaton()
+assert w.acc().is_t()
+assert not spot.sl2(w).acc().is_buchi()
+assert not spot.sl(w).acc().is_buchi()