acd: add support for state-based output

* spot/twaalgos/zlktree.hh, spot/twaalgos/zlktree.cc (acd::node_level,
acd::state_step, acd_transform_sbacc): New public functions.
* tests/python/zlktree.ipynb, tests/python/zlktree.py: More tests.
* NEWS: Typo.

NEWS

@@ -15,19 +15,19 @@ New in spot 2.9.8.dev (not yet released)
 
   - ltlsynt --aiger option now takes an optional argument indicating
     how the bdd and states are to be encoded in the aiger output.
-    The option has to be given in the form 
+    The option has to be given in the form
-    ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first 
+    ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first
     only obligatory argument decides whether "if-then-else" ("ite")
     or irreducible-sum-of-products ("isop") is to be used.
     "both" executes both strategies and retains the smaller circuits.
-    The additional options are for fine-tuning. "ud" also encodes the 
+    The additional options are for fine-tuning. "ud" also encodes the
     dual of the conditions and retains the smaller circuits.
     "dc" computes if for some inputs we do not care whether the
     output is high or low and try to use this information to compute
     a smaller circuit. "subX" indicates different strategies to find
     common subexpressions, with "sub0" indicating no extra computations.
 
-  - ltlsynt --verify checks the computed strategy or aiger circuit 
+  - ltlsynt --verify checks the computed strategy or aiger circuit
     against the specification.
 
   - ltlsynt -x "specification-decomposition" determines whether or not
@@ -36,8 +36,8 @@ New in spot 2.9.8.dev (not yet released)
     into a circuit.
 
   - ltlsynt -x "minimization-level=[0-5]" determines how to minimize
-    the strategy (a monitor). 0, no minimization; 1, regular DFA 
+    the strategy (a monitor). 0, no minimization; 1, regular DFA
-    minimization; 2, signature based minimization with 
+    minimization; 2, signature based minimization with
     output assignement; 3, SAT based minimization; 4, 1 then 3;
     5, 2 then 3.
 
@@ -58,11 +58,11 @@ New in spot 2.9.8.dev (not yet released)
 
   Library:
   - Spot now provides convenient function to create and solve game.
-    The functions are located in twaalgos/game.hh and 
+    The functions are located in twaalgos/game.hh and
-    twaalgos/synthesis.hh. Moreover a new structure holding 
+    twaalgos/synthesis.hh. Moreover a new structure holding
     all the necessary options called game_info is now available.
 
-  - A new class called aig is introduced to represent 
+  - A new class called aig is introduced to represent
     and-inverter-graphs, which is useful for synthesis.
 
   - Historically, Spot labels automata by Boolean formulas over
@@ -275,7 +275,7 @@ New in spot 2.9.8.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 and spot::acd are new class that implement the
+  - spot::zielonka_tree and spot::acd are new classes that implement the
     Zielonka Tree and Alternatic Cycle Decomposition, based on a paper
     by Casares et al. (ICALP'21).  Those structures can be used to
     paritize any automaton, and more.  The graphical rendering of ACD

spot/twaalgos/zlktree.cc

@@ -646,25 +646,69 @@ namespace spot
         branch = parent;
       }
     unsigned lvl = nodes_[branch].level;
-    if (child != 0)
+    if (child == 0)             // came here without climbing up
+      return { leftmost_branch_(branch, dst), lvl };
+
+    unsigned start_child = child;
+    // find the next children that contains dst.
+    do
       {
-        unsigned start_child = child;
+        child = nodes_[child].next_sibling;
-        // find the next children that contains dst.
+        if (nodes_[child].states.get(dst))
-        do
+          return {leftmost_branch_(child, dst), lvl};
-          {
-            child = nodes_[child].next_sibling;
-            if (nodes_[child].states.get(dst))
-              return {leftmost_branch_(child, dst), lvl};
-          }
-        while (child != start_child);
-        return { branch, lvl };
-      }
-    else
-      {
-        return { leftmost_branch_(branch, dst), lvl };
       }
+    while (child != start_child);
+    return { branch, lvl };
   }
 
+  unsigned acd::state_step(unsigned node, unsigned edge) const
+  {
+    // The rule is almost similar to step(), except we do note
+    // go down to the leftmost leave after we have seen a round
+    // of all children.
+    if (SPOT_UNLIKELY(nodes_.size() <= node))
+      throw std::runtime_error("acd::step(): incorrect node number");
+    if (SPOT_UNLIKELY(nodes_[node].edges.size() < edge))
+      throw std::runtime_error("acd::step(): incorrect edge number");
+
+    unsigned child = 0;
+    auto& es = aut_->edge_storage(edge);
+    unsigned dst = es.dst;
+    unsigned src = es.src;
+    // If we are not on a leaf of the subtree of src, go there before
+    // continuing.
+    node = leftmost_branch_(node, src);
+    while (!nodes_[node].edges.get(edge))
+      {
+        unsigned parent = nodes_[node].parent;
+        if (SPOT_UNLIKELY(node == parent))
+          {
+            // Changing SCc
+            return first_branch(dst);
+          }
+        child = node;
+        node = parent;
+      }
+    if (child == 0)             // came here without climbing up
+      return leftmost_branch_(node, dst);
+    unsigned start_child = child;
+    // find the next children that contains dst.
+    do
+      {
+        child = nodes_[child].next_sibling;
+        if (nodes_[child].states.get(dst))
+          {
+            if (child <= start_child)
+              return node; // full loop of children done
+            else
+              return child;
+          }
+      }
+    while (child != start_child);
+    return node;
+  }
+
+
   void acd::dot(std::ostream& os, const char* id) const
   {
     unsigned ns = nodes_.size();
@@ -786,6 +830,14 @@ namespace spot
     return (nodes_[n].level & 1) ^ is_even_;
   }
 
+  /// Return the level of a node.
+  unsigned acd::node_level(unsigned n)
+  {
+    if (SPOT_UNLIKELY(nodes_.size() <= n))
+      throw std::runtime_error("acd::node_level(): unknown node");
+    return nodes_[n].level;
+  }
+
   std::vector<unsigned> acd::edges_of_node(unsigned n) const
   {
     if (SPOT_UNLIKELY(nodes_.size() <= n))
@@ -821,8 +873,11 @@ namespace spot
     return has_streett_shape_ && has_rabin_shape_;
   }
 
+  // This handle both the transition-based and state-based version of
+  // ACD, to
+  template<bool sbacc>
   twa_graph_ptr
-  acd_transform(const const_twa_graph_ptr& a, bool colored)
+  acd_transform_(const const_twa_graph_ptr& a, bool colored)
   {
     auto res = make_twa_graph(a->get_dict());
     res->copy_ap_of(a);
@@ -844,6 +899,8 @@ namespace spot
     // state-based acceptance is lost,
     // inherently-weak automata become weak.
     res->prop_copy(a, { false, false, true, true, true, true });
+    if constexpr (sbacc)
+      res->prop_state_acc(true);
 
     auto orig_states = new std::vector<unsigned>();
     auto branches = new std::vector<unsigned>();
@@ -889,24 +946,42 @@ namespace spot
         unsigned src_scc = si.scc_of(s.first);
         unsigned scc_max_lvl = theacd.scc_max_level(src_scc);
         bool scc_max_lvl_can_be_omitted = (scc_max_lvl & 1) == max_level_is_odd;
+        unsigned src_prio;
+        if constexpr (!sbacc)
+          {
+            (void)src_prio; // this is only used for sbacc
+          }
+        else
+          {
+            src_prio = si.is_trivial(src_scc) ?
+              scc_max_lvl : theacd.node_level(branch);
+            if (!scc_max_lvl_can_be_omitted || src_prio != scc_max_lvl)
+              max_color = std::max(max_color, src_prio);
+          }
         for (auto& i: a->out(s.first))
           {
             unsigned newbranch;
             unsigned prio;
+            if constexpr (sbacc) // All successor have the same colors.
+              prio = src_prio;
             unsigned dst_scc = si.scc_of(i.dst);
             if (dst_scc != src_scc)
               {
                 newbranch = theacd.first_branch(i.dst);
-                prio = 0;
+                if constexpr (!sbacc)
+                  prio = 0;
               }
             else
               {
-                std::tie(newbranch, prio) =
+                if constexpr (!sbacc)
-                  theacd.step(branch, a->edge_number(i));
+                  std::tie(newbranch, prio) =
+                    theacd.step(branch, a->edge_number(i));
+                else
+                  newbranch = theacd.state_step(branch, a->edge_number(i));
               }
             zlk_state d(i.dst, newbranch);
             unsigned dst = new_state(d);
-            if (!colored && ((dst_scc != src_scc)
+            if (!colored && ((!sbacc && dst_scc != src_scc)
                              || (scc_max_lvl_can_be_omitted
                                  && scc_max_lvl == prio)))
               {
@@ -914,7 +989,8 @@ namespace spot
               }
             else
               {
-                max_color = std::max(max_color, prio);
+                if (!sbacc)
+                  max_color = std::max(max_color, prio);
                 res->new_edge(src, dst, i.cond, {prio});
               }
           }
@@ -939,4 +1015,16 @@ namespace spot
     return res;
   }
 
+  twa_graph_ptr
+  acd_transform(const const_twa_graph_ptr& a, bool colored)
+  {
+    return acd_transform_<false>(a, colored);
+  }
+
+  twa_graph_ptr
+  acd_transform_sbacc(const const_twa_graph_ptr& a, bool colored)
+  {
+    return acd_transform_<true>(a, colored);
+  }
+
 }

spot/twaalgos/zlktree.hh

@@ -222,6 +222,13 @@ namespace spot
     std::pair<unsigned, unsigned>
     step(unsigned branch, unsigned edge) const;
 
+    /// \brief Step through the ACD, with rules for state-based output.
+    ///
+    /// Given a \a node number, and an edge, this returns
+    /// the new node to associate to the destination state.  This
+    /// node is not necessarily a leave, and its level should be
+    /// the level for the output state.
+    unsigned state_step(unsigned node, unsigned edge) const;
 
     /// \brief Return the list of edges covered by node n of the ACD.
     ///
@@ -239,6 +246,9 @@ namespace spot
     /// This is mostly used for interactive display.
     bool node_acceptance(unsigned n) const;
 
+    /// Return the level of a node.
+    unsigned node_level(unsigned n);
+
     /// \brief Whether the ACD corresponds to a min even or min odd
     /// parity acceptance in SCC \a scc.
     bool is_even(unsigned scc) const
@@ -392,7 +402,18 @@ namespace spot
   /// if the input has n colors. If \colored is unsed (the default),
   /// output transitions will use at most one color, and output
   /// automaton will use at most n colors.
+  ///
+  /// The acd_tranform() is the original function producing
+  /// optimal transition-based output (optimal in the sense of least
+  /// number of duplicated states), while the acd_tansform_sbacc() variant
+  /// produces state-based output from transition-based input and without
+  /// any optimality claim.
+  /// @{
   SPOT_API
   twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
                               bool colored = false);
+  SPOT_API
+  twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut,
+                                    bool colored = false);
+  /// @}
 }

tests/python/zlktree.py

@@ -117,3 +117,10 @@ except RuntimeError as e:
     assert 'unknown node' in str(e)
 else:
     report_missing_exception()
+
+try:
+    aa.node_level(0)
+except RuntimeError as e:
+    assert 'unknown node' in str(e)
+else:
+    report_missing_exception()