improve partial_degeneralize() on several cases

On these 4 cases, added to pdegen.py, and supplied by Florian Renkin,
partial_degeneralize() is now at least as good as degeneralize_tba(),
and sometimes better.  This is achieved as follows: (1) a
propagate_marks procedure is introduced to propagate marks as far as
possible on the automaton (e.g., common outgoing marks can be push
onto the incoming transitions and vice-versa), (2) the
degeneralization order is compute dynamically, and (3) whenever and
fully-accepting transition is taken in the original automaton, the
destination level is chosen to be the highest existing level.

* spot/twaalgos/degen.cc,
spot/twaalgos/degen.hh (propagate_marks_vector, propagate_marks_here):
New functions.
(partial_degeneralize): Improve, as described above.
* tests/python/pdegen.py: Add test cases.

NEWS

@@ -58,7 +58,7 @@ New in spot 2.8.5.dev (not yet released)
        parity_min_even(n) = parity_min(false, n)
 
   - partial_degeneralize() is a new function performing partial
-    degeneralization to get rid of conjunction of Inf terms in
+    degeneralization to get rid of conjunctions of Inf terms in
     acceptance conditions.
 
   - simplify_acceptance_here() and simplify_acceptance() learned to
@@ -68,6 +68,16 @@ New in spot 2.8.5.dev (not yet released)
     and the automaton is adjusted to that i also appears where j
     appeared.
 
+  - propagate_marks_vector() and propagate_marks_here() are helper
+    functions for propagatings marks on the automaton: ignoring
+    self-loop and out-of-SCC transitions, marks common to all the
+    input transitions of a state can be pushed to all outgoing
+    transitions of a state, and vice-versa.  This is repeated until a
+    fix point is reached.  propagate_marks_vector() does not modify
+    the automaton and returns a vector of the acc_cond::mark_t that
+    should be on each transition; propagate_marks_here() actually
+    modifies the automaton.
+
 New in spot 2.8.5 (2020-01-04)
 
   Bugs fixed:

spot/twaalgos/degen.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2019 Laboratoire de Recherche
+// Copyright (C) 2012-2020 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -122,7 +122,7 @@ namespace spot
         unsigned n = a->num_states();
         acc_cond::mark_t all = a_->acc().all_sets();
         // slot 2 will hold acceptance mark that are common to the
-        // incoming transitions of each state.  For know with all
+        // incoming transitions of each state.  For now with all
         // marks if there is some incoming edge.  The next loop will
         // constrain this value.
         for (auto& e: a_->edges())
@@ -176,36 +176,59 @@ namespace spot
     // Order of accepting sets (for one SCC)
     class acc_order final
     {
+      std::vector<std::pair<acc_cond::mark_t, unsigned>> found_;
       std::vector<unsigned> order_;
-      acc_cond::mark_t found_;
 
     public:
-      unsigned
+      acc_order(acc_cond::mark_t all)
-      next_level(int slevel, acc_cond::mark_t set, bool skip_levels)
       {
-        // Update the order with any new set we discover
+        unsigned count = all.count();
-        if (auto newsets = set - found_)
+        found_.emplace_back(all, count);
-          {
+        order_.insert(order_.begin(), count, 0);
-            newsets.fill(std::back_inserter(order_));
-            found_ |= newsets;
       }
 
-        unsigned next = slevel;
+      unsigned
-        while (next < order_.size() && set.has(order_[next]))
+      next_level(unsigned slevel, acc_cond::mark_t set)
       {
-            ++next;
+        unsigned last = order_.size();
-            if (!skip_levels)
+        if (last == 0)
-              break;
+          return slevel;
+        unsigned index = order_[slevel];
+
+        while (slevel < last
+               && (found_[index].first & set) == found_[index].first)
+          slevel += found_[index++].second;
+        if (slevel == last)
+          return slevel;
+        if (acc_cond::mark_t match = (found_[index].first & set))
+          {
+            unsigned matchsize = match.count();
+            found_[index].first -= match;
+            found_[index].second -= matchsize;
+            found_.emplace(found_.begin() + index, match, matchsize);
+            slevel += matchsize;
+            // update order_
+            unsigned opos = 0;
+            unsigned fpos = 0;
+            for (auto& p: found_)
+              {
+                for (unsigned n = 0; n < p.second; ++n)
+                  order_[opos++] = fpos;
+                ++fpos;
               }
-        return next;
+          }
+        return slevel;
       }
 
       void
       print(int scc)
       {
         std::cout << "Order_" << scc << ":\t";
+        for (auto i: found_)
+          std::cout << i.first << ' ';
+        std::cout << " // ";
         for (auto i: order_)
-          std::cout << i << ", ";
+          std::cout << i << ' ';
         std::cout << '\n';
       }
     };
@@ -213,27 +236,26 @@ namespace spot
     // Accepting order for each SCC
     class scc_orders final
     {
-      std::map<int, acc_order> orders_;
+      std::vector<acc_order> orders_;
-      bool skip_levels_;
 
     public:
-      scc_orders(bool skip_levels):
+      scc_orders(acc_cond::mark_t all, unsigned scc_count)
-        skip_levels_(skip_levels)
+        : orders_(scc_count, acc_order(all))
       {
       }
 
       unsigned
       next_level(int scc, int slevel, acc_cond::mark_t set)
       {
-        return orders_[scc].next_level(slevel, set, skip_levels_);
+        return orders_[scc].next_level(slevel, set);
       }
 
       void
       print()
       {
-        std::map<int, acc_order>::iterator i;
+        unsigned sz = orders_.size();
-        for (i = orders_.begin(); i != orders_.end(); i++)
+        for (unsigned i = 0; i < sz; ++i)
-          i->second.print(i->first);
+          orders_[i].print(i);
       }
     };
 
@@ -348,9 +370,6 @@ namespace spot
           order.emplace_back(i - 1);
       }
 
-      // Initialize scc_orders
-      scc_orders orders(skip_levels);
-
       // and vice-versa.
       ds2num_map ds2num;
 
@@ -370,6 +389,11 @@ namespace spot
         ? std::make_unique<scc_info>(a, scc_info_options::NONE)
         : nullptr;
 
+      // Initialize scc_orders
+      std::unique_ptr<scc_orders> orders = use_cust_acc_orders
+        ? std::make_unique<scc_orders>(a->acc().all_sets(), m->scc_count())
+        : nullptr;
+
       // Cache for common outgoing/incoming acceptances.
       inout_acc inout(a, m.get());
 
@@ -390,7 +414,7 @@ namespace spot
         {
           auto set = inout.common_inout_acc(s.first);
           if (SPOT_UNLIKELY(use_cust_acc_orders))
-            s.second = orders.next_level(m->initial(), s.second, set);
+            s.second = orders->next_level(m->initial(), s.second, set);
           else
             while (s.second < order.size() && set.has(order[s.second]))
               {
@@ -589,7 +613,7 @@ namespace spot
                       // for this scc
                       if (use_cust_acc_orders)
                         {
-                          d.second = orders.next_level(scc, next, acc);
+                          d.second = orders->next_level(scc, next, acc);
                         }
                       // Else compute level according the global acc order
                       else
@@ -628,7 +652,7 @@ namespace spot
 
               // In case we are building a TBA is_acc has to be
               // set differently for each edge, and
-              // we do not need to stay use final level.
+              // we do not need to stay on final level.
               if (!want_sba)
                 {
                   is_acc = d.second == order.size();
@@ -640,7 +664,7 @@ namespace spot
                         {
                           if (use_cust_acc_orders)
                             {
-                              d.second = orders.next_level(scc, d.second, acc);
+                              d.second = orders->next_level(scc, d.second, acc);
                             }
                           else
                             {
@@ -670,7 +694,7 @@ namespace spot
       for (auto i: order)
         std::cout << i << ", ";
       std::cout << '\n';
-      orders.print();
+      orders->print();
 #endif
       res->merge_edges();
       if (remove_extra_scc)
@@ -808,21 +832,40 @@ namespace spot
     update_acc_for_partial_degen(acc, todegen, tostrip, degenmark);
     res->set_acceptance(acc);
 
-    std::vector<unsigned> order;
-    for (unsigned set: todegen.sets())
-      order.push_back(set);
-
     // auto* names = new std::vector<std::string>;
     // res->set_named_prop("state-names", names);
     auto orig_states = new std::vector<unsigned>();
     auto levels = new std::vector<unsigned>();
-    orig_states->reserve(a->num_states()); // likely more are needed.
+    unsigned ns = a->num_states();
+    orig_states->reserve(ns); // likely more are needed.
     levels->reserve(a->num_states());
     res->set_named_prop("original-states", orig_states);
     res->set_named_prop("degen-levels", levels);
 
     scc_info si_orig(a, scc_info_options::NONE);
 
+    auto marks = propagate_marks_vector(a, &si_orig);
+
+    std::vector<unsigned> highest_level(ns, 0);
+    // Compute the marks that are common to all incoming or all
+    // outgoing transitions of each state, ignoring self-loops and
+    // out-of-SCC transitions.  Note that because
+    // propagate_marks_verctor() has been used, the intersection
+    // of all incoming marks is equal to the intersection of all
+    // outgoing marks unless the state has no predecessor or no
+    // successor.  We take the outgoing marks because states without
+    // successor are useless (but states without predecessors are not).
+    std::vector<acc_cond::mark_t> inout(ns, todegen);
+    for (auto& e: a->edges())
+      if (e.src != e.dst && si_orig.scc_of(e.src) == si_orig.scc_of(e.dst))
+        {
+          unsigned idx = a->edge_number(e);
+          inout[e.src] &= marks[idx];
+        }
+
+    scc_orders orders(todegen, si_orig.scc_count());
+    unsigned ordersize = todegen.count();
+
     // degen_states -> new state numbers
     ds2num_map ds2num;
 
@@ -834,6 +877,9 @@ namespace spot
                        if (di != ds2num.end())
                          return di->second;
 
+                       highest_level[ds.first] =
+                         std::max(highest_level[ds.first], ds.second);
+
                        unsigned ns = res->new_state();
                        ds2num[ds] = ns;
                        todo.emplace_back(ds);
@@ -846,13 +892,26 @@ namespace spot
                        levels->emplace_back(ds.second);
                        return ns;
                      };
-    degen_state s(a->get_init_state_number(), 0);
+
+    unsigned init = a->get_init_state_number();
+    degen_state s(init, 0);
+    // The initial level can be anything.  As a heuristic, pretend we
+    // have just seen the acceptance condition common to incoming
+    // edges.
+    s.second = orders.next_level(si_orig.scc_of(init), 0, inout[init]);
+    if (s.second == ordersize)
+      s.second = 0;
+
     new_state(s);
 
+    // A list of edges are that "all accepting" and whose destination
+    // could be redirected to a higher level.
+    std::vector<unsigned> allaccedges;
+
     while (!todo.empty())
       {
-        s = todo.front();
+        s = todo.back();
-        todo.pop_front();
+        todo.pop_back();
 
         int src = ds2num[s];
         unsigned slevel = s.second;
@@ -860,22 +919,39 @@ namespace spot
         unsigned scc_src = si_orig.scc_of(orig_src);
         for (auto& e: a->out(orig_src))
           {
+            bool saveedge = false;
             unsigned nextlvl = slevel;
             acc_cond::mark_t accepting = {};
             if (si_orig.scc_of(e.dst) == scc_src)
               {
-                while (nextlvl < order.size() && e.acc.has(order[nextlvl]))
+                unsigned idx = a->edge_number(e);
-                  ++nextlvl;
+                acc_cond::mark_t acc = marks[idx] & todegen;
-
+                nextlvl = orders.next_level(scc_src, nextlvl, acc);
-                if (nextlvl == order.size())
+                if (nextlvl == ordersize)
                   {
                     accepting = degenmark;
                     nextlvl = 0;
-
+                    if ((acc & todegen) != todegen)
-                    if ((e.acc & todegen) != todegen)
+                      {
-                      while (nextlvl < order.size()
+                        nextlvl = orders.next_level(scc_src, nextlvl, acc);
-                             && e.acc.has(order[nextlvl]))
+                      }
-                        ++nextlvl;
+                    else
+                      {
+                        // Because we have seen all sets on this
+                        // transition, we can jump to any level we
+                        // like.  As a heuristic, let's jump to the
+                        // highest existing level.
+                        nextlvl = highest_level[e.dst];
+                        if (nextlvl == 0 // probably a new state ->
+                                         // use inout for now
+                            && inout[e.dst] != todegen)
+                          nextlvl = orders.next_level(scc_src, nextlvl,
+                                                      inout[e.dst]);
+                        // It's possible that we have not yet seen the
+                        // highest level yet, so let's save this edge
+                        // and revisit this issue at the end.
+                        saveedge = true;
+                      }
                   }
                 accepting |= e.acc.strip(tostrip);
               }
@@ -886,13 +962,87 @@ namespace spot
 
             degen_state ds_dst(e.dst, nextlvl);
             unsigned dst = new_state(ds_dst);
-            res->new_edge(src, dst, e.cond, accepting);
+            unsigned idx = res->new_edge(src, dst, e.cond, accepting);
+            if (saveedge)
+              allaccedges.push_back(idx);
           }
       }
-
+    // Raise the destination of the "all-accepting" edges to the
+    // highest existing level.
+    auto& ev = res->edge_vector();
+    for (unsigned idx: allaccedges)
+      {
+        unsigned dst = ev[idx].dst;
+        unsigned orig_dst = (*orig_states)[dst];
+        unsigned hl = highest_level[orig_dst];
+        ev[idx].dst = ds2num[degen_state{orig_dst, hl}];
+      }
+    //orders.print();
     res->merge_edges();
     keep_bottommost_copies(res, si_orig, orig_states);
     return res;
   }
 
+
+  std::vector<acc_cond::mark_t>
+  propagate_marks_vector(const const_twa_graph_ptr& aut,
+                         scc_info* si)
+  {
+    bool own_si = true;
+    if (si)
+      own_si = false;
+    else
+      si = new scc_info(aut);
+
+    unsigned ns = aut->num_states();
+    acc_cond::mark_t allm = aut->acc().all_sets();
+    unsigned es = aut->edge_vector().size();
+    std::vector<acc_cond::mark_t> marks(es, acc_cond::mark_t{});
+    const auto& edges = aut->edge_vector();
+    for (unsigned e = 1; e < es; ++e)
+      marks[e] = edges[e].acc;
+
+    std::vector<acc_cond::mark_t> common_in(ns, allm);
+    std::vector<acc_cond::mark_t> common_out(ns, allm);
+
+    for (;;)
+      {
+        bool changed = false;
+        for (auto& e: aut->edges())
+          if (e.src != e.dst && si->scc_of(e.src) == si->scc_of(e.dst))
+            {
+              unsigned idx = aut->edge_number(e);
+              common_in[e.dst] &= marks[idx];
+              common_out[e.src] &= marks[idx];
+            }
+        for (auto& e: aut->edges())
+          if (e.src != e.dst && si->scc_of(e.src) == si->scc_of(e.dst))
+            {
+              unsigned idx = aut->edge_number(e);
+              auto acc = marks[idx] | common_in[e.src] | common_out[e.dst];
+              if (acc != marks[idx])
+                {
+                  marks[idx] = acc;
+                  changed = true;
+                }
+            }
+        if (!changed)
+          break;
+        std::fill(common_in.begin(), common_in.end(), allm);
+        std::fill(common_out.begin(), common_out.end(), allm);
+      }
+    if (own_si)
+      delete si;
+    return marks;
+  }
+
+  void propagate_marks_here(twa_graph_ptr& aut, scc_info* si)
+  {
+    auto marks = propagate_marks_vector(aut, si);
+    for (auto& e: aut->edges())
+      {
+        unsigned idx = aut->edge_number(e);
+        e.acc = marks[idx];
+      }
+  }
 }

spot/twaalgos/degen.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2015, 2017-2019 Laboratoire de
+// Copyright (C) 2012-2015, 2017-2020 Laboratoire de
 // Recherche et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -23,6 +23,8 @@
 
 namespace spot
 {
+  class scc_info;
+
   /// \ingroup twa_acc_transform
   /// \brief Degeneralize a spot::tgba into an equivalent sba with
   /// only one acceptance condition.
@@ -101,4 +103,29 @@ namespace spot
   SPOT_API twa_graph_ptr
   partial_degeneralize(const const_twa_graph_ptr& a,
                        acc_cond::mark_t todegen);
+
+  /// \ingroup twa_algorithms
+  /// \brief Propagate marks around the automaton
+  ///
+  /// For each state of the automaton, marks that are common
+  /// to all input transitions will be pushed on the outgoing
+  /// transitions, and marks that are common to all outgoing
+  /// transitions will be pulled to the input transitions.
+  /// This considers only transitions that are not self-loops
+  /// and that belong to some SCC.  If an scc_info has already
+  /// been built, pass it as \a si to avoid building it again.
+  ///
+  /// Two variants of the algorithm are provided.  One modifies
+  /// the automaton in place; the second returns a vector of marks
+  /// indexed by transition numbers.
+  ///
+  /// @{
+  SPOT_API std::vector<acc_cond::mark_t>
+  propagate_marks_vector(const const_twa_graph_ptr& aut,
+                         scc_info* si = nullptr);
+
+  SPOT_API void
+  propagate_marks_here(twa_graph_ptr& aut,
+                       scc_info* si = nullptr);
+  /// @}
 }

tests/python/pdegen.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2019, 2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -80,10 +80,10 @@ Acceptance: 2 Fin(0) | Inf(1)
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0 "2#0"
+[0] 1
+State: 1 "0#0" {0 1}
 [0] 2
-State: 1 "1#0"
+State: 2 "1#0" {1}
-[0] 2
-State: 2 "0#1" {0 1}
 [0] 1
 --END--"""
 
@@ -96,3 +96,65 @@ dd = spot.partial_degeneralize(d, [])
 assert dd.equivalent_to(d)
 assert dd.num_states() == 1
 assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'
+
+aut5 = spot.automaton(""" HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
+acc-name: generalized-Buchi 10 Acceptance: 10
+Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)&Inf(7)&Inf(8)&Inf(9)
+properties: trans-labels explicit-labels trans-acc deterministic --BODY--
+State: 0 [0&!1&2] 3 {2 4 9} State: 1 [!0&1&2] 5 {2 6 7 8} [!0&!1&!2] 0 {2}
+State: 2 [0&!1&2] 3 {1 4 9} State: 3 [0&!1&2] 4 {0 1 5 9} State: 4 [!0&!1&2] 1
+{7} [0&!1&2] 6 {1 2} State: 5 [!0&1&2] 7 {3 5} State: 6 [!0&!1&2] 2 {1 3 5}
+State: 7 [0&!1&!2] 0 {4 7} --END--""")
+
+daut5 = spot.degeneralize_tba(aut5)
+assert daut5.equivalent_to(aut5)
+sets = list(range(aut5.num_sets()))
+pdaut5 = spot.partial_degeneralize(aut5, sets)
+assert pdaut5.equivalent_to(aut5)
+assert daut5.num_states() == 10
+assert pdaut5.num_states() == 8
+
+aut6 = spot.automaton("""HOA: v1 States: 6 Start: 0 AP: 3 "p0" "p1" "p2"
+acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties:
+trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0
+[0&!1&!2] 4 {1} State: 1 [!0&!1&!2] 2 {0 1} State: 2 [!0&1&2] 0 {1} State: 3
+[0&1&!2] 5 {1} State: 4 [!0&1&!2] 0 {1 2} [0&!1&!2] 3 {0} State: 5 [!0&1&2] 1
+--END-- """)
+daut6 = spot.degeneralize_tba(aut6)
+assert daut6.equivalent_to(aut6)
+sets = list(range(aut6.num_sets()))
+pdaut6 = spot.partial_degeneralize(aut6, sets)
+assert pdaut6.equivalent_to(aut6)
+assert daut6.num_states() == 8
+assert pdaut6.num_states() == 8
+
+
+aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
+acc-name: generalized-Buchi 4 Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc deterministic --BODY--
+State: 0 [0&!1&2] 1 {2 3} State: 1 [0&!1&2] 0 {0 2} [0&!1&!2] 6 State: 2
+[0&1&2] 0 [!0&!1&2] 5 [!0&1&!2] 6 {1} State: 3 [0&!1&2] 5 [0&!1&!2] 6 State: 4
+[!0&!1&!2] 3 State: 5 [0&1&!2] 0 [!0&1&2] 7 State: 6 [0&1&2] 2 {1} State: 7
+[!0&!1&2] 0 {0} [!0&1&!2] 4 --END--""")
+daut7 = spot.degeneralize_tba(aut7)
+assert daut7.equivalent_to(aut7)
+sets = list(range(aut7.num_sets()))
+pdaut7 = spot.partial_degeneralize(aut7, sets)
+assert pdaut7.equivalent_to(aut7)
+assert daut7.num_states() == 11
+assert pdaut7.num_states() == 10
+
+aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
+acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)
+properties: trans-labels explicit-labels trans-acc deterministic --BODY--
+State: 0 [!0&1&!2] 7 {0} State: 1 [!0&1&2] 1 {4} [0&!1&2] 6 {1 2} State: 2
+[!0&!1&2] 3 {1 2} [0&1&2] 5 State: 3 [0&1&2] 2 {2} State: 4 [!0&!1&!2] 3 State:
+5 [!0&1&!2] 0 {1 3} State: 6 [0&1&2] 4 [0&1&!2] 6 State: 7 [!0&!1&!2] 1
+--END--""")
+daut8 = spot.degeneralize_tba(aut8)
+assert daut8.equivalent_to(aut8)
+sets = list(range(aut8.num_sets()))
+pdaut8 = spot.partial_degeneralize(aut8, sets)
+assert pdaut8.equivalent_to(aut8)
+assert daut8.num_states() == 22
+assert pdaut8.num_states() == 9