From 7cefe30d9774dec4703129727dc99abd733aa9b7 Mon Sep 17 00:00:00 2001
From: philipp <philipp@lrde.epita.fr>
Date: Fri, 7 Jan 2022 09:28:11 +0100
Subject: [PATCH] Fixes #495

Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.

* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here
* tests/python/_synthesis.ipynb: Testing
---
 spot/twaalgos/synthesis.cc    |  70 +++-
 spot/twaalgos/synthesis.hh    |  12 +-
 tests/python/_synthesis.ipynb | 764 +++++++++++++++++++++++++++++++++-
 3 files changed, 824 insertions(+), 22 deletions(-)

diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index 27e53b4d8..9025bb303 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -447,16 +447,28 @@ namespace spot
               const bdd& output_bdd, bool complete_env)
   {
     auto split = make_twa_graph(aut->get_dict());
+
+    auto [has_unsat, unsat_mark] = aut->acc().unsat_mark();
+
     split->copy_ap_of(aut);
-    split->copy_acceptance_of(aut);
     split->new_states(aut->num_states());
     split->set_init_state(aut->get_init_state_number());
-    split->set_named_prop<bdd>("synthesis-outputs", new bdd(output_bdd));
+    set_synthesis_outputs(split, output_bdd);
 
-    auto [is_unsat, unsat_mark] = aut->acc().unsat_mark();
-    if (!is_unsat && complete_env)
-      throw std::runtime_error("split_2step(): Cannot complete arena for "
-                               "env as there is no unsat mark.");
+    const auto use_color = has_unsat;
+    if (has_unsat)
+      split->copy_acceptance_of(aut);
+    else
+      {
+        if (complete_env)
+          {
+            split->set_co_buchi(); // Fin(0)
+            unsat_mark = acc_cond::mark_t({0});
+            has_unsat = true;
+          }
+        else
+          split->acc().set_acceptance(acc_cond::acc_code::t());
+      }
 
     bdd input_bdd = bddtrue;
     {
@@ -504,9 +516,10 @@ namespace spot
     unsigned sink_con = -1u;
     unsigned sink_env = -1u;
     auto get_sink_con_state = [&split, &sink_con, &sink_env,
-                               um = unsat_mark]
+                               um = unsat_mark, hu = has_unsat]
                               (bool create = true)
       {
+        assert(hu);
         if (SPOT_UNLIKELY((sink_con == -1u) && create))
           {
             sink_con = split->new_state();
@@ -518,7 +531,8 @@ namespace spot
       };
 
     // Loop over all states
-    for (unsigned src = 0; src < aut->num_states(); ++src)
+    const auto n_states = aut->num_states();
+    for (unsigned src = 0; src < n_states; ++src)
       {
         env_edge_hash.clear();
         e_cache.clear();
@@ -579,11 +593,16 @@ namespace spot
                 auto out = split->out(i);
                 if (std::equal(out.begin(), out.end(),
                                dests.begin(), dests.end(),
-                               [](const twa_graph::edge_storage_t& x,
+                               [uc = use_color]
+                               (const twa_graph::edge_storage_t& x,
                                   const e_info_t* y)
                                {
+                                 // If there is no unsat -> we do not care
+                                 // about color
+                                 // todo further optim?
                                  return   x.dst == y->dst
-                                          &&  x.acc == y->acc
+                                          &&  (!uc
+                                               || x.acc == y->acc)
                                           &&  x.cond.id() == y->econdout.id();
                                }))
                   {
@@ -592,6 +611,7 @@ namespace spot
                     if (it != env_edge_hash.end())
                       it->second.second |= one_letter;
                     else
+                      // Uncolored
                       env_edge_hash.emplace(i,
                           eeh_t(split->new_edge(src, i, bddtrue), one_letter));
                     break;
@@ -605,7 +625,8 @@ namespace spot
                 env_hash.emplace(h, d);
                 env_edge_hash.emplace(d, eeh_t(n_e, one_letter));
                 for (const auto &t: dests)
-                  split->new_edge(d, t->dst, t->econdout, t->acc);
+                  split->new_edge(d, t->dst, t->econdout,
+                                  use_color ? t->acc : acc_cond::mark_t({}));
               }
           } // letters
         // save locally stored condition
@@ -619,21 +640,34 @@ namespace spot
     // The named property
     // compute the owners
     // env is equal to false
-    std::vector<bool>* owner =
-        new std::vector<bool>(split->num_states(), false);
+    auto owner = std::vector<bool>(split->num_states(), false);
     // All "new" states belong to the player
-    std::fill(owner->begin()+aut->num_states(), owner->end(), true);
+    std::fill(owner.begin()+aut->num_states(), owner.end(), true);
     // Check if sinks have been created
     if (sink_env != -1u)
-      owner->at(sink_env) = false;
-    split->set_named_prop("state-player", owner);
-    split->set_named_prop("synthesis-outputs",
-                          new bdd(output_bdd));
+      owner.at(sink_env) = false;
+
+    // !use_color -> all words accepted
+    // complete_env && sink_env == -1u
+    // complet. for env demanded but already
+    // satisfied -> split is also all true
+    if (complete_env && sink_env == -1u && !use_color)
+      split->acc() = acc_cond::acc_code::t();
+
+    set_state_players(split, std::move(owner));
 
     // Done
     return split;
   }
 
+  twa_graph_ptr
+  split_2step(const const_twa_graph_ptr& aut, bool complete_env)
+  {
+    return split_2step(aut,
+                       get_synthesis_outputs(aut),
+                       complete_env);
+  }
+
   twa_graph_ptr
   unsplit_2step(const const_twa_graph_ptr& aut)
   {
diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh
index 44e6ca7dc..95590504c 100644
--- a/spot/twaalgos/synthesis.hh
+++ b/spot/twaalgos/synthesis.hh
@@ -52,11 +52,17 @@ namespace spot
   /// \param complete_env Whether the automaton should be complete for the
   ///                     environment, i.e. the player of inputs
   /// \note This function also computes the state players
-  /// \note If the automaton is to be completed for both env and player
-  ///       then egdes between the sinks will be added
+  /// \note If the automaton is to be completed, sink states will
+  ///       be added for both env and player if necessary
   SPOT_API twa_graph_ptr
   split_2step(const const_twa_graph_ptr& aut,
-              const bdd& output_bdd, bool complete_env);
+              const bdd& output_bdd, bool complete_env = true);
+
+  /// \ingroup synthesis
+  /// \brief Like split_2step but relying on the named property
+  /// 'synthesis-outputs'
+  SPOT_API twa_graph_ptr
+  split_2step(const const_twa_graph_ptr& aut, bool complete_env = true);
 
   /// \ingroup synthesis
   /// \brief the inverse of split_2step
diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb
index 1ed59760d..c99235f71 100644
--- a/tests/python/_synthesis.ipynb
+++ b/tests/python/_synthesis.ipynb
@@ -6,7 +6,7 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "import spot\n",
+    "import spot, buddy\n",
     "spot.setup()"
    ]
   },
@@ -389,6 +389,768 @@
     "assert(mmus3.equivalent_to(msep3))\n",
     "assert(mmus3.equivalent_to(mus3))"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Testing related to #495"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(0, t)\n"
+     ]
+    },
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"244pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 244.00 115.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 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 240,-111 240,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"115\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"107\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;1 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.12,-18C102.48,-18 159.32,-18 192.12,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"199.52,-18 192.52,-21.15 196.02,-18 192.52,-18 192.52,-18 192.52,-18 196.02,-18 192.52,-14.85 199.52,-18 199.52,-18\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">(!i &amp; !o) | (i &amp; o)</text>\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=\"M205.29,-31.29C199.86,-42.4 204.09,-54 218,-54 229.08,-54 234.02,-46.63 232.82,-38.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"230.71,-31.29 235.81,-37.03 231.76,-34.63 232.81,-37.97 232.81,-37.97 232.81,-37.97 231.76,-34.63 229.8,-38.91 230.71,-31.29 230.71,-31.29\"/>\n",
+       "<text text-anchor=\"middle\" x=\"218\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f7b0> >"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a = spot.translate(\"i<->o\", \"parity\")\n",
+    "print(a.acc())\n",
+    "a"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"206pt\" height=\"85pt\"\n",
+       " viewBox=\"0.00 0.00 205.50 85.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 81)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-81 201.5,-81 201.5,4 -4,4\"/>\n",
+       "<!-- I -->\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;1 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"175\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"175\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.01,-18C93.94,-18 127.11,-18 149.73,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"156.97,-18 149.97,-21.15 153.47,-18 149.97,-18 149.97,-18 149.97,-18 153.47,-18 149.97,-14.85 156.97,-18 156.97,-18\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-41 94.5,-60 105.5,-60 105.5,-41 94.5,-41\"/>\n",
+       "<text text-anchor=\"start\" x=\"96.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
+       "<text text-anchor=\"start\" x=\"109.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-41 120.5,-60 137.5,-60 137.5,-41 120.5,-41\"/>\n",
+       "<text text-anchor=\"start\" x=\"122.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-20 94.5,-39 105.5,-39 105.5,-20 94.5,-20\"/>\n",
+       "<text text-anchor=\"start\" x=\"99.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
+       "<text text-anchor=\"start\" x=\"109.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-20 120.5,-39 137.5,-39 137.5,-20 120.5,-20\"/>\n",
+       "<text text-anchor=\"start\" x=\"122.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\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=\"M165.19,-33.17C162.21,-43.66 165.48,-54 175,-54 182.29,-54 185.91,-47.94 185.87,-40.39\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"184.81,-33.17 188.95,-39.63 185.32,-36.63 185.83,-40.09 185.83,-40.09 185.83,-40.09 185.32,-36.63 182.71,-40.55 184.81,-33.17 184.81,-33.17\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"155,-55.5 155,-74.5 168,-74.5 168,-55.5 155,-55.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"157\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"172\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"183,-55.5 183,-74.5 196,-74.5 196,-55.5 183,-55.5\"/>\n",
+       "<text text-anchor=\"start\" x=\"185\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f7b0> >"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "spot.set_synthesis_outputs(a, buddy.bdd_ithvar(a.register_ap(\"o\")))\n",
+    "a"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(0, t)\n"
+     ]
+    },
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"363pt\" height=\"136pt\"\n",
+       " viewBox=\"0.00 0.00 363.00 136.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 132)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-132 359,-132 359,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"174.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"166.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;1 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-45C2.79,-45 17.15,-45 30.63,-45\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-45 30.94,-48.15 34.44,-45 30.94,-45 30.94,-45 30.94,-45 34.44,-45 30.94,-41.85 37.94,-45 37.94,-45\"/>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-90 117,-72 144,-54 171,-72 144,-90\"/>\n",
+       "<text text-anchor=\"middle\" x=\"144\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.58,-50.21C86.33,-54.21 104.15,-59.8 118.53,-64.32\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-66.44 117.66,-67.35 121.95,-65.39 118.61,-64.34 118.61,-64.34 118.61,-64.34 121.95,-65.39 119.55,-61.34 125.29,-66.44 125.29,-66.44\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-36 117,-18 144,0 171,-18 144,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"144\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;4 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.58,-39.79C86.33,-35.79 104.15,-30.2 118.53,-25.68\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-23.56 119.55,-28.66 121.95,-24.61 118.61,-25.66 118.61,-25.66 118.61,-25.66 121.95,-24.61 117.66,-22.65 125.29,-23.56 125.29,-23.56\"/>\n",
+       "<text text-anchor=\"start\" x=\"93.5\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"238\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"238\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"328,-63 301,-45 328,-27 355,-45 328,-63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"328\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M256.39,-45C267.02,-45 280.98,-45 293.68,-45\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"300.97,-45 293.97,-48.15 297.47,-45 293.97,-45 293.97,-45 293.97,-45 297.47,-45 293.97,-41.85 300.97,-45 300.97,-45\"/>\n",
+       "<text text-anchor=\"middle\" x=\"278.5\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">1</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=\"M314.15,-35.81C303.54,-29.35 288.02,-22.44 274,-26 269.14,-27.23 264.22,-29.3 259.67,-31.62\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"253.31,-35.13 257.91,-28.99 256.37,-33.44 259.44,-31.74 259.44,-31.74 259.44,-31.74 256.37,-33.44 260.96,-34.5 253.31,-35.13 253.31,-35.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"278.5\" y=\"-29.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;0 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M163.18,-66.67C177.62,-62.43 197.92,-56.47 213.58,-51.87\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-49.87 214.58,-54.86 217.05,-50.86 213.69,-51.84 213.69,-51.84 213.69,-51.84 217.05,-50.86 212.8,-48.82 220.41,-49.87 220.41,-49.87\"/>\n",
+       "<text text-anchor=\"start\" x=\"189\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;0 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>4&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M163.18,-23.33C177.62,-27.57 197.92,-33.53 213.58,-38.13\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-40.13 212.8,-41.18 217.05,-39.14 213.69,-38.16 213.69,-38.16 213.69,-38.16 217.05,-39.14 214.58,-35.14 220.41,-40.13 220.41,-40.13\"/>\n",
+       "<text text-anchor=\"start\" x=\"191\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f630> >"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a_s = spot.split_2step(a, True)\n",
+    "print(a.acc())\n",
+    "a_s"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"326pt\" height=\"108pt\"\n",
+       " viewBox=\"0.00 0.00 326.00 108.23\" 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 104.23)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-104.23 322,-104.23 322,4 -4,4\"/>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-38.53\" 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,-42.23C2.79,-42.23 17.15,-42.23 30.63,-42.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-42.23 30.94,-45.38 34.44,-42.23 30.94,-42.23 30.94,-42.23 30.94,-42.23 34.44,-42.23 30.94,-39.08 37.94,-42.23 37.94,-42.23\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"176\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"176\" y=\"-38.53\" 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=\"M72.74,-48.86C78.67,-51.03 85.54,-53.15 92,-54.23 113.04,-57.73 118.96,-57.73 140,-54.23 144.14,-53.54 148.45,-52.42 152.57,-51.13\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"159.26,-48.86 153.64,-54.09 155.94,-49.99 152.63,-51.11 152.63,-51.11 152.63,-51.11 155.94,-49.99 151.62,-48.13 159.26,-48.86 159.26,-48.86\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-79.23 94,-98.23 110,-98.23 110,-79.23 94,-79.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"96\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
+       "<text text-anchor=\"start\" x=\"114\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-79.23 125,-98.23 138,-98.23 138,-79.23 125,-79.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"127\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
+       "<text text-anchor=\"start\" x=\"108\" y=\"-64.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M165.21,-27.48C159.03,-19.57 150.28,-10.57 140,-6.23 120.35,2.08 111.65,2.08 92,-6.23 84.13,-9.55 77.16,-15.61 71.55,-21.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"66.79,-27.48 68.88,-20.1 69.04,-24.8 71.29,-22.12 71.29,-22.12 71.29,-22.12 69.04,-24.8 73.7,-24.14 66.79,-27.48 66.79,-27.48\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-29.23 94,-48.23 110,-48.23 110,-29.23 94,-29.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"96\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">i1</text>\n",
+       "<text text-anchor=\"start\" x=\"114\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-29.23 125,-48.23 138,-48.23 138,-29.23 125,-29.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"127\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"108\" y=\"-14.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"300\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"300\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M194.22,-42.23C215.2,-42.23 250.79,-42.23 274.59,-42.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"281.87,-42.23 274.87,-45.38 278.37,-42.23 274.87,-42.23 274.87,-42.23 274.87,-42.23 278.37,-42.23 274.87,-39.08 281.87,-42.23 281.87,-42.23\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"214,-65.23 214,-84.23 230,-84.23 230,-65.23 214,-65.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"216\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
+       "<text text-anchor=\"start\" x=\"234\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"245,-65.23 245,-84.23 262,-84.23 262,-65.23 245,-65.23\"/>\n",
+       "<text text-anchor=\"start\" x=\"247\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "<text text-anchor=\"start\" x=\"230\" y=\"-50.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee36703f60> >"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a = spot.make_twa_graph()\n",
+    "a.acc().set_acceptance(spot.acc_code.t())\n",
+    "i0 = buddy.bdd_ithvar(a.register_ap('i0'))\n",
+    "i1 = buddy.bdd_ithvar(a.register_ap('i1'))\n",
+    "o = buddy.bdd_ithvar(a.register_ap('o'))\n",
+    "tt = buddy.bddtrue\n",
+    "a0 = spot.mark_t([0])\n",
+    "a.new_states(3)\n",
+    "a.new_edge(0,1,i0&o,a0)\n",
+    "a.new_edge(1,0,i1,a0)\n",
+    "a.new_edge(1,2,i0&(buddy.bdd_not(o)),a0)\n",
+    "spot.set_synthesis_outputs(a, o)\n",
+    "a"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(0, t)\n"
+     ]
+    },
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"484pt\" height=\"198pt\"\n",
+       " viewBox=\"0.00 0.00 484.00 198.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 194)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-194 480,-194 480,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"235\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"227\" y=\"-159.8\" 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=\"-80\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-76.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=\"M1.15,-80C2.79,-80 17.15,-80 30.63,-80\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-80 30.94,-83.15 34.44,-80 30.94,-80 30.94,-80 30.94,-80 34.44,-80 30.94,-76.85 37.94,-80 37.94,-80\"/>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-98 122,-80 149,-62 176,-80 149,-98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"149\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.12,-80C85.52,-80 100.87,-80 114.63,-80\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"121.65,-80 114.65,-83.15 118.15,-80 114.65,-80 114.65,-80 114.65,-80 118.15,-80 114.65,-76.85 121.65,-80 121.65,-80\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-80\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"239\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;1 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M176.4,-80C188.2,-80 202.01,-80 213.57,-80\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"220.79,-80 213.79,-83.15 217.29,-80 213.79,-80 213.79,-80 213.79,-80 217.29,-80 213.79,-76.85 220.79,-80 220.79,-80\"/>\n",
+       "<text text-anchor=\"start\" x=\"194\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;4 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M255.26,-71.53C261.37,-68.19 268.49,-64.36 275,-61 297.28,-49.51 323.09,-37 340.97,-28.44\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"347.64,-25.26 342.68,-31.12 344.48,-26.77 341.32,-28.27 341.32,-28.27 341.32,-28.27 344.48,-26.77 339.97,-25.43 347.64,-25.26 347.64,-25.26\"/>\n",
+       "<text text-anchor=\"start\" x=\"275\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; i1</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-98 337,-80 364,-62 391,-80 364,-98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;5 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M257.1,-80C275.77,-80 306.11,-80 329.55,-80\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"336.58,-80 329.58,-83.15 333.08,-80 329.58,-80 329.58,-80 329.58,-80 333.08,-80 329.58,-76.85 336.58,-80 336.58,-80\"/>\n",
+       "<text text-anchor=\"start\" x=\"275\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; !i1</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-152 337,-134 364,-116 391,-134 364,-152\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;6 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M255.65,-87.24C261.68,-90.01 268.65,-93.18 275,-96 297.15,-105.84 322.59,-116.79 340.39,-124.39\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"347.06,-127.24 339.38,-127.39 343.84,-125.86 340.62,-124.49 340.62,-124.49 340.62,-124.49 343.84,-125.86 341.86,-121.59 347.06,-127.24 347.06,-127.24\"/>\n",
+       "<text text-anchor=\"start\" x=\"277\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; i1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;0 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>4&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M338.99,-19.5C295.19,-22.67 199.65,-31.6 122,-53 107.19,-57.08 91.25,-63.67 78.86,-69.31\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"72.37,-72.33 77.39,-66.52 75.55,-70.85 78.72,-69.38 78.72,-69.38 78.72,-69.38 75.55,-70.85 80.05,-72.23 72.37,-72.33 72.37,-72.33\"/>\n",
+       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"458\" cy=\"-107\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"458\" y=\"-103.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;2 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>5&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M385.52,-83.87C396.46,-86.14 410.08,-89.28 422,-93 426.08,-94.27 430.36,-95.81 434.47,-97.39\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"441.16,-100.05 433.49,-100.39 437.91,-98.76 434.66,-97.46 434.66,-97.46 434.66,-97.46 437.91,-98.76 435.82,-94.54 441.16,-100.05 441.16,-100.05\"/>\n",
+       "<text text-anchor=\"start\" x=\"409\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;0 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>6&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M338.67,-135.14C320.98,-135.69 296.46,-135.88 275,-134 206.21,-127.98 189.42,-121.91 122,-107 108.53,-104.02 104.82,-104.11 92,-99 87.43,-97.18 82.69,-94.9 78.23,-92.56\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"71.95,-89.13 79.61,-89.72 75.03,-90.81 78.1,-92.49 78.1,-92.49 78.1,-92.49 75.03,-90.81 76.59,-95.25 71.95,-89.13 71.95,-89.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;2 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>6&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M383.18,-128.67C397.62,-124.43 417.92,-118.47 433.58,-113.87\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"440.41,-111.87 434.58,-116.86 437.05,-112.86 433.69,-113.84 433.69,-113.84 433.69,-113.84 437.05,-112.86 432.8,-110.82 440.41,-111.87 440.41,-111.87\"/>\n",
+       "<text text-anchor=\"start\" x=\"409\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f930> >"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a_snc = spot.split_2step(a, False)\n",
+    "print(a_snc.acc())\n",
+    "a_snc"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(1, Fin(0))\n"
+     ]
+    },
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"706pt\" height=\"269pt\"\n",
+       " viewBox=\"0.00 0.00 706.00 269.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 265)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-265 702,-265 702,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"327.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"350.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"366.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"317.5\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">[co&#45;Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-59\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-55.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=\"M1.15,-59C2.79,-59 17.15,-59 30.63,-59\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-59 30.94,-62.15 34.44,-59 30.94,-59 30.94,-59 30.94,-59 34.44,-59 30.94,-55.85 37.94,-59 37.94,-59\"/>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"583,-190 556,-172 583,-154 610,-172 583,-190\"/>\n",
+       "<text text-anchor=\"middle\" x=\"583\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M59.28,-76.91C65.47,-116.91 86.48,-210 148,-210 148,-210 148,-210 494,-210 519.79,-210 546.6,-196.08 563.75,-185.08\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"569.61,-181.2 565.52,-187.69 566.69,-183.13 563.78,-185.07 563.78,-185.07 563.78,-185.07 566.69,-183.13 562.04,-182.44 569.61,-181.2 569.61,-181.2\"/>\n",
+       "<text text-anchor=\"start\" x=\"289\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">!i0</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-108 122,-90 149,-72 176,-90 149,-108\"/>\n",
+       "<text text-anchor=\"middle\" x=\"149\" y=\"-86.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.27,-64.54C87.28,-69.31 107.7,-76.27 123.65,-81.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"130.63,-84.08 122.99,-84.81 127.32,-82.95 124.01,-81.83 124.01,-81.83 124.01,-81.83 127.32,-82.95 125.02,-78.84 130.63,-84.08 130.63,-84.08\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-77.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"680\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"680\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M605.09,-175.35C616.59,-176.77 631.07,-177.92 644,-177 647.49,-176.75 651.16,-176.37 654.76,-175.92\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"661.96,-174.93 655.46,-179 658.49,-175.4 655.03,-175.88 655.03,-175.88 655.03,-175.88 658.49,-175.4 654.6,-172.76 661.96,-174.93 661.96,-174.93\"/>\n",
+       "<text text-anchor=\"start\" x=\"631.5\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"628\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-104\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"239\" y=\"-100.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;1 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>5&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M171.3,-93.39C184.18,-95.44 200.62,-98.05 213.96,-100.18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"221.01,-101.3 213.61,-103.31 217.56,-100.75 214.1,-100.2 214.1,-100.2 214.1,-100.2 217.56,-100.75 214.6,-97.09 221.01,-101.3 221.01,-101.3\"/>\n",
+       "<text text-anchor=\"start\" x=\"194\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M249.03,-119.4C255.17,-128.4 264.14,-139.12 275,-145 321.53,-170.19 479.42,-172.57 548.82,-172.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"556.04,-172.32 549.06,-175.5 552.54,-172.34 549.04,-172.35 549.04,-172.35 549.04,-172.35 552.54,-172.34 549.03,-169.2 556.04,-172.32 556.04,-172.32\"/>\n",
+       "<text text-anchor=\"start\" x=\"409\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; !i1</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-90 337,-72 364,-54 391,-72 364,-90\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;6 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M256.59,-99.68C277.36,-94.28 313.15,-84.97 337.44,-78.65\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"344.26,-76.87 338.28,-81.69 340.88,-77.76 337.49,-78.64 337.49,-78.64 337.49,-78.64 340.88,-77.76 336.7,-75.59 344.26,-76.87 344.26,-76.87\"/>\n",
+       "<text text-anchor=\"start\" x=\"275\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; i1</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-144 337,-126 364,-108 391,-126 364,-144\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;7 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>1&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M255.24,-112.42C261.23,-115.33 268.26,-118.29 275,-120 293.02,-124.57 313.74,-126.16 330.55,-126.56\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"337.97,-126.67 330.92,-129.71 334.47,-126.62 330.97,-126.57 330.97,-126.57 330.97,-126.57 334.47,-126.62 331.02,-123.42 337.97,-126.67 337.97,-126.67\"/>\n",
+       "<text text-anchor=\"start\" x=\"275\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; !i1</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M250.63,-89.89C257.09,-81.94 265.84,-72.19 275,-65 295.27,-49.1 321.69,-35.81 340.28,-27.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"346.74,-24.62 341.6,-30.32 343.54,-26.03 340.33,-27.44 340.33,-27.44 340.33,-27.44 343.54,-26.03 339.06,-24.56 346.74,-24.62 346.74,-24.62\"/>\n",
+       "<text text-anchor=\"start\" x=\"277\" y=\"-68.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; i1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;0 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>6&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M350.67,-62.68C342.25,-56.92 330.55,-50.05 319,-47 233.55,-24.42 127.04,-42.98 80.55,-53.28\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"73.61,-54.85 79.74,-50.23 77.03,-54.08 80.44,-53.3 80.44,-53.3 80.44,-53.3 77.03,-54.08 81.14,-56.37 73.61,-54.85 73.61,-54.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"493\" cy=\"-126\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"493\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;2 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>7&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M391.01,-126C413.57,-126 445.96,-126 467.93,-126\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"474.95,-126 467.95,-129.15 471.45,-126 467.95,-126 467.95,-126 467.95,-126 471.45,-126 467.95,-122.85 474.95,-126 474.95,-126\"/>\n",
+       "<text text-anchor=\"start\" x=\"426.5\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;0 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>8&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M339.67,-16.08C306.97,-13.79 245.73,-10.98 194,-17 161.34,-20.8 153.63,-25.01 122,-34 108.48,-37.84 105.14,-39.01 92,-44 87.96,-45.54 83.71,-47.26 79.6,-48.99\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"72.92,-51.85 78.11,-46.2 76.13,-50.47 79.35,-49.1 79.35,-49.1 79.35,-49.1 76.13,-50.47 80.59,-51.99 72.92,-51.85 72.92,-51.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-20.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;2 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>8&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M376.72,-27.97C398.76,-46.71 446.53,-87.34 473.14,-109.96\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"478.8,-114.77 471.42,-112.64 476.13,-112.51 473.47,-110.24 473.47,-110.24 473.47,-110.24 476.13,-112.51 475.51,-107.84 478.8,-114.77 478.8,-114.77\"/>\n",
+       "<text text-anchor=\"start\" x=\"426.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M510.25,-131.34C518.71,-134.35 529.12,-138.42 538,-143 546.64,-147.45 555.69,-153.2 563.32,-158.41\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"569.35,-162.61 561.81,-161.2 566.48,-160.61 563.61,-158.61 563.61,-158.61 563.61,-158.61 566.48,-160.61 565.41,-156.03 569.35,-162.61 569.35,-162.61\"/>\n",
+       "<text text-anchor=\"middle\" x=\"533.5\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;3 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>4&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M667.4,-158.86C661.16,-152.78 652.91,-146.21 644,-143 637.31,-140.59 634.81,-140.96 628,-143 618.42,-145.87 608.99,-151.59 601.34,-157.19\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"595.36,-161.8 598.98,-155.03 598.13,-159.66 600.9,-157.52 600.9,-157.52 600.9,-157.52 598.13,-159.66 602.82,-160.02 595.36,-161.8 595.36,-161.8\"/>\n",
+       "<text text-anchor=\"start\" x=\"631.5\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"628\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716fa20> >"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a_s = spot.split_2step(a, True)\n",
+    "print(a_s.acc())\n",
+    "a_s"
+   ]
   }
  ],
  "metadata": {