From 488efee7b3c1391116eb1effa61c8d5ee1b10de5 Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber <philipp@lrde.epita.fr>
Date: Mon, 22 Nov 2021 14:14:28 +0100
Subject: [PATCH] aiger accepts splitted mealy machines

* spot/twaalgos/aiger.cc,
  spot/twaalgos/aiger.hh: Here
* tests/python/synthesis.ipynb: Tests
---
 spot/twaalgos/aiger.cc       | 106 +++++++---
 spot/twaalgos/aiger.hh       |   4 +-
 tests/python/synthesis.ipynb | 384 +++++++++++++++++++++++++++++++++--
 3 files changed, 456 insertions(+), 38 deletions(-)

diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index ae7b665e9..d846e678c 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -1379,7 +1379,8 @@ namespace
   using namespace spot;
 
   // We have to decide which actual output to use:
-  // Heuristic : Use the assignment having the least highs
+  // Heuristic : Use the assignment having the smallest cost
+  // according to satoneshortest
   static std::vector<std::vector<bdd>>
   choose_outc(const std::vector<std::pair<const_twa_graph_ptr, bdd>>&
                   strat_vec,
@@ -1387,18 +1388,44 @@ namespace
   {
     std::vector<std::vector<bdd>> used_outc;
 
-    for (auto&& astrat : strat_vec)
+    for (const auto& astrat : strat_vec)
       {
         used_outc.emplace_back(astrat.first->num_edges()+1);
         auto& this_outc = used_outc.back();
 
-        for (auto&& e: astrat.first->edges())
+        // Check if split or separated
+        if (auto sp_ptr =
+              astrat.first->get_named_prop<region_t>("state-player"))
           {
-            assert(e.cond != bddfalse);
-            bdd bout = bdd_exist(e.cond, all_inputs);
-            // low is good, dc is ok, high is bad
-            this_outc[astrat.first->edge_number(e)] =
-                bdd_satoneshortest(bout, 0, 1, 5);
+            // Split -> We only need outs for env edges
+            auto sp = *sp_ptr;
+            const unsigned N = astrat.first->num_states();
+            for (unsigned s = 0; s < N; ++s)
+              {
+                if (sp[s])
+                  continue; //Player state -> nothing to do
+                for (const auto& e : astrat.first->out(s))
+                  {
+                    assert(e.cond != bddfalse);
+                    bdd bout = astrat.first->out(e.dst).begin()->cond;
+                    assert(bout != bddfalse);
+                    // low is good, dc is ok, high is bad
+                    this_outc[astrat.first->edge_number(e)] =
+                        bdd_satoneshortest(bout, 0, 1, 5);
+                  }
+              }
+          }
+        else
+          {
+            // separated
+            for (const auto& e: astrat.first->edges())
+              {
+                assert(e.cond != bddfalse);
+                bdd bout = bdd_exist(e.cond, all_inputs);
+                // low is good, dc is ok, high is bad
+                this_outc[astrat.first->edge_number(e)] =
+                    bdd_satoneshortest(bout, 0, 1, 5);
+              }
           }
       }
     //Done
@@ -1409,6 +1436,7 @@ namespace
   state_to_vec(std::vector<unsigned>& v, unsigned s,
                unsigned offset)
   {
+    assert(s != -1u && "-1u is not a valid sstate");
     v.clear();
     unsigned i = offset;
     while (s > 0)
@@ -1466,8 +1494,10 @@ namespace
         }
     // This checks the acc again, but does more and is to
     // costly for non-debug mode
+    // We can also handle split machines
     assert(std::all_of(strat_vec.begin(), strat_vec.end(),
-           [](const auto& p){ return is_separated_mealy(p.first); }));
+           [](const auto& p){ return is_separated_mealy(p.first)
+                                     || is_split_mealy(p.first); }));
 
     // get the propositions
     std::vector<std::string> input_names;
@@ -1558,30 +1588,48 @@ namespace
     unsigned n_latches = 0;
     for (const auto& astrat : strat_vec)
       {
-        state_numbers.emplace_back();
-        state_numbers.back().reserve(astrat.first->num_states());
+        const unsigned N = astrat.first->num_states();
+        state_numbers.emplace_back(N, -1u);
+        auto& sn = state_numbers.back();
         unsigned max_index = 0;
         // Check if named
+        auto sp_ptr = astrat.first->get_named_prop<region_t>("state-player");
         if (const auto* s_names =
                 astrat.first->
                   get_named_prop<std::vector<std::string>>("state-names"))
           {
-            std::transform(s_names->cbegin(), s_names->cend(),
-                           std::back_inserter(state_numbers.back()),
-                           [&max_index](const auto& sn)
-                           {
-                             unsigned su = std::stoul(sn);
-                             max_index = std::max(max_index, su);
-                             return su;
-                           });
+            for (unsigned n = 0; n < N; ++n)
+              {
+                if (sp_ptr && (*sp_ptr)[n])
+                  continue;
+                // Remains -1u
+                unsigned su = std::stoul((*s_names)[n]);
+                max_index = std::max(max_index, su);
+                sn[n] = su;
+              }
             ++max_index;
           }
         else
           {
-            max_index = astrat.first->num_states();
-            state_numbers.back().resize(astrat.first->num_states());
-            std::iota(state_numbers.back().begin(),
-                      state_numbers.back().end(), 0);
+            if (sp_ptr)
+              {
+                auto sp = *sp_ptr;
+                // Split
+                unsigned n_next = 0;
+                // Player -1u
+                // Env: Succesively numbered according to appearance
+                for (unsigned n = 0; n < N; ++n)
+                  if (!sp[n])
+                    sn[n] = n_next++;
+                max_index = n_next;
+              }
+            else
+              {
+                std::iota(state_numbers.back().begin(),
+                          state_numbers.back().end(), 0);
+                max_index = N;
+              }
+
             // Ensure 0 <-> init state
             std::swap(state_numbers.back()[0],
                       state_numbers.back()[astrat.first->
@@ -1621,6 +1669,8 @@ namespace
         auto&& [astrat, aouts] = strat_vec[i];
         const auto& sn = state_numbers.at(i);
 
+        auto sp_ptr = astrat->get_named_prop<region_t>("state-player");
+
         auto latchoff = latch_offset[i];
 #ifndef NDEBUG
         auto latchoff_next = latch_offset.at(i+1);
@@ -1628,6 +1678,8 @@ namespace
         auto alog2n = log2n[i];
         auto state2bdd = [&](auto s)
           {
+            assert((!sp_ptr || !(*sp_ptr)[s])
+                    && "Only env states need to be encoded.");
             auto s2 = sn[s];
             bdd b = bddtrue;
             for (unsigned j = 0; j < alog2n; ++j)
@@ -1654,13 +1706,19 @@ namespace
 
         for (unsigned s = 0; s < astrat->num_states(); ++s)
           {
+            // Player state -> continue
+            if (sp_ptr && (*sp_ptr)[s])
+              continue;
             // Convert src state to bdd
             bdd src_bdd = state2bdd(s);
 
             for (const auto& e : astrat->out(s))
               {
                 // High latches of dst
-                state_to_vec(next_state_vec, sn[e.dst], latchoff);
+                state_to_vec(next_state_vec,
+                             sp_ptr ? sn[astrat->out(e.dst).begin()->dst]
+                                    : sn[e.dst],
+                             latchoff);
 
                 // Get high outs depending on cond
                 output_to_vec(out_vec, out_dc_vec,
diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh
index 707f1bc3c..c89ae1ecb 100644
--- a/spot/twaalgos/aiger.hh
+++ b/spot/twaalgos/aiger.hh
@@ -452,9 +452,9 @@ namespace spot
   ///@}
 
   /// \ingroup synthesis
-  /// \brief Convert multiple strategies into an aig relying on
+  /// \brief Convert multiple mealy machines into an aig relying on
   ///        the transformation described by mode.
-  /// \note The states of each strategy are represented by a block of latches
+  /// \note The states of each machine are represented by a block of latches
   ///       not affected by the others. For this to work in a general setting,
   ///       the outputs must be disjoint.
   ///
diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb
index 91f526508..be001a9b3 100644
--- a/tests/python/synthesis.ipynb
+++ b/tests/python/synthesis.ipynb
@@ -698,7 +698,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc79b6f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7ff27d57dc90> >"
       ]
      },
      "metadata": {},
@@ -2718,7 +2718,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc79ba50> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7ff27d4e7300> >"
       ]
      },
      "metadata": {},
@@ -3039,7 +3039,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc6a8360> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7ff27ca90390> >"
       ]
      },
      "metadata": {},
@@ -3114,7 +3114,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bd884390> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7ff27d57dd20> >"
       ]
      },
      "metadata": {},
@@ -3191,7 +3191,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8660> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7ff27d57d660> >"
       ]
      },
      "metadata": {},
@@ -3318,7 +3318,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8900> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7ff27d4e70c0> >"
       ]
      },
      "metadata": {},
@@ -3345,7 +3345,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 11,
    "id": "4f9be142",
    "metadata": {},
    "outputs": [
@@ -3753,7 +3753,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6ae030> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7ff29402fa80> >"
       ]
      },
      "metadata": {},
@@ -3926,7 +3926,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8d50> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7ff27ca90b10> >"
       ]
      },
      "metadata": {},
@@ -4050,7 +4050,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc6a8330> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7ff27ca90cf0> >"
       ]
      },
      "execution_count": 16,
@@ -4061,11 +4061,371 @@
    "source": [
     "this_aig.as_automaton()"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "671b849d",
+   "metadata": {},
+   "source": [
+    "Note that the generation of aiger circuits from mealy machines is flexible and accepts separated mealy machines\n",
+    "as well as split mealy machines."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "id": "fcf3b73e",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"170pt\" height=\"126pt\"\n",
+       " viewBox=\"0.00 0.00 170.00 126.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 122)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-122 166,-122 166,4 -4,4\"/>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"81\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"81\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M26.15,-18C27.79,-18 42.15,-18 55.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.94,-18 55.94,-21.15 59.44,-18 55.94,-18 55.94,-18 55.94,-18 59.44,-18 55.94,-14.85 62.94,-18 62.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M77.76,-35.78C77.21,-45.31 78.29,-54 81,-54 82.99,-54 84.1,-49.32 84.33,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"84.24,-35.78 87.48,-42.74 84.28,-39.28 84.33,-42.78 84.33,-42.78 84.33,-42.78 84.28,-39.28 81.18,-42.82 84.24,-35.78 84.24,-35.78\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"2,-55.5 2,-74.5 120,-74.5 120,-55.5 2,-55.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"4\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1) | (i0 &amp; i1)</text>\n",
+       "<text text-anchor=\"start\" x=\"124\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"135,-55.5 135,-74.5 160,-74.5 160,-55.5 135,-55.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"137\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">!o0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M75.83,-35.41C72.6,-54.42 74.32,-77 81,-77 86.84,-77 88.89,-59.71 87.15,-42.65\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"86.17,-35.41 90.23,-41.93 86.64,-38.88 87.11,-42.35 87.11,-42.35 87.11,-42.35 86.64,-38.88 83.98,-42.77 86.17,-35.41 86.17,-35.41\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"4,-78.5 4,-97.5 122,-97.5 122,-78.5 4,-78.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"6\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; i1) | (i0 &amp; !i1)</text>\n",
+       "<text text-anchor=\"start\" x=\"126\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"137,-78.5 137,-97.5 158,-97.5 158,-78.5 137,-78.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"139\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"286pt\" height=\"174pt\"\n",
+       " viewBox=\"0.00 0.00 286.00 173.85\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 169.85)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-169.85 282,-169.85 282,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"136\" y=\"-150.65\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"128\" y=\"-135.65\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-66.85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-63.15\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-66.85C2.79,-66.85 17.15,-66.85 30.63,-66.85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-66.85 30.94,-70 34.44,-66.85 30.94,-66.85 30.94,-66.85 30.94,-66.85 34.44,-66.85 30.94,-63.7 37.94,-66.85 37.94,-66.85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-116.85 224,-98.85 251,-80.85 278,-98.85 251,-116.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"251\" y=\"-95.15\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M66.88,-81.2C73.09,-88.89 81.84,-97.64 92,-101.85 135.6,-119.91 191.93,-112.35 224.21,-105.44\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"231.1,-103.9 224.96,-108.5 227.69,-104.67 224.27,-105.43 224.27,-105.43 224.27,-105.43 227.69,-104.67 223.58,-102.36 231.1,-103.9 231.1,-103.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-116.65\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1) | (i0 &amp; i1)</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-51.85 224,-33.85 251,-15.85 278,-33.85 251,-51.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"251\" y=\"-30.15\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M71.81,-57.65C77.85,-54.33 85.05,-50.89 92,-48.85 134.16,-36.51 185.09,-33.72 217.52,-33.38\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"224.54,-33.34 217.56,-36.53 221.04,-33.36 217.54,-33.38 217.54,-33.38 217.54,-33.38 221.04,-33.36 217.53,-30.23 224.54,-33.34 224.54,-33.34\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-52.65\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; i1) | (i0 &amp; !i1)</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M233.99,-91.97C225.76,-88.71 215.5,-85.06 206,-82.85 162.78,-72.83 111.01,-69.06 81.27,-67.66\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"74.21,-67.35 81.34,-64.51 77.7,-67.51 81.2,-67.66 81.2,-67.66 81.2,-67.66 77.7,-67.51 81.06,-70.81 74.21,-67.35 74.21,-67.35\"/>\n",
+       "<text text-anchor=\"start\" x=\"138.5\" y=\"-86.65\" font-family=\"Lato\" font-size=\"14.00\">!o0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M235.87,-25.56C227.5,-21.13 216.5,-16.13 206,-13.85 156.48,-3.13 136.62,10.15 92,-13.85 80.15,-20.23 71.64,-32.57 65.99,-43.74\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.98,-50.13 63.11,-42.46 64.47,-46.96 65.96,-43.8 65.96,-43.8 65.96,-43.8 64.47,-46.96 68.81,-45.14 62.98,-50.13 62.98,-50.13\"/>\n",
+       "<text text-anchor=\"start\" x=\"140.5\" y=\"-17.65\" font-family=\"Lato\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "('o0',)\n",
+      "('o0',)\n"
+     ]
+    }
+   ],
+   "source": [
+    "strat1_s = spot.split_separated_mealy(strat1)\n",
+    "display_inline(strat1, strat1_s)\n",
+    "print(spot.get_synthesis_output_aps(strat1))\n",
+    "print(spot.get_synthesis_output_aps(strat1_s))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "id": "cd06f9ab",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"182pt\" height=\"289pt\"\n",
+       " viewBox=\"0.00 0.00 181.99 289.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 285.5)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-285.5 177.99,-285.5 177.99,4 -4,4\"/>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"60\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"87\" cy=\"-176.75\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"87\" y=\"-173.05\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;10 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>6&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M65.86,-117.22C69.04,-126.05 73.08,-137.22 76.77,-147.44\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"78.15\" cy=\"-151.24\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"114\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"114\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M108.14,-117.22C104.95,-126.05 100.91,-137.22 97.22,-147.44\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"95.85\" cy=\"-151.24\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"87,-235.5 131.39,-270 42.6,-270 87,-235.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"87\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>10&#45;&gt;o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M87,-199.69C87,-208.03 87,-217.81 87,-227.29\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"87\" cy=\"-231.5\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"39,-46 0,-11.5 77.99,-11.5 39,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"39\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;6 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>2&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M43.97,-41.77C46.72,-51.58 50.17,-63.89 53.16,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.26\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;8 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M50.72,-35.72C62.4,-47.4 80.54,-65.55 94.41,-79.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"92.07,-82.02 101.61,-86.62 97.02,-77.07 92.07,-82.02\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"135,-46 96,-11.5 173.99,-11.5 135,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"135\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M123.28,-35.72C111.6,-47.4 93.45,-65.55 79.58,-79.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"76.98,-77.07 72.38,-86.62 81.93,-82.02 76.98,-77.07\"/>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>4&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M130.02,-41.77C127.27,-51.58 123.83,-63.89 120.83,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"119.73\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"182pt\" height=\"289pt\"\n",
+       " viewBox=\"0.00 0.00 181.99 289.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 285.5)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-285.5 177.99,-285.5 177.99,4 -4,4\"/>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"60\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"60\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"87\" cy=\"-176.75\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"87\" y=\"-173.05\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;10 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>6&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M65.86,-117.22C69.04,-126.05 73.08,-137.22 76.77,-147.44\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"78.15\" cy=\"-151.24\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"114\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"114\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M108.14,-117.22C104.95,-126.05 100.91,-137.22 97.22,-147.44\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"95.85\" cy=\"-151.24\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"87,-235.5 131.39,-270 42.6,-270 87,-235.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"87\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>10&#45;&gt;o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M87,-199.69C87,-208.03 87,-217.81 87,-227.29\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"87\" cy=\"-231.5\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"39,-46 0,-11.5 77.99,-11.5 39,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"39\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;6 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>2&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M43.97,-41.77C46.72,-51.58 50.17,-63.89 53.16,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.26\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;8 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M50.72,-35.72C62.4,-47.4 80.54,-65.55 94.41,-79.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"92.07,-82.02 101.61,-86.62 97.02,-77.07 92.07,-82.02\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"135,-46 96,-11.5 173.99,-11.5 135,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"135\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M123.28,-35.72C111.6,-47.4 93.45,-65.55 79.58,-79.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"76.98,-77.07 72.38,-86.62 81.93,-82.02 76.98,-77.07\"/>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>4&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M130.02,-41.77C127.27,-51.58 123.83,-63.89 120.83,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"119.73\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "display_inline(spot.mealy_machine_to_aig(strat1, \"isop\"), spot.mealy_machine_to_aig(strat1_s, \"isop\"))"
+   ]
   }
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   },
@@ -4079,7 +4439,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.9.2"
+   "version": "3.8.10"
   }
  },
  "nbformat": 4,