From 858629dd3ad9b13e253f187cc1ea71e098c3d911 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 20 Sep 2023 00:00:15 +0200
Subject: [PATCH] twagraph: fix merge_states() on automata without edges

This corner case was simply causing segfaults.

* tests/python/mergedge.py: Add a test case.
* spot/twa/twagraph.cc (merge_states): Add special handling for
the case where the automaton has no edges.
---
 spot/twa/twagraph.cc     | 23 ++++++++++++++++++-----
 tests/python/mergedge.py | 22 +++++++++++++++++++++-
 2 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index 3f74d4d99..50145803d 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -363,6 +363,24 @@ namespace spot
       throw std::runtime_error(
           "twa_graph::merge_states() does not work on alternating automata");
 
+    const unsigned n_states = num_states();
+
+    const auto& e_vec = edge_vector();
+    unsigned n_edges = e_vec.size();
+    if (n_edges <= 1)
+      {
+        if (n_states == 1)
+          return 0;
+        // We don't have a very convenient way to resize the state
+        // vector.
+        std::vector<unsigned> remap(n_states, -1U);
+        remap[0] = 0;
+        get_graph().defrag_states(remap, 1);
+        SPOT_ASSERT(num_states() == 1);
+        set_init_state(0);
+        return n_states - 1;
+      }
+
 #ifdef ENABLE_PTHREAD
     const unsigned nthreads = ppolicy.nthreads();
 #else
@@ -387,8 +405,6 @@ namespace spot
     }, nthreads);
     g_.chain_edges_();
 
-    const unsigned n_states = num_states();
-
     // Edges are nicely chained and there are no erased edges
     // -> We can work with the edge_vector
 
@@ -406,9 +422,6 @@ namespace spot
     for (unsigned i = 0; i < n_states; ++i)
       hash_of_state.push_back(i);
 
-    const auto& e_vec = edge_vector();
-    unsigned n_edges = e_vec.size();
-
     // For each state we need 4 indices of the edge vector
     // [first, first_non_sfirst_selflooplfloop, first_selfloop, end]
     // The init value makes sure nothing is done for dead end states
diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py
index b3e934946..e2c88874e 100644
--- a/tests/python/mergedge.py
+++ b/tests/python/mergedge.py
@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020-2023 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -56,6 +56,26 @@ aut.merge_edges()
 tc.assertEqual(aut.num_edges(), 5)
 tc.assertTrue(spot.is_deterministic(aut))
 
+aut = spot.automaton("""
+HOA: v1
+States: 3
+Start: 2
+AP: 0
+Acceptance: 0 t
+--BODY--
+State: 0
+State: 1
+State: 2
+--END--""")
+tc.assertEqual(aut.num_states(), 3)
+tc.assertEqual(aut.num_edges(), 0)
+tc.assertEqual(aut.get_init_state_number(), 2)
+tc.assertEqual(aut.merge_states(), 2);
+tc.assertEqual(aut.num_states(), 1)
+tc.assertEqual(aut.num_edges(), 0)
+tc.assertEqual(aut.get_init_state_number(), 0)
+tc.assertEqual(aut.merge_states(), 0);
+
 for nthread in range(1, 16, 2):
     aut = spot.automaton("""
     HOA: v1