From 4ed5160fb8293af2da71f7702836db9f3c83363f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 8 Sep 2021 15:15:08 +0200
Subject: [PATCH] zlktree: fix a bug

Reported by Florian.

* spot/twaalgos/zlktree.cc: Handle the case where the condition does
not cover all colors.
* tests/python/zlktree.py: New file.
* tests/Makefile.am: Add it.
---
 spot/twaalgos/zlktree.cc |  4 ++--
 tests/Makefile.am        |  1 +
 tests/python/zlktree.py  | 29 +++++++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 tests/python/zlktree.py

diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc
index c31ec1509..44f6876aa 100644
--- a/spot/twaalgos/zlktree.cc
+++ b/spot/twaalgos/zlktree.cc
@@ -97,12 +97,12 @@ namespace spot
   zielonka_tree::zielonka_tree(const acc_cond& cond)
   {
     const acc_cond::acc_code& code = cond.get_acceptance();
-    auto used = code.used_sets();
+    auto all = cond.all_sets();
     acc_cond negcond(cond.num_sets(), cond.get_acceptance().complement());
 
     nodes_.emplace_back();
     nodes_[0].parent = 0;
-    nodes_[0].colors = used;
+    nodes_[0].colors = all;
     nodes_[0].level = 0;
 
     std::vector<size_model> models;
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 309ff8105..b7ec460aa 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -450,6 +450,7 @@ TESTS_python = \
   python/twagraph.py \
   python/toweak.py \
   python/_word.ipynb \
+  python/zlktree.py \
   $(TESTS_ipython)
 endif
 
diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py
new file mode 100644
index 000000000..92df881fb
--- /dev/null
+++ b/tests/python/zlktree.py
@@ -0,0 +1,29 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# 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
+
+a = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1"
+Acceptance: 4 Inf(3) | Fin(3) properties: trans-labels explicit-labels
+trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3}
+[0&!1] 0 {2} [!0&1] 1 {2} State: 2 [!0&1] 0 {0 2} [!0&!1] 1 State: 3
+[!0&1] 2 State: 4 [0&!1] 3 --END--""")
+b = spot.zielonka_tree_transform(a)
+assert spot.are_equivalent(a, b)
+assert b.acc().is_buchi()