From 0940c9a25a2281dd0220229515bac98b0e278ff4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 12 Mar 2020 21:54:13 +0100
Subject: [PATCH] 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/python/stutter.py: Add test cases.
---
 spot/twaalgos/stutter.cc | 53 ++++++++++++++++++++++++++++++++++++----
 tests/python/stutter.py  | 15 +++++++++++-
 2 files changed, 62 insertions(+), 6 deletions(-)

diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc
index 0a58294c3..af47a3c50 100644
--- a/spot/twaalgos/stutter.cc
+++ b/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.
@@ -276,6 +276,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;
@@ -318,7 +331,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;
@@ -335,6 +348,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();
@@ -378,10 +421,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.
-                i = a->new_edge(tmp, dst, one, {});
+                // unsat acceptance here to preserve the state-based property.
+                i = a->new_edge(tmp, dst, one, unsat);
                 assert(i > num_edges);
                 (void)i;
               }
diff --git a/tests/python/stutter.py b/tests/python/stutter.py
index 48240f940..7a7586190 100644
--- a/tests/python/stutter.py
+++ b/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()