From 80fd158ed5fd60439dea2490a4fbbb9ed63261fa Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 16 Dec 2021 17:23:06 +0100
Subject: [PATCH] sbacc: remove spurious initial state in some output
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes #492, based on a report from Jérôme Dubois.

* spot/twaalgos/sbacc.cc: If the initial state is in a rejecting
component, start with an initial state whose colors are unsat_mark.
* tests/core/sbacc.test: Add test case.
* tests/python/pdegen.py: Adjust it.
---
 NEWS                   |  6 +++++-
 spot/twaalgos/sbacc.cc |  2 ++
 tests/core/sbacc.test  | 34 ++++++++++++++++++++++++++++++++++
 tests/python/pdegen.py | 12 ++++++------
 4 files changed, 47 insertions(+), 7 deletions(-)

diff --git a/NEWS b/NEWS
index 4ca413e07..12176da5e 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,10 @@
 New in spot 2.10.2.dev  (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - On automata where the absence of color is not rejecting
+    (e.g. co-Büchi) and where the initial state was in a rejecting
+    SCC, sbacc() could output a superflous state.  (Issue #492)
 
 New in spot 2.10.2  (2021-12-03)
 
diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc
index c64ca321f..e79cba774 100644
--- a/spot/twaalgos/sbacc.cc
+++ b/spot/twaalgos/sbacc.cc
@@ -145,6 +145,8 @@ namespace spot
           // Use any edge going into the initial state to set the first
           // acceptance mark.
           init_acc = one_in[s] | common_out[s];
+        else
+          init_acc = unsat_mark.second;
 
         old_st.push_back(new_state(s, init_acc));
       }
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index d694fa831..715001b7b 100755
--- a/tests/core/sbacc.test
+++ b/tests/core/sbacc.test
@@ -289,3 +289,37 @@ State: 0 [0] 0 {0}
 State: 1 [0] 1 [0] 0
 --END--
 EOF
+
+autfilt -S > out <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 1
+State: 1
+[1] 1 {0}
+--END--
+EOF
+cat >exp <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels state-acc colored
+--BODY--
+State: 0 {0}
+[0] 0
+[1] 1
+State: 1 {0}
+[1] 1
+--END--
+EOF
+diff out exp
diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py
index 66c89b117..02150d375 100644
--- a/tests/python/pdegen.py
+++ b/tests/python/pdegen.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019, 2020 Laboratoire de Recherche et Développement de
+# Copyright (C) 2019, 2020, 2021 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -124,8 +124,8 @@ assert dehoa == """HOA: v1
 States: 4
 Start: 0
 AP: 1 "p0"
-acc-name: parity max even 2
-Acceptance: 2 Fin(1) & Inf(0)
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
@@ -134,11 +134,11 @@ State: 0 "0#0"
 [!0] 2
 State: 1 "1#0"
 [!0] 2
-[0] 3 {0 1}
+[0] 3 {0}
 State: 2 "3#0"
-[t] 2 {0}
+[t] 2
 State: 3 "2#0"
-[0] 1 {0 1}
+[0] 1 {0}
 [!0] 2
 --END--"""