From 99bf152673592223114d308d426d86c248d274f3 Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber-Caissier <philipp@lrde.epita.fr>
Date: Wed, 29 Jun 2022 14:02:25 +0200
Subject: [PATCH] propagate_marks_here can break state-acc prop

* spot/twaalgos/degen.cc: Fix
* tests/python/pdegen.py: Test
---
 spot/twaalgos/degen.cc |  4 ++++
 tests/python/pdegen.py | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)

diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc
index 11092ddac..0c07ccfa8 100644
--- a/spot/twaalgos/degen.cc
+++ b/spot/twaalgos/degen.cc
@@ -1168,5 +1168,9 @@ namespace spot
         unsigned idx = aut->edge_number(e);
         e.acc = marks[idx];
       }
+    // If aut was state-based acc before, this might no longer
+    // this might no longer be the case
+    if (aut->prop_state_acc() == 1)
+      aut->prop_state_acc(0);
   }
 }
diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py
index 12bc9e39a..7df9f0878 100644
--- a/tests/python/pdegen.py
+++ b/tests/python/pdegen.py
@@ -442,3 +442,44 @@ si = spot.scc_info(aut15)
 aut15b = si.split_on_sets(2, [])[0]; d
 aut15c = spot.partial_degeneralize(aut15b)
 tc.assertTrue(aut15c.equivalent_to(aut15b))
+
+
+# Testing property propagation/update
+# for propagate_marks_here
+
+s = """HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[0] 1
+[!0] 2
+State: 1 {0}
+[0] 0
+State: 2
+[!0] 0
+--END--"""
+aut = spot.automaton(s)
+spot.propagate_marks_here(aut)
+s2 = aut.to_str("hoa")
+
+tc.assertEqual(s2, """HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0] 1 {0}
+[!0] 2
+State: 1
+[0] 0 {0}
+State: 2
+[!0] 0
+--END--""")
\ No newline at end of file