introduce a zielonka_tree class

* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: New files.
* spot/twaalgos/Makefile.am: Add them.
* tests/python/_zlktree.ipynb: New file.
* tests/Makefile.am: Add it.
* python/spot/__init__.py, python/spot/impl.i: Add bindings for it.
* doc/spot.bib (casares.21.icalp): New entry.
* NEWS: Mention this.

NEWS

@@ -231,6 +231,11 @@ New in spot 2.9.7.dev (not yet released)
     Additionally, this function now returns the number of states that
     have been merged (and therefore removed from the automaton).
 
+  - spot::zielonka_tree is a new class that can be constructed from
+    any acceptance condition to help paritizing it.  This is based on
+    a paper by Casares et al. (ICALP'21). Its python binding will
+    display the tree graphically.
+
   Python:
 
   - Bindings for functions related to games.

doc/spot.bib

@@ -1,4 +1,3 @@
-
 @InProceedings{	  babiak.12.tacas,
   author	= {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
 		  K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
@@ -114,6 +113,24 @@
   url		= {http://www.numdam.org/item/ITA_1999__33_6_495_0/}
 }
 
+@InProceedings{	  casares.21.icalp,
+  author	= {Antonio Casares and Thomas Colcombet and Nathana\"{e}l
+		  Fijalkow},
+  title		= {Optimal Transformations of Games and Automata Using
+		  {M}uller Conditions},
+  booktitle	= {Proceedings of the 48th International Colloquium on
+		  Automata, Languages, and Programming (ICALP'21)},
+  pages		= {123:1--123:14},
+  series	= {Leibniz International Proceedings in Informatics
+		  (LIPIcs)},
+  year		= {2021},
+  volume	= {198},
+  editor	= {Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
+  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address	= {Dagstuhl, Germany},
+  doi		= {10.4230/LIPIcs.ICALP.2021.123}
+}
+
 @InProceedings{	  cerna.03.mfcs,
   author	= {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
   title		= {Relating Hierarchy of Temporal Properties to Model
@@ -169,13 +186,13 @@
   doi		= {10.1109/TCAD.2008.2003303}
 }
 
-@article{   clemente.2.17.corr,
+@Article{	  clemente.2.17.corr,
-  author    = {Lorenzo Clemente and Richard Mayr},
+  author	= {Lorenzo Clemente and Richard Mayr},
-  title     = {Efficient reduction of nondeterministic automata with application
+  title		= {Efficient reduction of nondeterministic automata with
-               to language inclusion testing},
+		  application to language inclusion testing},
-  journal   = {CoRR},
+  journal	= {CoRR},
-  volume    = {abs/1711.09946},
+  volume	= {abs/1711.09946},
-  year      = {2017},
+  year		= {2017}
 }
 
 @Article{	  courcoubetis.92.fmsd,

python/spot/__init__.py

@@ -428,6 +428,15 @@ class atomic_prop_set:
         return res
 
 
+@_extend(zielonka_tree)
+class zielonka_tree:
+    def _repr_svg_(self):
+        """Output the Zielonka tree as SVG"""
+        ostr = ostringstream()
+        self.dot(ostr)
+        return _ostream_to_svg(ostr)
+
+
 def automata(*sources, timeout=None, ignore_abort=True,
              trust_hoa=True, no_sid=False, debug=False,
              want_kripke=False):

python/spot/impl.i

@@ -164,6 +164,7 @@
 #include <spot/twaalgos/word.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
 #include <spot/twaalgos/toparity.hh>
+#include <spot/twaalgos/zlktree.hh>
 
 #include <spot/parseaut/public.hh>
 
@@ -690,6 +691,7 @@ def state_is_accepting(self, src) -> "bool":
 %template(list_bdd) std::list<bdd>;
 %include <spot/twaalgos/are_isomorphic.hh>
 %include <spot/twaalgos/toparity.hh>
+%include <spot/twaalgos/zlktree.hh>
 
 %pythonprepend spot::twa::dtwa_complement %{
   from warnings import warn

spot/twaalgos/Makefile.am

@@ -98,7 +98,8 @@ twaalgos_HEADERS = \
   totgba.hh \
   toweak.hh \
   translate.hh \
-  word.hh
+  word.hh \
+  zlktree.hh
 
 noinst_LTLIBRARIES = libtwaalgos.la
 libtwaalgos_la_SOURCES = \
@@ -170,6 +171,7 @@ libtwaalgos_la_SOURCES = \
   totgba.cc \
   toweak.cc \
   translate.cc \
-  word.cc
+  word.cc \
+  zlktree.cc
 
 libtwaalgos_la_LIBADD = gtec/libgtec.la

spot/twaalgos/zlktree.cc

@@ -0,0 +1,228 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Developpement 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/>.
+
+#include "config.h"
+#include <iostream>
+#include <spot/twaalgos/zlktree.hh>
+#include "spot/priv/bddalloc.hh"
+
+namespace spot
+{
+  zielonka_tree::zielonka_tree(acc_cond& cond)
+  {
+    acc_cond::acc_code& code = cond.get_acceptance();
+    auto used = code.used_sets();
+    unsigned c = used.count();
+    unsigned max = used.max_set();
+
+    bdd_allocator ba;
+    int base = ba.allocate_variables(c);
+    assert(base == 0);
+    std::vector<bdd> col_to_bdd(max ? max : 1, bddfalse);
+    std::vector<unsigned> bdd_to_col(c);
+    bdd all_neg = bddtrue;
+    for (unsigned i = 0; i < max; ++i)
+      if (used.has(i))
+        {
+          bdd_to_col[base] = i;
+          all_neg &= bdd_nithvar(base);
+          col_to_bdd[i] = bdd_ithvar(base++);
+        }
+
+    bdd poscond = code.to_bdd(col_to_bdd.data());
+    bdd negcond = !poscond;
+
+    nodes_.emplace_back();
+    nodes_[0].parent = 0;
+    nodes_[0].colors = used;
+    nodes_[0].level = 0;
+
+    // Or goal is the find the list of maximal models for a formula named
+    // cond and defined later for each node.
+    //
+    // For instance if cond is satisfied by {1}, {3}, {1,2}, {1,2,3},
+    // {0,3}, and {0,1,3}, then the maximal models are {1,2,3} and
+    // {0,1,3}.
+    //
+    // To do that we build a list of models ordered by decreasing
+    // size.  When inserting a model, we will compare it to all
+    // model of larger size first, and abort the insertion if
+    // needed.  Otherwise we insert it, and then compare it to
+    // smaller models to possibly remove them.
+    //
+    // "models" is the variable where we store those ordered models.
+    // This list is local to each node, but we reuse the vector
+    // between each iteration to avoid unnecessary allocations.
+    struct size_model
+    {
+      unsigned size;
+      acc_cond::mark_t model;
+    };
+    std::vector<size_model> models;
+
+    // This loop is a BFS over the increasing set of nodes.
+    for (unsigned node = 0; node < nodes_.size(); ++node)
+    {
+      acc_cond::mark_t colors = nodes_[node].colors;
+      bool is_accepting = code.accepting(colors);
+      if (node == 0)
+        is_even_ = is_accepting;
+
+      // colors that do not appear in this node should
+      // be set to false in the acceptance.
+      bdd to_remove = bddtrue;
+      for (unsigned c: (colors ^ used).sets())
+        to_remove &= !col_to_bdd[c];
+      bdd cond = bdd_restrict(is_accepting ? negcond : poscond, to_remove);
+
+      // These is where we will store the ordered list of models, as
+      // explained in the declation of that vector.
+      models.clear();
+
+      while (cond != bddfalse)
+        {
+          // Find one model of cond.  If it has some don't cares
+          // variable, we interpret them as true, so in effect, we can
+          // start from a model where all colors are sets, and only
+          // unset those that are negative in the output of
+          // bdd_satone.
+          bdd one = bdd_satone(cond);
+          cond -= one;
+          acc_cond::mark_t curmodel = colors;
+          while (one != bddtrue)
+            {
+              unsigned v = bdd_to_col[bdd_var(one)];
+              if (bdd_high(one) == bddfalse)
+                {
+                  curmodel.clear(v);
+                  one = bdd_low(one);
+                }
+              else
+                {
+                  one = bdd_high(one);
+                }
+            }
+          //
+          unsigned sz = curmodel.count();
+          if (sz == 0)
+            // ignore the empty set
+            continue;
+          auto iter = models.begin();
+          while (iter != models.end())
+            {
+              if (iter->size < sz)
+                // We have checked all larger models.
+                break;
+              if (curmodel.subset(iter->model))
+                // curmodel is covered by iter->model.
+                goto donotinsert;
+              ++iter;
+            }
+          // insert the model
+          iter = models.insert(iter, {sz, curmodel});
+          ++iter;
+          // erase all models it contains
+          models.erase(std::remove_if(iter, models.end(),
+                                      [&](auto& mod) {
+                                        return mod.model.subset(curmodel);
+                                      }), models.end());
+        donotinsert:;
+        }
+      if (models.empty()) // This is a leaf of the tree.
+        {
+          if (num_branches_++ == 0)
+            one_branch_ = node;
+          continue;
+        }
+      unsigned first = nodes_.size();
+      nodes_[node].first_child = first;
+      unsigned num_children = models.size();
+      nodes_.reserve(first + num_children);
+      for (auto& m: models)
+        nodes_.push_back({node, static_cast<unsigned>(nodes_.size() + 1),
+                          0, nodes_[node].level + 1, m.model});
+      nodes_.back().next_sibling = first;
+
+      if (num_children > 1)
+        {
+          if (is_accepting)
+            has_rabin_shape_ = false;
+          else
+            has_streett_shape_ = false;
+        }
+    };
+  }
+
+  void zielonka_tree::dot(std::ostream& os) const
+  {
+    os << "digraph zielonka_tree {\n";
+    unsigned ns = nodes_.size();
+    for (unsigned n = 0; n < ns; ++n)
+      {
+        os << "  " << n << " [label=\"" << nodes_[n].colors;
+        unsigned first_child = nodes_[n].first_child;
+        if (!first_child)
+            os << "\n<" << n << '>';
+        os << "\", shape="
+           << (((nodes_[n].level & 1) ^ is_even_) ? "ellipse" : "box")
+           << "]\n";
+        if (first_child)
+          {
+            unsigned child = first_child;
+            do
+              {
+                os << "  " << n << " -> " << child << '\n';
+                child = nodes_[child].next_sibling;
+              }
+            while (child != first_child);
+          }
+      }
+    os << "}\n";
+  }
+
+  std::pair<unsigned, unsigned>
+  zielonka_tree::step(unsigned branch, acc_cond::mark_t colors) const
+  {
+    if (SPOT_UNLIKELY(nodes_.size() < branch || nodes_[branch].first_child))
+      throw std::runtime_error
+        ("zielonka_tree::next_branch(): incorrect branch number");
+
+    if (!colors)
+      return {branch, nodes_[branch].level + 1};
+
+    unsigned child = 0;
+    for (;;)
+      {
+        colors -= nodes_[branch].colors;
+        if (!colors)
+          break;
+        child = branch;
+        branch = nodes_[branch].parent;
+      }
+    unsigned lvl = nodes_[branch].level;
+    if (child != 0)
+      {
+        // The following computation could be precomputed.
+        branch = nodes_[child].next_sibling;
+        while (nodes_[branch].first_child)
+          branch = nodes_[branch].first_child;
+      }
+    return {branch, lvl};
+  }
+}

spot/twaalgos/zlktree.hh

@@ -0,0 +1,132 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Developpement 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/>.
+
+#pragma once
+
+#include <iosfwd>
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  /// \ingroup twa_acc_transform
+  /// \brief Zielonka Tree implementation
+  ///
+  /// This class implements a Zielonka Tree, using
+  /// conventions similar to those in \cite casares.21.icalp
+  ///
+  /// The differences is that this tree is built from Emerson-Lei
+  /// acceptance conditions, and can be "walked through" with multiple
+  /// colors at once.
+  class SPOT_API zielonka_tree
+  {
+  public:
+    /// \brief Build a Zielonka tree from the acceptance condition.
+    zielonka_tree(acc_cond& cond);
+
+    /// \brief The number of branches in the Zielonka tree.
+    ///
+    /// Branch are designated by the node number of their
+    /// leaves.
+    unsigned num_branches() const
+    {
+      return num_branches_;
+    }
+
+    /// \brief The number of one branch in the tree.
+    ///
+    /// This returns the branch whose leave is the smallest one.
+    unsigned first_branch() const
+    {
+      return one_branch_;
+    }
+
+    /// \brief Walk through the Zielonka tree.
+    ///
+    /// Given a \a branch number, and a set of \a colors, this returns
+    /// a pair (new branch, level), as needed in definition 3.7 of
+    /// \cite casares.21.icalp
+    ///
+    /// The level correspond to the priority of a minimum parity acceptance
+    /// condition, with the parity odd/even as specified by is_even().
+    ///
+    /// This implementation is slightly different from the original
+    /// definition since it allows a set of colors to be processed,
+    /// and not exactly one color.  When multiple colors are given,
+    /// the minimum corresponding level is returned.  When no color is
+    /// given, the branch is not changed and the level returned is one
+    /// more than the depth of that branch (this is as if the tree add
+    /// another layer of leaves labeled by the empty sets, that do not
+    /// store for simplicity).
+    std::pair<unsigned, unsigned>
+    step(unsigned branch, acc_cond::mark_t colors) const;
+
+    /// \brief Whether the tree corresponds to a min even or min odd
+    /// parity acceptance.
+    bool is_even() const
+    {
+      return is_even_;
+    }
+
+    /// \brief Whether the Zielonka tree has Rabin shape.
+    ///
+    /// The tree has Rabin shape of all accepting (round) nodes have
+    /// at most one child.
+    bool has_rabin_shape() const
+    {
+      return has_rabin_shape_;
+    }
+
+    /// \brief Whether the Zielonka tree has Streett shape.
+    ///
+    /// The tree has Streett shape of all rejecting (square) nodes have
+    /// at most one child.
+    bool has_streett_shape() const
+    {
+      return has_streett_shape_;
+    }
+
+    /// \brief Whether the Zielonka tree has parity shape.
+    ///
+    /// The tree has parity shape of all nodes have at most one child.
+    bool has_parity_shape() const
+    {
+      return has_streett_shape_ && has_rabin_shape_;
+    }
+
+    /// \brief Render the tree as in GraphViz format.
+    void dot(std::ostream&) const;
+
+  private:
+    struct zielonka_node
+    {
+      unsigned parent;
+      unsigned next_sibling = 0;
+      unsigned first_child = 0;
+      unsigned level;
+      acc_cond::mark_t colors;
+    };
+    std::vector<zielonka_node> nodes_;
+    unsigned one_branch_ = 0;
+    unsigned num_branches_ = 0;
+    bool is_even_;
+    bool has_rabin_shape_ = true;
+    bool has_streett_shape_ = true;
+  };
+
+}

tests/Makefile.am

@@ -449,6 +449,7 @@ TESTS_python = \
   python/twagraph.py \
   python/toweak.py \
   python/_word.ipynb \
+  python/_zlktree.ipynb \
   $(TESTS_ipython)
 endif