Introduce mealy_prod

Product between mealy machines
with propagation of synthesis outputs
and additional assertions.
Currently it only supports input complete machines

* spot/twaalgos/mealy_machine.cc,
  spot/twaalgos/mealy_machine.hh: Here
* bin/ltlsynt.cc: Use
* tests/python/except.py,
  tests/python/synthesis.ipynb: Test

spot/twaalgos/mealy_machine.cc

@@ -34,6 +34,7 @@
 #include <spot/misc/minato.hh>
 #include <spot/twaalgos/game.hh>
 #include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/synthesis.hh>
 
 #include <picosat/picosat.h>
@@ -55,6 +56,7 @@
 
 namespace
 {
+  using namespace spot;
   bool is_deterministic_(const std::vector<bdd>& ins)
   {
     const unsigned n_ins = ins.size();
@@ -64,6 +66,24 @@ namespace
           return false;
     return true;
   }
+
+  bool is_complete_(const const_twa_graph_ptr& m,
+                    const bdd& outs)
+  {
+    auto* sp = m->get_named_prop<region_t>("state-player");
+    const auto N = m->num_states();
+    for (auto s = 0u; s < N; ++s)
+      {
+        if (sp && sp->at(s))
+          continue; // No need tpo check player states
+        bdd all_cond = bddfalse;
+        for (const auto& e : m->out(s))
+          all_cond |= bdd_exist(e.cond, outs);
+        if (all_cond != bddtrue)
+          return false;
+      }
+    return true;
+  }
 }
 
 
@@ -3843,4 +3863,38 @@ namespace spot
     return true;
   }
 
+  twa_graph_ptr
+  mealy_product(const const_twa_graph_ptr& left,
+                const const_twa_graph_ptr& right)
+  {
+    bdd outs[] = {get_synthesis_outputs(left),
+                  get_synthesis_outputs(right)};
+
+#ifndef NDEBUG
+    for (const auto& [m, n, o] : {std::tuple{left, "left", outs[0]},
+                                            {right, "right", outs[1]}})
+      {
+        if (!is_mealy(m))
+          throw std::runtime_error(std::string("mealy_prod(): ") + n
+                                  + " is not a mealy machine");
+        if (!is_complete_(m, o))
+          throw std::runtime_error(std::string("mealy_prod(): ") + n
+                                   + " is not input complete");
+      }
+#endif
+
+    auto p = product(left, right);
+    bdd pouts = outs[0] & outs[1];
+    set_synthesis_outputs(p, pouts);
+
+#ifndef NDEBUG
+    if (!is_mealy(p))
+      throw std::runtime_error("mealy_prod(): Prooduct is not mealy");
+    if (!is_complete_(p, pouts))
+      throw std::runtime_error("mealy_prod(): Prooduct is not input complete. "
+                               "Incompatible machines?");
+#endif
+
+    return p;
+  }
 }

spot/twaalgos/mealy_machine.hh

@@ -128,4 +128,14 @@ namespace spot
   is_split_mealy_specialization(const_twa_graph_ptr left,
                                 const_twa_graph_ptr right,
                                 bool verbose = false);
+
+  /// \brief Product between two mealy machines \a left and \a right.
+  /// \pre The machines have to be both either split or unsplit,
+  /// input complete and compatible. All of this is check by assertion
+  /// \result The mealy machine representing the shared behaviour.
+  /// The resulting machine has the same class (mealy/separated/split)
+  /// as the input machines
+  SPOT_API twa_graph_ptr
+  mealy_product(const const_twa_graph_ptr& left,
+                const const_twa_graph_ptr& right);
 }