From 0e54a853104f1124fd7dd60546cbbc14e9985d41 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 18 Apr 2023 15:04:58 +0200
Subject: [PATCH] powerset: fix segfault when the initial state is a sink

Reported by Raven Beutner.

* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
---
 NEWS                      |  3 +++
 spot/twaalgos/minimize.cc |  6 +++---
 spot/twaalgos/powerset.cc | 26 ++++++++++++++------------
 tests/core/wdba2.test     | 37 +++++++++++++++++++++++++++++++++++--
 4 files changed, 55 insertions(+), 17 deletions(-)

diff --git a/NEWS b/NEWS
index 7fbb4f66a..32ef6b9ed 100644
--- a/NEWS
+++ b/NEWS
@@ -30,6 +30,9 @@ New in spot 2.11.4.dev  (not yet released)
     verbatim.  We also changed the behavior of as_twa() to not merge
     identical states.
 
+  - Fix segfaults occuring in determinization of 1-state terminal
+    automata.
+
 New in spot 2.11.4  (2023-02-10)
 
   Python:
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 4fd6847b3..1ac961d46 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2010-2020, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -394,8 +394,8 @@ namespace spot
       else
         {
           // Find any accepting sink state, to speed up the
-          // determinization by merging all states containing a sink
-          // state.
+          // determinization by merging all macro-states containing a
+          // sink state.
           std::vector<unsigned> acc_sinks;
           unsigned ns = a->num_states();
           if (!a->prop_terminal().is_true())
diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc
index c5fc07f94..326de7c76 100644
--- a/spot/twaalgos/powerset.cc
+++ b/spot/twaalgos/powerset.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2011, 2013-2019, 2021 Laboratoire de Recherche et
+// Copyright (C) 2009-2011, 2013-2019, 2021, 2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -217,17 +217,19 @@ namespace spot
         pm.map_.emplace_back(std::move(ps));
       }
 
-    {
-      unsigned init_num = aut->get_init_state_number();
-      auto bvi = make_bitvect(ns);
-      bvi->set(init_num);
-      power_state ps{init_num};
-      unsigned num = res->new_state();
-      res->set_init_state(num);
-      seen[bvi] = num;
-      assert(pm.map_.size() == num);
-      pm.map_.emplace_back(std::move(ps));
-      toclean.emplace_back(bvi);
+    // Add the initial state unless it's a sink.
+    if (unsigned init_num = aut->get_init_state_number();
+        !acc_sinks || !acc_sinks->get(init_num))
+      {
+        auto bvi = make_bitvect(ns);
+        bvi->set(init_num);
+        power_state ps{init_num};
+        unsigned num = res->new_state();
+        res->set_init_state(num);
+        seen[bvi] = num;
+        assert(pm.map_.size() == num);
+        pm.map_.emplace_back(std::move(ps));
+        toclean.emplace_back(bvi);
     }
 
     // outgoing map
diff --git a/tests/core/wdba2.test b/tests/core/wdba2.test
index ca49bad94..3850a447a 100755
--- a/tests/core/wdba2.test
+++ b/tests/core/wdba2.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2014, 2015, 2018, 2019 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2012, 2014-2015, 2018-2019, 2023 Laboratoire de
+# Recherche et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -82,3 +82,36 @@ EOF
 
 autfilt --small --high -C -Hi input > output
 diff output expected
+
+# This test comes from a report from Raven Beutner and used to cause a
+# segfault.
+cat >input <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 3  "l0" "l1" "l2"
+acc-name: generalized-Buchi 0
+Acceptance: 0 t
+--BODY--
+State: 0
+[0&1] 0
+[2] 0
+[!2] 0
+--END--
+EOF
+autfilt --small -S input >output
+cat >expected <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic terminal
+--BODY--
+State: 0 {0}
+[t] 0
+--END--
+EOF
+diff output expected