From a9c457f93fb38569849d8d1318c74dc16009cfcd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 23 Jan 2023 11:59:49 +0100
Subject: [PATCH] dbranch: fix handling of states without successors
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #524, reported by Rüdiger Ehlers.

* spot/twaalgos/dbranch.cc: When merging an edge going to state
without successors simply delete it.
* bin/spot-x.cc: Typo in documentation.
* tests/core/ltlcross.test: Add a test case.
* NEWS: Mention the bug.
---
 NEWS                     |  4 ++++
 bin/spot-x.cc            |  4 ++--
 spot/twaalgos/dbranch.cc | 39 +++++++++++++++++++++------------------
 tests/core/ltlcross.test |  5 ++++-
 4 files changed, 31 insertions(+), 21 deletions(-)

diff --git a/NEWS b/NEWS
index d6f6a702b..d25bf4ff4 100644
--- a/NEWS
+++ b/NEWS
@@ -24,6 +24,10 @@ New in spot 2.11.3.dev  (not yet released)
     multiple initial states (because Spot supports only one), the HOA
     parser could break state-based acceptance.  (Issue #522.)
 
+  - delay_branching_here(), a new optimization of Spot 2.11 had an
+    incorrectly handling of states without successors, causing some
+    segfaults.  (Issue #524.)
+
 New in spot 2.11.3  (2022-12-09)
 
   Bug fixes:
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index 1edb3f54e..964710dc1 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -53,7 +53,7 @@ implication-based simplifications are attempted.  Defaults to 16.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("ltl-split", "Set to 0 to disable the translation of automata \
 as product or sum of subformulas.") },
-    { DOC("branch-prop", "Set to 0 to disable branching-postponement \
+    { DOC("branch-post", "Set to 0 to disable branching-postponement \
 (done during translation, may create more states) and delayed-branching \
 (almost similar, but done after translation to only remove states).  \
 Set to 1 to force branching-postponement, and to 2 \
diff --git a/spot/twaalgos/dbranch.cc b/spot/twaalgos/dbranch.cc
index 465f8326e..19a0d9474 100644
--- a/spot/twaalgos/dbranch.cc
+++ b/spot/twaalgos/dbranch.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2022-2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -118,27 +118,30 @@ namespace spot
                   continue;
                 }
               unsigned mergedst = it2->second;
-              // we have to merge canddst into mergedst.  This is as
-              // simple as:
+              // we have to merge canddst into mergedst.
+              // This is as simple as:
               // 1) connecting their list of transitions
-              unsigned& mergedfirst = g.state_storage(mergedst).succ;
-              unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
-              unsigned& candfirst = g.state_storage(canddst).succ;
               unsigned& candlast = g.state_storage(canddst).succ_tail;
-              if (mergedlast)
-                aut->edge_storage(mergedlast).next_succ = candfirst;
-              else              // mergedst had now successor
-                mergedfirst = candfirst;
-              mergedlast = candlast;
-              // 2) updating the source of the merged transitions
-              for (unsigned e2 = candfirst; e2 != 0;)
+              if (candlast)
                 {
-                  auto& edge = aut->edge_storage(e2);
-                  edge.src = mergedst;
-                  e2 = edge.next_succ;
+                  unsigned& mergedfirst = g.state_storage(mergedst).succ;
+                  unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
+                  unsigned& candfirst = g.state_storage(canddst).succ;
+                  if (mergedlast)
+                    aut->edge_storage(mergedlast).next_succ = candfirst;
+                  else              // mergedst had no successor
+                    mergedfirst = candfirst;
+                  mergedlast = candlast;
+                  // 2) updating the source of the merged transitions
+                  for (unsigned e2 = candfirst; e2 != 0;)
+                    {
+                      auto& edge = aut->edge_storage(e2);
+                      edge.src = mergedst;
+                      e2 = edge.next_succ;
+                    }
+                  // 3) deleting the edge to canddst.
+                  candfirst = candlast = 0;
                 }
-              // 3) deleting the edge to canddst.
-              candfirst = candlast = 0;
               it.erase();
               // 4) updating succ_cand
               succ_cand[mergedst] += succ_cand[canddst];
diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test
index 1a5806ba8..ebe20fb26 100755
--- a/tests/core/ltlcross.test
+++ b/tests/core/ltlcross.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012-2014, 2016, 2019 Laboratoire de Recherche et
+# Copyright (C) 2012-2014, 2016, 2019, 2023 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -65,3 +65,6 @@ ltlcross -D \
 # Spot 2.8.  We use ltl2tgba twice so ltlcross build cross-products.
 ltlcross --verbose ltl2tgba ltl2tgba \
 -f '(G(F((a1)&(X(X(b1))))))&(G(F((a2)&(X(X(b2))))))&(G(F((a3)&(X(X(b3))))))'
+
+# Issue #524.
+ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))'