split: add separate_edges() and a edge_separator class

This generalizes (and replaces) the two-argument split that was
introduced in c2832cabfc.

* spot/twaalgos/split.cc, spot/twaalgos/split.hh (edge_separator): New
class.
(separate_edges): New function.
(split_edges): Remove the two argument version.
* spot/twaalgos/forq_contains.cc: Adjust to use the edge_separator
class.
* tests/python/splitedge.py: Adjust test case.
* tests/python/split.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention it.

NEWS

@@ -135,6 +135,9 @@ New in spot 2.11.6.dev  (not yet released)
     Büchi automaton will always return a Büchi automaton.  For those,
     a "keep_one_color" option has been added to scc_filter.
 
+  - spot::separate_edges() and spot::edge_separator offers more ways
+    to split labels.  See https://spot.lrde.epita.fr/ipynb/split.html
+
   - ltsmin's interface will now point to README.ltsmin in case an
     error is found while running divine or spins.
 

doc/org/tut.org

@@ -71,6 +71,7 @@ real notebooks instead.
   conditions
 - [[https://spot.lrde.epita.fr/ipynb/contains.html][=contains.ipynb=]] demonstrates containment checks between formulas or
   automata
+- [[https://spot.lrde.epita.fr/ipynb/split.html][=split.ipynb=]] illustrates various ways to split labels
 - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata
   in Python
 - [[https://spot.lrde.epita.fr/ipynb/games.html][=games.ipynb=]] illustrates support for games

spot/twaalgos/forq_contains.cc

@@ -695,19 +695,6 @@ namespace spot::forq::util
     return all_states;
   }
 
-  // Create a list of bdds, where each corresponds to an edge in B
-  static std::vector<bdd> create_edge_splitting_basis(const_graph const& B)
-  {
-    auto edges = B->edges();
-    std::unordered_set<bdd, ::spot::bdd_hash> out;
-    std::transform(edges.begin(), edges.end(), std::inserter(out, out.begin()),
-      [](auto& edge)
-        {
-          return edge.cond;
-        });
-    return std::vector<bdd>(out.begin(), out.end());
-  }
-
   forq_context create_forq_context(const_graph const& A, const_graph const& B)
   {
     forq_context retval;
@@ -715,7 +702,9 @@ namespace spot::forq::util
     retval.B.outgoing = util::generate_outgoing_states(B);
     retval.B.final_edges = get_final_edges(B);
 
-    retval.A.aut = split_edges(A, create_edge_splitting_basis(B));
+    edge_separator es;
+    es.add_to_basis(B);
+    retval.A.aut = es.separate_compat(A);
     retval.A.outgoing = util::generate_outgoing_states(retval.A.aut);
     retval.A.final_edges = get_final_edges(retval.A.aut);
     retval.cache.precomputed_ipost.resize(B->num_states());

spot/twaalgos/split.cc

@@ -22,180 +22,10 @@
 #include <spot/priv/robin_hood.hh>
 #include <unordered_set>
 
-namespace std
-{
-  template<>
-  struct hash<::bdd>
-  {
-    size_t operator()(::bdd const& instance) const noexcept
-    {
-      return ::spot::bdd_hash{}(instance);
-    }
-  };
-
-  template<>
-  struct hash<pair<bdd, bdd>>
-  {
-    size_t operator()(pair<bdd, bdd> const& x) const noexcept
-    {
-      size_t first_hash = std::hash<bdd>()(x.first);
-      size_t second_hash = std::hash<bdd>()(x.second);
-      size_t sum = second_hash
-                   + 0x9e3779b9
-                   + (first_hash << 6)
-                   + (first_hash >> 2);
-      return  first_hash ^ sum;
-    }
-  };
-}
-
 namespace spot
 {
   namespace
   {
-    // We attempt to add a potentially new set of symbols defined as "value" to
-    // our current set of edge partitions, "current_set". We also specify a set
-    // of valid symbols considered
-    static void
-    add_to_lower_bound_set_helper(std::unordered_set<bdd>& current_set,
-                                  bdd valid_symbol_set, bdd value)
-    {
-      // This function's correctness is defined by the invariant, that
-      // we never add a bdd to our current set unless the bdd is
-      // disjoint from every other element in the current_set. In
-      // other words, we will only reach the final set.insert(value),
-      // if we can iterate over the whole of current_set without
-      // finding some set intersections
-      if (value == bddfalse) // Don't add empty sets, as they subsume everything
-        {
-          return;
-        }
-      for (auto sym : current_set)
-        {
-          // If a sym is a subset of value, recursively add the set of symbols
-          // defined in value, but not in sym. This ensures the two elements
-          // are disjoint.
-          if (bdd_implies(sym, value))
-            {
-              add_to_lower_bound_set_helper(current_set,
-                                            valid_symbol_set,
-                                            (value - sym) & valid_symbol_set);
-              return;
-            }
-          // If a sym is a subset of the value we're trying to add, then we
-          // remove the symbol and add the two symbols created by partitioning
-          // the sym with value.
-          else if (bdd_implies(value, sym))
-            {
-              current_set.erase(sym);
-              add_to_lower_bound_set_helper(current_set,
-                                            valid_symbol_set,
-                                            sym & value);
-              add_to_lower_bound_set_helper(current_set,
-                                            valid_symbol_set,
-                                            sym - value);
-              return;
-            }
-        }
-      // This line is only reachable if value is not a subset and doesn't
-      // subsume any element currently in our set
-      current_set.insert(value);
-    }
-
-    using bdd_set = std::unordered_set<bdd>;
-    using bdd_pair_set = std::unordered_set<std::pair<bdd, bdd>>;
-
-    // Transforms each element of the basis into a complement pair,
-    // with a valid symbol set specified
-    static bdd_pair_set create_complement_pairs(std::vector<bdd> const& basis,
-                                                bdd valid_symbol_set)
-    {
-      bdd_pair_set intersections;
-      for (bdd sym: basis)
-        {
-          bdd intersection = sym & valid_symbol_set;
-          if (intersection != bddfalse)
-            {
-              bdd negation = valid_symbol_set - intersection;
-              intersections.insert(std::make_pair(intersection, negation));
-            }
-        }
-      return intersections;
-    }
-
-    template<typename Callable>
-    void iterate_possible_intersections(bdd_pair_set const& complement_pairs,
-                                        bdd valid_symbol_set,
-                                        Callable callable)
-    {
-      for (auto it = complement_pairs.begin();
-           it != complement_pairs.end(); ++it)
-        for (auto it2 = std::next(it); it2 != complement_pairs.end(); ++it2)
-          {
-            auto intermediate = it2->first & valid_symbol_set;
-            auto intermediate2 = it2->second & valid_symbol_set;
-            callable(it->first & intermediate);
-            callable(it->second & intermediate);
-            callable(it->first & intermediate2);
-            callable(it->second & intermediate2);
-          }
-    }
-
-    // Compute the lower set bound of a set. A valid symbol set is also
-    // provided to make sure that no symbol exists in the output if it is
-    // not also included in the valid symbol set
-    static bdd_set lower_set_bound(std::vector<bdd> const& basis,
-                                   bdd valid_symbol_set)
-    {
-      auto complement_pairs = create_complement_pairs(basis, valid_symbol_set);
-      if (complement_pairs.size() == 1)
-        {
-          bdd_set lower_bound;
-          auto& pair = *complement_pairs.begin();
-          if (pair.first != bddfalse
-              && bdd_implies(pair.first, valid_symbol_set))
-            lower_bound.insert(pair.first);
-          if (pair.second != bddfalse
-              && bdd_implies(pair.second, valid_symbol_set))
-            lower_bound.insert(pair.second);
-          return lower_bound;
-        }
-      else
-        {
-          bdd_set lower_bound;
-          iterate_possible_intersections(complement_pairs, valid_symbol_set,
-             [&](auto intersection)
-             {
-               add_to_lower_bound_set_helper(lower_bound,
-                                             valid_symbol_set,
-                                             intersection);
-             });
-          return lower_bound;
-        }
-    }
-
-    // Partitions a symbol based on a list of other bdds called the
-    // basis.  The resulting partition will have the property that for
-    // any partitioned element and any element element in the basis,
-    // the partitioned element will either by completely contained by
-    // that element of the basis, or completely disjoint.
-    static bdd_set
-    generate_contained_or_disjoint_symbols(bdd sym,
-                                           std::vector<bdd> const& basis)
-    {
-      auto lower_bound = lower_set_bound(basis, sym);
-      // If the sym was disjoint from everything in the basis, we'll
-      // be left with an empty lower_bound. To fix this, we will
-      // simply return a singleton, with sym as the only
-      // element. Notice, this singleton will satisfy the requirements
-      // of a return value from this function. Additionally, if the
-      // sym is false, that means nothing can traverse it, so we
-      // simply are left with no edges.
-      if (lower_bound.empty() && sym != bddfalse)
-        lower_bound.insert(sym);
-      return lower_bound;
-    }
-
     template<typename genlabels>
     twa_graph_ptr split_edges_aux(const const_twa_graph_ptr& aut,
                                   genlabels gen)
@@ -217,7 +47,7 @@ namespace spot
       // robin_hood::unordered_map with GCC 9.4.  Use robin_hood::pair
       // instead.
       typedef robin_hood::pair<unsigned, unsigned> cached_t;
-      robin_hood::unordered_map<unsigned, cached_t> split_cond;
+      robin_hood::unordered_map<int, cached_t> split_cond;
 
       internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph());
 
@@ -260,12 +90,60 @@ namespace spot
     });
   }
 
-  twa_graph_ptr split_edges(const const_twa_graph_ptr& aut,
+  void edge_separator::add_to_basis(bdd label)
-                            std::vector<bdd> const& basis)
   {
-    bdd all = aut->ap_vars();
+    if (label == bddfalse)
-    return split_edges_aux(aut, [&](bdd cond) {
+      return;
-      return generate_contained_or_disjoint_symbols(cond, basis);
+    // Split our current set of labels using this new one.
+    //
+    // Do not use a range-based or iterator-based for loop here,
+    // as push_back invalidates the end iterator.
+    for (unsigned cur = 0, sz = basis_.size(); cur < sz; ++cur)
+      if (bdd common = basis_[cur] & label;
+          common != bddfalse && common != basis_[cur])
+        {
+          basis_[cur] -= label;
+          basis_.push_back(common);
+        }
+  }
+
+  void edge_separator::add_to_basis(const const_twa_graph_ptr& aut)
+  {
+    for (formula f: aut->ap())
+      aps_.insert(f);
+
+    robin_hood::unordered_set<int> seen{bddtrue.id()};
+    for (auto& e: aut->edges())
+      if (bdd lab = e.cond; seen.insert(lab.id()).second)
+        add_to_basis(lab);
+  }
+
+  twa_graph_ptr
+  edge_separator::separate_implying(const const_twa_graph_ptr& aut)
+  {
+    auto res = split_edges_aux(aut, [this](bdd cond) {
+      return this->separate_implying(cond);
     });
+    for (formula f: aps_)
+      res->register_ap(f);
+    return res;
+  }
+
+  twa_graph_ptr
+  edge_separator::separate_compat(const const_twa_graph_ptr& aut)
+  {
+    auto res = split_edges_aux(aut, [this](bdd cond) {
+      return this->separate_compat(cond);
+    });
+    for (formula f: aps_)
+      res->register_ap(f);
+    return res;
+  }
+
+  twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut)
+  {
+    edge_separator es;
+    es.add_to_basis(aut);
+    return es.separate_implying(aut);
   }
 }

spot/twaalgos/split.hh

@@ -28,17 +28,198 @@ namespace spot
   ///
   /// Create a new version of the automaton where all edges are split
   /// so that they are all labeled by a conjunction of all atomic
-  /// propositions. After this we can consider that each edge of the
+  /// propositions.
-  /// automate is a transition labeled by one letter.
+  ///
+  /// So if an edge is labeled by "true", it will be split into
+  /// $2^{AP}$ distinct edges.
+  ///
+  /// After this we can consider that each edge of the automaton is a
+  /// transition labeled by one of $2^{AP}$ letters.
+  ///
+  /// \see separate_edges
   SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut);
 
+#ifndef SWIG
+  // pseudo container that we use to iterate over
+  // the items of LABELS that are compatible with COND.
+  template<bool subsumed>
+  struct SPOT_API edge_separator_filter
+    {
+      edge_separator_filter(const std::vector<bdd>& labels, bdd cond)
+      : labels_(labels), cond_(cond)
+      {
+      }
+
+      class iterator
+      {
+        std::vector<bdd>::const_iterator pos_;
+        std::vector<bdd> const& labels_;
+        bdd cond_;
+
+      public:
+        iterator(const std::vector<bdd>& labels, bdd cond)
+          : labels_(labels), cond_(cond)
+        {
+          pos_ = labels_.begin();
+          next();
+        }
+
+        iterator& operator++()
+        {
+          ++pos_;
+          next();
+          return *this;
+        }
+
+        void next()
+        {
+          // If subsumed is true, we want to match the labels
+          // that imply the current condition.  Otherwise we
+          // want to match the labels that are compatible.
+          while (pos_ != labels_.end() &&
+                 ((subsumed && !bdd_implies(*pos_, cond_))
+                  || (!subsumed && (*pos_ & cond_) == bddfalse)))
+            ++pos_;
+        }
+
+        bdd operator*() const
+        {
+          if (subsumed)
+            return *pos_;
+          else
+            return *pos_ & cond_;
+        }
+
+        bool operator==(const iterator& other) const
+        {
+          return pos_ == other.pos_;
+        }
+
+        bool operator!=(const iterator& other) const
+        {
+          return pos_ != other.pos_;
+        }
+
+        bool operator==(std::vector<bdd>::const_iterator pos) const
+        {
+          return pos_ == pos;
+        }
+
+        bool operator!=(std::vector<bdd>::const_iterator pos) const
+        {
+          return pos_ != pos;
+        }
+      };
+
+      iterator begin() const
+      {
+        return iterator(labels_, cond_);
+      }
+
+      std::vector<bdd>::const_iterator end() const
+      {
+        return labels_.end();
+      }
+
+    private:
+      const std::vector<bdd>& labels_;
+      bdd cond_;
+    };
+#endif
+
+
   /// \ingroup twa_misc
-  /// \brief transform edges into transitions based on set of bdds
+  /// \brief separate edges so that their labels are disjoint
+  ///
+  /// To use this class, first call add_to_basis() for each label that
+  /// you want to separate.  Then call separate() to get a new
+  /// automaton.
+  ///
+  /// Note that all labels seen by separate() should have been
+  /// previously declared using add_to_basis(), but more can be
+  /// declared.
+  ///
+  /// For instance an automaton has labels in {a,b,!a&!b&c} and those
+  /// are used as basis, the separated automaton should have its
+  /// labels among {a&!b,a&b,!a&b,!a&!b&c}.
+  class SPOT_API edge_separator
+  {
+  public:
+    /// \brief add label(s) to a basis
+    ///
+    /// Add a single label, or all the labels of an automaton.
+    ///
+    /// The version that takes an automaton will also record the
+    /// atomic propositions used by the automaton.  Those atomic
+    /// propositions will be registered by separate_implying() or
+    /// separate_compat().  If you call the BDD version of
+    /// add_to_basis() and add a new atomic proposition, you should
+    /// remember to register it in the result of separate_implying()
+    /// or separate_compat() yourself.
+    /// @{
+    void add_to_basis(bdd label);
+    void add_to_basis(const const_twa_graph_ptr& aut);
+    /// @}
+    /// \brief Separate an automaton
+    ///
+    /// This variant replaces each edge labeled by L by an edge
+    /// for each label of the basis that is implies L.  This
+    /// faster than separate_compat when all edges of aut have
+    /// been declared in the basis.
+    twa_graph_ptr separate_implying(const const_twa_graph_ptr& aut);
+    /// \brief Separate an automaton
+    ///
+    /// This variant replaces each edge labeled by L by an edge for
+    /// each label of the basis that compatible implies L.  This
+    /// faster than separate_compat when all edges of aut have been
+    /// declared in the basis.
+    twa_graph_ptr separate_compat(const const_twa_graph_ptr& aut);
+#ifndef SWIG
+    /// \brief Separate a label
+    ///
+    /// This returns a pseudo-container that can be used to iterate
+    /// over the elements of the basis that imply the current label.
+    ///
+    /// For instance if the basis was created from {a,b} (i.e., the
+    /// basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is
+    /// {a}, the result will be {a&!b,a&b}.
+    edge_separator_filter<true> separate_implying(bdd label)
+    {
+      return {basis_, label};
+    }
+    /// \brief Separate a label
+    ///
+    /// This returns a pseudo-container that can be used to iterate
+    /// over the elements of the basis compatible with the current labal.
+    ///
+    /// For instance if the basis was created from {a,b} (i.e., the
+    /// basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is
+    /// {c&a}, the result will be {a&!b&c,a&b&c}.
+    edge_separator_filter<false> separate_compat(bdd label)
+    {
+      return {basis_, label};
+    }
+#endif
+    unsigned basis_size() const
+    {
+      return basis_.size();
+    }
+  private:
+    std::vector<bdd> basis_{bddtrue};
+    std::set<formula> aps_;
+  };
+
+  /// \ingroup twa_misc
+  /// \brief Make edge labels disjoints
   ///
   /// Create a new version of the automaton where all edges are split
-  /// such that, for any transformed edge and any set of symbols in
+  /// in such a way that two labels are either equal or disjoint.
-  /// the basis, the transformed edge is either completely disjoint
+  ///
-  /// from the set of symbols, or it is a subset of them.
+  /// For instance if the automaton uses only {a,b,!a&!b&c} as labels,
-  SPOT_API twa_graph_ptr split_edges(
+  /// the result should have label among {a&!b,a&b,!a&b,!a&!b&c}.
-    const const_twa_graph_ptr& aut, std::vector<bdd> const& basis);
+  ///
+  /// Using split_edges() also creates an automaton with separated labels,
+  /// but the separation will be much finer since it will result in a much
+  /// involves all atomtic proposition.
+  SPOT_API twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut);
 }

tests/Makefile.am

@@ -378,6 +378,7 @@ TESTS_ipython = \
   python/randaut.ipynb \
   python/randltl.ipynb \
   python/satmin.ipynb \
+  python/split.ipynb \
   python/stutter-inv.ipynb \
   python/synthesis.ipynb \
   python/testingaut.ipynb \

tests/python/splitedge.py

@@ -27,8 +27,11 @@ def create_aps(aut):
 
 def do_edge_test(aut, aps, edges_before, edges_after):
     tc.assertEqual(aut.num_edges(), edges_before)
-    aut = spot.split_edges(aut, aps)
+    es = spot.edge_separator()
-    tc.assertEqual(aut.num_edges(), edges_after)
+    for ap in aps:
+        es.add_to_basis(ap)
+    res = es.separate_compat(aut)
+    tc.assertEqual(res.num_edges(), edges_after)
 
 aut = spot.automaton("""
 HOA: v1