From 9b3956f892a800853251ddae9633f595e1baf4ea Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 7 Oct 2021 11:11:49 +0200
Subject: [PATCH] zlktree: fix handling of automata with false acceptance

Reported by Florian.

* spot/twaalgos/zlktree.cc (zielonka_tree_transform, acd_transform):
Here.
* tests/python/zlktree.py: Add test cases.
---
 spot/twaalgos/zlktree.cc | 16 ++++++++--------
 tests/python/zlktree.py  | 10 ++++++++++
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc
index 668363ec5..babfafdf3 100644
--- a/spot/twaalgos/zlktree.cc
+++ b/spot/twaalgos/zlktree.cc
@@ -242,7 +242,9 @@ namespace spot
   {
     auto res = make_twa_graph(a->get_dict());
     res->copy_ap_of(a);
-    zielonka_tree zlk(a->get_acceptance());
+    auto& acc = a->get_acceptance();
+    zielonka_tree zlk(acc);
+    acc_cond::mark_t mask = acc.used_sets();
 
     // Preserve determinism, weakness, and stutter-invariance
     res->prop_copy(a, { false, true, true, true, true, true });
@@ -289,7 +291,7 @@ namespace spot
 
         for (auto& i: a->out(s.first))
           {
-            auto [newbranch, prio] = zlk.step(branch, i.acc);
+            auto [newbranch, prio] = zlk.step(branch, i.acc & mask);
             zlk_state d(i.dst, newbranch);
             unsigned dst = new_state(d);
             max_color = std::max(max_color, prio);
@@ -1146,12 +1148,10 @@ namespace spot
           }
       }
 
-    if (!colored && max_level == 0)
-      res->set_acceptance(0, acc_cond::acc_code::t());
-    else
-      res->set_acceptance(max_color + 1,
-                          acc_cond::acc_code::parity_min(!is_even,
-                                                         max_color + 1));
+    bool extra = colored || max_level > 0;
+    res->set_acceptance(max_color + extra,
+                        acc_cond::acc_code::parity_min(!is_even,
+                                                       max_color + extra));
 
     // compose original-states with the any previously existing one.
     if (auto old_orig_states =
diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py
index 89571e520..224c7de88 100644
--- a/tests/python/zlktree.py
+++ b/tests/python/zlktree.py
@@ -124,3 +124,13 @@ except RuntimeError as e:
     assert 'unknown node' in str(e)
 else:
     report_missing_exception()
+
+a = spot.translate('true')
+a.set_acceptance(spot.acc_cond('f'))
+b = spot.acd_transform(a)
+assert a.equivalent_to(b)
+
+a = spot.translate('true')
+a.set_acceptance(spot.acc_cond('f'))
+b = spot.zielonka_tree_transform(a)
+assert a.equivalent_to(b)