From 27b8e5aa73def0d2b58137952538e5773dc293e0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 6 Feb 2024 14:09:42 +0100
Subject: [PATCH] postproc: fix default for acd and interaction with colored

* spot/twaalgos/postproc.hh (postprocess::acd_): Default to true.
* spot/twaalgos/postproc.cc (postprocess::run): When acd is used
to color an automaton, do not run scc_filter to remove color
from transiant edges.
* tests/python/acd.py: New file.
* tests/Makefile.am: Add it.
---
 NEWS                      | 12 +++++++
 spot/twaalgos/postproc.cc | 22 +++---------
 spot/twaalgos/postproc.hh |  2 +-
 tests/Makefile.am         |  1 +
 tests/python/acd.py       | 71 +++++++++++++++++++++++++++++++++++++++
 5 files changed, 90 insertions(+), 18 deletions(-)
 create mode 100644 tests/python/acd.py

diff --git a/NEWS b/NEWS
index 7a15bd1ac..5246909ea 100644
--- a/NEWS
+++ b/NEWS
@@ -207,6 +207,18 @@ New in spot 2.11.6.dev  (not yet released)
   - spot::minimize_obligation will skip attempts to complement very
     weak automata when those would require too many acceptance sets.
 
+  - acd_transform() was not used by spot::postprocessor unless an
+    option_map was passed.  This was due to some bad default for the
+    "acd" option: it defaulted to true when an option_map was given,
+    and to false otherwise.  This had no consequences on
+    ltl2tgba/autfilt were some option_map is always passed, but for
+    instance the parity automata generated by spot.postprocessor in
+    Python were not using ACD by default.
+
+  - Using spot::postprocessor to produce colored parity automata could
+    fail to color some transiant edges when the "acd" option was
+    activated.
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index 1a1ceb9cc..0a5979064 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -407,7 +407,7 @@ namespace spot
       // ignored.
       a = scc_filter_states(a);
     else
-      a = do_scc_filter(a, (PREF_ == Any));
+      a = do_scc_filter(a, (PREF_ == Any) && !COLORED_);
 
     if (type_ == Monitor)
       {
@@ -721,23 +721,11 @@ namespace spot
           sim = nullptr;
       }
 
-    if (level_ == High && scc_filter_ != 0)
-      {
-        if (dba)
-          {
-            // Do that even for WDBA, to remove marks from transitions
-            // leaving trivial SCCs.
-            dba = do_scc_filter(dba, true);
-            assert(!sim);
-          }
-        else if (sim)
-          {
-            sim = do_scc_filter(sim, true);
-            assert(!dba);
-          }
-      }
-
     sim = dba ? dba : sim;
+    if (level_ == High && scc_filter_ != 0 && !(acd_was_used_ && COLORED_))
+      // Do that even for WDBA, to remove marks from transitions
+      // leaving trivial SCCs.
+      sim = do_scc_filter(sim, true);
 
     if (type_ == CoBuchi)
       {
diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh
index 2a162501d..73da4baab 100644
--- a/spot/twaalgos/postproc.hh
+++ b/spot/twaalgos/postproc.hh
@@ -269,7 +269,7 @@ namespace spot
     int simul_max_ = 4096;
     int merge_states_min_ = 128;
     int wdba_det_max_ = 4096;
-    bool acd_ = false;
+    bool acd_ = true;
     bool acd_was_used_;
   };
   /// @}
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 3609ec03b..67e5bb4d6 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -395,6 +395,7 @@ TESTS_python = \
   python/_autparserr.ipynb \
   python/_aux.ipynb \
   python/acc.py \
+  python/acd.py \
   python/accparse2.py \
   python/alarm.py \
   python/aliases.py \
diff --git a/tests/python/acd.py b/tests/python/acd.py
new file mode 100644
index 000000000..6e393a781
--- /dev/null
+++ b/tests/python/acd.py
@@ -0,0 +1,71 @@
+#!/usr/bin/python3
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) by the Spot authors, see the AUTHORS file for details.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+import spot
+from unittest import TestCase
+tc = TestCase()
+
+
+a = spot.automaton("""
+HOA: v1
+States: 3
+Start: 0
+AP: 3 "p0" "p1" "p2"
+Acceptance: 3 Fin(0) & Inf(1) & Fin(2)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[!0] 1
+[0&!1&2] 0
+[0&!1&!2] 0 {2}
+[0&1&2] 0 {1}
+[0&1&!2] 0 {1 2}
+State: 1
+[!1&2] 2
+[!1&!2] 2 {2}
+[1&2] 2 {1}
+[1&!2] 2 {1 2}
+State: 2
+[0&!1&2] 2
+[0&!1&!2] 2 {2}
+[0&1&2] 2 {1}
+[0&1&!2] 2 {1 2}
+--END--""")
+res = a.postprocess("small", "high", "parity min odd", "colored")
+tc.assertEqual(res.to_str(), """HOA: v1
+States: 3
+Start: 0
+AP: 3 "p0" "p1" "p2"
+acc-name: parity min odd 3
+Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
+properties: trans-labels explicit-labels trans-acc colored
+properties: deterministic
+--BODY--
+State: 0
+[0&!2] 0 {0}
+[0&1&2] 0 {1}
+[0&!1&2] 0 {2}
+[!0] 1 {0}
+State: 1
+[t] 2 {0}
+State: 2
+[0&!2] 2 {0}
+[0&1&2] 2 {1}
+[0&!1&2] 2 {2}
+--END--""")