dbranch: fix handling of state-based acceptance

Fixes issue #525.

* spot/twaalgos/dbranch.hh, NEWS: Document.
* spot/twaalgos/dbranch.cc: Detect cases where the acceptance should
be changed from state-based to transition-based.
* tests/python/dbranch.py: Add a test case.

NEWS

@@ -32,6 +32,10 @@ New in spot 2.11.3.dev  (not yet released)
     incorrectly handling of states without successors, causing some
     segfaults.  (Issue #524.)
 
+  - Running delay_branching_here() on state-based automata (this was not
+    done in Spot so far) may require the output to use transition-based
+    acceptance.  (Issue #525.)
+
 New in spot 2.11.3  (2022-12-09)
 
   Bug fixes:

spot/twaalgos/dbranch.cc

@@ -66,6 +66,10 @@ namespace spot
       hashmap_t first_dest[1 + is_game];
       auto& g = aut->get_graph();
 
+      // Merging outgoing transitions may cause the automaton to need
+      // transition-based acceptance.
+      bool need_trans = !aut->prop_state_acc().is_true();
+
       // setup a DFS
       std::vector<bool> seen(ns);
       std::stack<unsigned> todo;
@@ -128,9 +132,18 @@ namespace spot
                   unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
                   unsigned& candfirst = g.state_storage(canddst).succ;
                   if (mergedlast)
-                    aut->edge_storage(mergedlast).next_succ = candfirst;
+                    {
+                      aut->edge_storage(mergedlast).next_succ = candfirst;
+                      // Do we need to require transition-based acceptance?
+                      if (!need_trans)
+                        need_trans =
+                          (aut->edge_storage(candfirst).acc
+                           != aut->edge_storage(mergedfirst).acc);
+                    }
                   else              // mergedst had no successor
-                    mergedfirst = candfirst;
+                    {
+                      mergedfirst = candfirst;
+                    }
                   mergedlast = candlast;
                   // 2) updating the source of the merged transitions
                   for (unsigned e2 = candfirst; e2 != 0;)
@@ -149,6 +162,8 @@ namespace spot
               changed = true;
             }
         }
+      if (need_trans)
+        aut->prop_state_acc(false);
       return changed;
     }
   }

spot/twaalgos/dbranch.hh

@@ -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.
@@ -26,10 +26,15 @@ namespace spot
   /// \ingroup twa_algorithms
   /// \brief Merge states to delay
   ///
-  /// If a state (x) has two outgoing transitions (x,l,m,y) and
-  /// (x,l,m,z) going to states (x) and (y) that have no other
-  /// incoming edges, then (y) and (z) can be merged (keeping the
-  /// union of their outgoing destinations).
+  /// In an automaton with transition-based acceptance, if a state (x)
+  /// has two outgoing transitions (x,l,m,y) and (x,l,m,z) going to
+  /// states (x) and (y) that have no other incoming edges, then (y)
+  /// and (z) can be merged (keeping the union of their outgoing
+  /// destinations).
+  ///
+  /// If the input automaton uses state-based acceptance, running this
+  /// function might make the acceptance transition-based, but only if
+  /// two states with different acceptance are merged at some point.
   ///
   /// \return true iff the automaton was modified.
   SPOT_API bool delay_branching_here(const twa_graph_ptr& aut);

tests/python/dbranch.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2022 Laboratoire de Recherche et
+# Copyright (C) 2022, 2023 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -145,3 +145,30 @@ State: 5
 State: 6
 [t] 6
 --END--""")
+
+# Running delay_branching_here on state-based acceptance may require
+# the output to use transition-based acceptance.  (Issue #525.)
+a = spot.automaton("""
+HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" Acceptance: 1 Inf(0) --BODY--
+State: 0 [0] 1 [0] 2 State: 1 [1] 3 State: 2 {0} [!1] 3 State: 3 [t] 0
+--END--""")
+copy = spot.make_twa_graph(a, spot.twa_prop_set.all())
+if spot.delay_branching_here(a):
+    a.purge_unreachable_states()
+tc.assertTrue(spot.are_equivalent(a, copy))
+tc.assertEqual(a.to_str(), """HOA: v1
+States: 3
+Start: 0
+AP: 2 "b" "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[1] 1
+State: 1
+[0] 2
+[!0] 2 {0}
+State: 2
+[t] 0
+--END--""")