diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc
index 17f94a7e4..faf29b2ba 100644
--- a/spot/twaalgos/game.cc
+++ b/spot/twaalgos/game.cc
@@ -149,73 +149,133 @@ namespace spot
     {
     public:
 
-      bool solve(const twa_graph_ptr& arena)
+      bool solve(const twa_graph_ptr& arena, bool solve_globally)
       {
         // todo check if reordering states according to scc is worth it
         set_up(arena);
         // Start recursive zielonka in a bottom-up fashion on each scc
         subgame_info_t subgame_info;
-        for (c_scc_idx_ = 0; c_scc_idx_ < info_->scc_count(); ++c_scc_idx_)
+        while (true)
           {
-            // Testing
-            // Make sure that every state that has a winner also
-            // belongs to a subgame
-            assert([&]()
-                    {
-                      for (unsigned i = 0; i < arena_->num_states(); ++i)
-                        if (w_.has_winner_[i]
-                            && (subgame_[i] == unseen_mark))
-                          return false;
-                        return true;
-                    }());
-            // Useless SCCs are winning for player 0.
-            if (!info_->is_useful_scc(c_scc_idx_))
+            // If we solve globally,
+            auto maybe_useful = [&](unsigned scc_idx){
+              if (info_->is_useful_scc(scc_idx))
+                return true;
+              if (!solve_globally)
+                return false;
+              // Check if we have an out-edge to a winning state
+              // in another scc
+              return std::any_of(
+                  info_->states_of(scc_idx).begin(),
+                  info_->states_of(scc_idx).end(),
+                  [&](unsigned s){
+                    return std::any_of(
+                                arena->out(s).begin(),
+                                arena->out(s).end(),
+                                [&](const auto& e){
+                                  assert ((subgame_[e.dst] == unseen_mark)
+                                          || (info_->scc_of(e.dst) != scc_idx));
+                                  return (info_->scc_of(e.dst) != scc_idx)
+                                          && w_.winner(e.dst);
+                                });
+                  });
+            };
+
+            for (c_scc_idx_ = 0; c_scc_idx_ < info_->scc_count(); ++c_scc_idx_)
               {
-                // This scc also gets its own subgame
-                ++rd_;
-                for (unsigned v: c_states())
-                  {
-                    subgame_[v] = rd_;
-                    w_.set(v, false);
-                    // The strategy for player 0 is to take the first
-                    // available edge.
-                    if ((*owner_ptr_)[v] == false)
-                      for (const auto &e : arena_->out(v))
+                // Testing
+                // Make sure that every state that has a winner also
+                // belongs to a subgame
+                assert([&]()
                         {
-                          s_[v] = arena_->edge_number(e);
-                          break;
-                        }
-                  }
-                continue;
-              }
-            // Convert transitions leaving edges to self-loops
-            // and check if trivially solvable
-            subgame_info = fix_scc();
-            // If empty, the scc was trivially solved
-            if (!subgame_info.is_empty)
-              {
-                // Check for special cases
-                if (subgame_info.is_one_parity)
-                  one_par_subgame_solver(subgame_info, max_abs_par_);
-                else
+                          for (unsigned i = 0; i < arena_->num_states(); ++i)
+                            if (w_.has_winner_[i]
+                                && (subgame_[i] == unseen_mark))
+                              return false;
+                            return true;
+                        }());
+                // Useless SCCs are winning for player 0.
+                if (!maybe_useful(c_scc_idx_))
                   {
-                    // "Regular" solver
-                    max_abs_par_ = *subgame_info.all_parities.begin();
-                    w_stack_.emplace_back(0, 0,
-                                          min_par_graph_, max_abs_par_);
-                    zielonka();
+                    // This scc also gets its own subgame
+                    ++rd_;
+                    for (unsigned v: c_states())
+                      {
+                        subgame_[v] = rd_;
+                        w_.set(v, false);
+                        // The strategy for player 0 is to take the first
+                        // available edge.
+                        if ((*owner_ptr_)[v] == false)
+                          for (const auto &e : arena_->out(v))
+                            {
+                              s_[v] = arena_->edge_number(e);
+                              break;
+                            }
+                      }
+                    continue;
+                  }
+                // Convert transitions leaving edges to self-loops
+                // and check if trivially solvable
+                subgame_info = fix_scc();
+                // If empty, the scc was trivially solved
+                if (!subgame_info.is_empty)
+                  {
+                    // Check for special cases
+                    if (subgame_info.is_one_parity)
+                      one_par_subgame_solver(subgame_info, max_abs_par_);
+                    else
+                      {
+                        // "Regular" solver
+                        max_abs_par_ = *subgame_info.all_parities.begin();
+                        w_stack_.emplace_back(0, 0,
+                                              min_par_graph_, max_abs_par_);
+                        zielonka();
+                      }
                   }
               }
+            if (!solve_globally)
+              break;
+
+            // Update the scc_info and continue
+            unsigned new_init
+              = std::distance(subgame_.begin(),
+                              std::find(subgame_.begin(), subgame_.end(),
+                                        unseen_mark));
+            if (new_init == arena->num_states())
+              break; // All states have been solved
+            // Compute new sccs
+            scc_info::edge_filter ef
+              = [](const twa_graph::edge_storage_t&,
+                   unsigned dst, void* subgame){
+                const auto& sg = *static_cast<std::vector<unsigned>*>(subgame);
+                return sg[dst] == unseen_mark ?
+                          scc_info::edge_filter_choice::keep :
+                          scc_info::edge_filter_choice::ignore;
+              };
+            info_ = std::make_unique<scc_info>(arena, new_init, ef, &subgame_);
           }
-        // Every state needs a winner
-        assert(std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(),
-                           [](bool b)
-                           { return b; }));
+        // Every state needs a winner (solve_globally)
+        // Or only those reachable
+        assert((solve_globally
+                && std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(),
+                               [](bool b) { return b; }))
+                || (!solve_globally
+                    && [&](){
+                         for (unsigned s = 0; s < arena->num_states(); ++s)
+                            {
+                              if ((info_->scc_of(s) != -1u)
+                                  && !w_.has_winner_.at(s))
+                                return false;
+                            }
+                          return true;
+                        }()));
         // Only the states owned by the winner need a strategy
         assert([&]()
                {
                   for (unsigned v = 0; v < arena_->num_states(); ++v)
                     {
+                      if (!solve_globally && (info_->scc_of(v) == -1u))
+                        continue;
                       if (((*owner_ptr_)[v] == w_.winner(v))
                           && ((s_[v] <= 0) || (s_[v] > arena_->num_edges())))
                         return false;
@@ -817,10 +877,10 @@ namespace spot
   } // anonymous
 
 
-  bool solve_parity_game(const twa_graph_ptr& arena)
+  bool solve_parity_game(const twa_graph_ptr& arena, bool solve_globally)
   {
     parity_game pg;
-    return pg.solve(arena);
+    return pg.solve(arena, solve_globally);
   }
 
   bool solve_game(const twa_graph_ptr& arena)
diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh
index dbaccce75..d4937e46c 100644
--- a/spot/twaalgos/game.hh
+++ b/spot/twaalgos/game.hh
@@ -70,13 +70,19 @@ namespace spot
   /// This computes the winning strategy and winning region using
   /// Zielonka's recursive algorithm.  \cite zielonka.98.tcs
   ///
+  /// By default only a 'local' strategy is computed:
+  /// Only the part of the arena reachable from the init state is considered.
+  /// If you want to compute a strategy for ALL states, set
+  /// \a solve_globally to true
+  ///
   /// Also includes some inspiration from Oink.
   /// \cite vandijk.18.tacas
   ///
   /// Returns the player winning in the initial state, and sets
   /// the state-winner and strategy named properties.
   SPOT_API
-  bool solve_parity_game(const twa_graph_ptr& arena);
+  bool solve_parity_game(const twa_graph_ptr& arena,
+                         bool solve_globally = false);
 
   /// \ingroup games
   /// \brief Solve a safety game.
diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb
index a6168b07e..9ec8bb76e 100644
--- a/tests/python/games.ipynb
+++ b/tests/python/games.ipynb
@@ -897,7 +897,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7feee9b0ebb0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcbe436f840> >"
       ]
      },
      "execution_count": 8,
@@ -1224,7 +1224,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fef001c87b0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcbe436e9a0> >"
       ]
      },
      "execution_count": 11,
@@ -1663,11 +1663,1143 @@
    ]
   },
   {
-   "cell_type": "code",
-   "execution_count": null,
+   "cell_type": "markdown",
    "metadata": {},
-   "outputs": [],
-   "source": []
+   "source": [
+    "# Global vs local solver\n",
+    "\n",
+    "The parity game solver now supports \"local\" and global solutions.\n",
+    "\n",
+    "- \"Local\" solutions are the ones computed so far. A strategy is only computed for the part of the automaton that is rachable from the initial state\n",
+    "- Global solutions can now be obtained by setting the argument \"solve_globally\" to true. In this case a strategy will be computed even for states not reachable in the original automaton.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "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=\"334pt\" height=\"360pt\"\n",
+       " viewBox=\"0.00 0.00 334.23 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7092198581560284 0.7092198581560284) rotate(0) translate(4 502)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-502 465.79,-502 465.79,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"210.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"231.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"247.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"209.39\" y=\"-469.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-98\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-94.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=\"M31.41,-112.99C33.49,-112.68 79.37,-105.92 108.79,-101.58\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"115.88,-100.54 109.41,-104.68 112.41,-101.05 108.95,-101.56 108.95,-101.56 108.95,-101.56 112.41,-101.05 108.49,-98.44 115.88,-100.54 115.88,-100.54\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-170 207.93,-152 230.89,-134 253.85,-152 230.89,-170\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-148.3\" 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=\"M150.34,-106.68C166.84,-116.08 193.18,-131.09 210.99,-141.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-144.73 209.49,-144 214.09,-143 211.05,-141.27 211.05,-141.27 211.05,-141.27 214.09,-143 212.61,-138.53 217.13,-144.73 217.13,-144.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-116 207.93,-98 230.89,-80 253.85,-98 230.89,-116\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-94.3\" 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=\"M152.5,-98C165.82,-98 184.51,-98 200.18,-98\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-98 200.6,-101.15 204.1,-98 200.6,-98 200.6,-98 200.6,-98 204.1,-98 200.6,-94.85 207.6,-98 207.6,-98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"334.67\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</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=\"M246.04,-145.46C263.02,-137.62 291.69,-124.39 311.59,-115.2\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"317.97,-112.25 312.94,-118.04 314.79,-113.72 311.62,-115.19 311.62,-115.19 311.62,-115.19 314.79,-113.72 310.3,-112.33 317.97,-112.25 317.97,-112.25\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-132.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M252.49,-99.42C268.96,-100.55 292.08,-102.14 309.44,-103.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"316.49,-103.82 309.29,-106.48 312.99,-103.58 309.5,-103.34 309.5,-103.34 309.5,-103.34 312.99,-103.58 309.72,-100.2 316.49,-103.82 316.49,-103.82\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"431.45,-92 408.5,-74 431.45,-56 454.41,-74 431.45,-92\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-70.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M352.18,-99.6C367.59,-94.56 390.71,-87 407.83,-81.4\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"414.76,-79.13 409.09,-84.3 411.44,-80.22 408.11,-81.31 408.11,-81.31 408.11,-81.31 411.44,-80.22 407.13,-78.31 414.76,-79.13 414.76,-79.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\">1</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=\"M412.27,-70.94C373.02,-64.94 277.67,-53.67 200.56,-71 185.48,-74.39 169.43,-80.96 157,-86.77\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"150.49,-89.9 155.44,-84.03 153.65,-88.38 156.8,-86.87 156.8,-86.87 156.8,-86.87 153.65,-88.38 158.16,-89.71 150.49,-89.9 150.49,-89.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-80.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"30.33,-63 7.37,-45 30.33,-27 53.29,-45 30.33,-63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M44.64,-51.93C61.66,-60.79 91.34,-76.25 111.59,-86.79\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"117.81,-90.03 110.15,-89.59 114.71,-88.41 111.6,-86.8 111.6,-86.8 111.6,-86.8 114.71,-88.41 113.06,-84 117.81,-90.03 117.81,-90.03\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M48.14,-40.54C64.89,-36.1 90.75,-29.24 109.54,-24.25\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"116.62,-22.38 110.66,-27.22 113.24,-23.27 109.85,-24.17 109.85,-24.17 109.85,-24.17 113.24,-23.27 109.04,-21.13 116.62,-22.38 116.62,-22.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;5 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>6&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M117.05,-11.84C106.03,-8.52 91.19,-5.87 78.66,-10 66.52,-14 54.94,-22.45 46.27,-30.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"40.77,-35.1 43.79,-28.05 43.35,-32.74 45.92,-30.37 45.92,-30.37 45.92,-30.37 43.35,-32.74 48.05,-32.69 40.77,-35.1 40.77,-35.1\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-13.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-244\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-316 207.93,-298 230.89,-280 253.85,-298 230.89,-316\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-294.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M150.34,-252.68C166.84,-262.08 193.18,-277.09 210.99,-287.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-290.73 209.49,-290 214.09,-289 211.05,-287.27 211.05,-287.27 211.05,-287.27 214.09,-289 212.61,-284.53 217.13,-290.73 217.13,-290.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-274.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>9</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-262 207.93,-244 230.89,-226 253.85,-244 230.89,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;9 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>7&#45;&gt;9</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M152.5,-244C165.82,-244 184.51,-244 200.18,-244\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-244 200.6,-247.15 204.1,-244 200.6,-244 200.6,-244 200.6,-244 204.1,-244 200.6,-240.85 207.6,-244 207.6,-244\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"334.67\" cy=\"-251\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-247.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M246.04,-291.46C262.34,-283.94 289.39,-271.45 309.13,-262.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"315.52,-259.38 310.49,-265.18 312.34,-260.85 309.17,-262.32 309.17,-262.32 309.17,-262.32 312.34,-260.85 307.85,-259.46 315.52,-259.38 315.52,-259.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9&#45;&gt;10 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>9&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M252.49,-245.42C267.8,-246.47 288.87,-247.92 305.71,-249.08\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"313.11,-249.59 305.91,-252.25 309.62,-249.35 306.12,-249.11 306.12,-249.11 306.12,-249.11 309.62,-249.35 306.34,-245.96 313.11,-249.59 313.11,-249.59\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11 -->\n",
+       "<g id=\"node13\" class=\"node\">\n",
+       "<title>11</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"431.45,-233 401.29,-215 431.45,-197 461.62,-215 431.45,-233\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-211.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;11 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>10&#45;&gt;11</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M354.4,-243.89C369.13,-238.29 389.77,-230.45 405.84,-224.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"412.41,-221.85 406.98,-227.28 409.14,-223.1 405.87,-224.34 405.87,-224.34 405.87,-224.34 409.14,-223.1 404.75,-221.39 412.41,-221.85 412.41,-221.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-239.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;7 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>11&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M406.24,-211.9C363.91,-207.22 273.97,-200.5 200.56,-217 185.48,-220.39 169.43,-226.96 157,-232.77\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"150.49,-235.9 155.44,-230.03 153.65,-234.38 156.8,-232.87 156.8,-232.87 156.8,-232.87 153.65,-234.38 158.16,-235.71 150.49,-235.9 150.49,-235.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g id=\"node14\" class=\"node\">\n",
+       "<title>12</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"30.33,-224 0.17,-206 30.33,-188 60.5,-206 30.33,-224\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>12&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.53,-212.79C66.49,-219.13 91.85,-228.6 110.19,-235.44\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"117.08,-238.02 109.42,-238.52 113.8,-236.79 110.53,-235.57 110.53,-235.57 110.53,-235.57 113.8,-236.79 111.63,-232.62 117.08,-238.02 117.08,-238.02\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13 -->\n",
+       "<g id=\"node15\" class=\"node\">\n",
+       "<title>13</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-179\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">13</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;13 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>12&#45;&gt;13</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M51.93,-200.54C67.58,-196.38 89.25,-190.64 106.26,-186.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"113.24,-184.27 107.28,-189.11 109.86,-185.17 106.47,-186.07 106.47,-186.07 106.47,-186.07 109.86,-185.17 105.67,-183.02 113.24,-184.27 113.24,-184.27\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;12 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>13&#45;&gt;12</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M114.35,-171.49C103.69,-168.3 90.19,-166.11 78.66,-170 66.9,-173.97 55.74,-182.15 47.22,-189.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"41.77,-194.79 44.74,-187.72 44.33,-192.41 46.89,-190.02 46.89,-190.02 46.89,-190.02 44.33,-192.41 49.04,-192.33 41.77,-194.79 41.77,-194.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g id=\"node16\" class=\"node\">\n",
+       "<title>14</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">14</text>\n",
+       "</g>\n",
+       "<!-- 15 -->\n",
+       "<g id=\"node17\" class=\"node\">\n",
+       "<title>15</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-462 200.73,-444 230.89,-426 261.06,-444 230.89,-462\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-440.3\" font-family=\"Lato\" font-size=\"14.00\">15</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;15 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>14&#45;&gt;15</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M152.5,-399.9C168.25,-408.88 191.53,-422.14 208.44,-431.78\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"214.81,-435.4 207.16,-434.68 211.76,-433.67 208.72,-431.94 208.72,-431.94 208.72,-431.94 211.76,-433.67 210.28,-429.2 214.81,-435.4 214.81,-435.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-420.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16 -->\n",
+       "<g id=\"node18\" class=\"node\">\n",
+       "<title>16</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"230.89,-408 200.73,-390 230.89,-372 261.06,-390 230.89,-408\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">16</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;16 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>14&#45;&gt;16</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M155.68,-390C166.6,-390 180.36,-390 193.05,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"200.37,-390 193.37,-393.15 196.87,-390 193.37,-390 193.37,-390 193.37,-390 196.87,-390 193.37,-386.85 200.37,-390 200.37,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 17 -->\n",
+       "<g id=\"node19\" class=\"node\">\n",
+       "<title>17</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"334.67\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">17</text>\n",
+       "</g>\n",
+       "<!-- 15&#45;&gt;17 -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>15&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M247.35,-435.8C263.94,-427 290.5,-412.91 309.78,-402.68\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"316.01,-399.37 311.31,-405.43 312.92,-401.01 309.83,-402.65 309.83,-402.65 309.83,-402.65 312.92,-401.01 308.35,-399.87 316.01,-399.37 316.01,-399.37\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-421.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16&#45;&gt;17 -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>16&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M261.06,-390C275.27,-390 292.25,-390 306.22,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"313.22,-390 306.22,-393.15 309.72,-390 306.22,-390 306.22,-390 306.22,-390 309.72,-390 306.22,-386.85 313.22,-390 313.22,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18 -->\n",
+       "<g id=\"node20\" class=\"node\">\n",
+       "<title>18</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"431.45,-378 401.29,-360 431.45,-342 461.62,-360 431.45,-378\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-356.3\" font-family=\"Lato\" font-size=\"14.00\">18</text>\n",
+       "</g>\n",
+       "<!-- 17&#45;&gt;18 -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>17&#45;&gt;18</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M355.31,-383.78C369.51,-379.29 388.85,-373.17 404.34,-368.26\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"411.16,-366.11 405.44,-371.22 407.83,-367.16 404.49,-368.22 404.49,-368.22 404.49,-368.22 407.83,-367.16 403.54,-365.21 411.16,-366.11 411.16,-366.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-380.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18&#45;&gt;14 -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>18&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M405.63,-357.3C363.12,-353.35 273.88,-347.97 200.56,-363 186.24,-365.94 171.09,-371.97 158.98,-377.6\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"152.59,-380.66 157.54,-374.79 155.75,-379.15 158.9,-377.63 158.9,-377.63 158.9,-377.63 155.75,-379.15 160.26,-380.48 152.59,-380.66 152.59,-380.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-356.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 19 -->\n",
+       "<g id=\"node21\" class=\"node\">\n",
+       "<title>19</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"30.33,-370 0.17,-352 30.33,-334 60.5,-352 30.33,-370\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-348.3\" font-family=\"Lato\" font-size=\"14.00\">19</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;14 -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>19&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.53,-358.79C65.58,-364.79 89.16,-373.59 107.18,-380.32\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"114.04,-382.88 106.38,-383.38 110.76,-381.65 107.48,-380.43 107.48,-380.43 107.48,-380.43 110.76,-381.65 108.58,-377.48 114.04,-382.88 114.04,-382.88\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-378.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20 -->\n",
+       "<g id=\"node22\" class=\"node\">\n",
+       "<title>20</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"134.11\" cy=\"-318\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-314.3\" font-family=\"Lato\" font-size=\"14.00\">20</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;20 -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>19&#45;&gt;20</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M50.48,-345.6C66.44,-340.27 89.34,-332.62 106.99,-326.73\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"113.71,-324.48 108.07,-329.69 110.39,-325.59 107.07,-326.7 107.07,-326.7 107.07,-326.7 110.39,-325.59 106.07,-323.71 113.71,-324.48 113.71,-324.48\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20&#45;&gt;19 -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>20&#45;&gt;19</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M118.61,-305.5C107.54,-297.55 91.98,-289.82 78.66,-296 62.59,-303.46 50,-319.37 41.86,-332.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"38.22,-338.41 39.11,-330.78 40.02,-335.4 41.82,-332.4 41.82,-332.4 41.82,-332.4 40.02,-335.4 44.52,-334.02 38.22,-338.41 38.22,-338.41\"/>\n",
+       "<text text-anchor=\"start\" x=\"82.16\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"78.66\" y=\"-299.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 0x7fcbe4382370> >"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "arena = spot.make_twa_graph()\n",
+    "\n",
+    "arena.new_states(3*7)\n",
+    "arena.set_buchi()\n",
+    "\n",
+    "edges = [(0,1), (0,2), (1,3), (2,3), (3,4), (4,0), (5,0), (5,6), (6,5)]\n",
+    "\n",
+    "for src, dst in edges:\n",
+    "    arena.new_edge(src, dst, bddtrue, [0] if src == 4 else [])\n",
+    "    arena.new_edge(src + 7, dst + 7, bddtrue, [0] if src == 4 else [])\n",
+    "    arena.new_edge(src + 14, dst + 14, bddtrue, [0] if src == 6 else [])\n",
+    "\n",
+    "arena.set_state_players(3*[False, True, True, False, True, True, False])\n",
+    "arena"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(0, 7, 10, 0, 16, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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=\"334pt\" height=\"360pt\"\n",
+       " viewBox=\"0.00 0.00 334.23 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7092198581560284 0.7092198581560284) rotate(0) translate(4 502)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-502 465.79,-502 465.79,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"210.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"231.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"247.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"209.39\" y=\"-469.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-98\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-94.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=\"M31.41,-112.99C33.49,-112.68 79.37,-105.92 108.79,-101.58\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"115.88,-100.54 109.41,-104.68 112.41,-101.05 108.95,-101.56 108.95,-101.56 108.95,-101.56 112.41,-101.05 108.49,-98.44 115.88,-100.54 115.88,-100.54\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-170 207.93,-152 230.89,-134 253.85,-152 230.89,-170\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-148.3\" 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=\"M150.34,-106.68C166.84,-116.08 193.18,-131.09 210.99,-141.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-144.73 209.49,-144 214.09,-143 211.05,-141.27 211.05,-141.27 211.05,-141.27 214.09,-143 212.61,-138.53 217.13,-144.73 217.13,-144.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-116 207.93,-98 230.89,-80 253.85,-98 230.89,-116\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-94.3\" 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=\"M152.5,-98C165.82,-98 184.51,-98 200.18,-98\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-98 200.6,-101.15 204.1,-98 200.6,-98 200.6,-98 200.6,-98 204.1,-98 200.6,-94.85 207.6,-98 207.6,-98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</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=\"#33a02c\" stroke-width=\"2\" d=\"M246.04,-145.46C263.02,-137.62 291.69,-124.39 311.59,-115.2\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"317.97,-112.25 312.94,-118.04 315,-114.17 311.83,-115.64 311.62,-115.19 311.41,-114.73 314.58,-113.26 310.3,-112.33 317.97,-112.25 317.97,-112.25\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-132.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M252.49,-99.42C268.96,-100.55 292.08,-102.14 309.44,-103.33\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"316.49,-103.82 309.29,-106.48 312.96,-104.08 309.47,-103.84 309.5,-103.34 309.54,-102.84 313.03,-103.08 309.72,-100.2 316.49,-103.82 316.49,-103.82\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"431.45,-92 408.5,-74 431.45,-56 454.41,-74 431.45,-92\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-70.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M352.18,-99.6C367.59,-94.56 390.71,-87 407.83,-81.4\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"414.76,-79.13 409.09,-84.3 411.44,-80.22 408.11,-81.31 408.11,-81.31 408.11,-81.31 411.44,-80.22 407.13,-78.31 414.76,-79.13 414.76,-79.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\">1</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=\"#33a02c\" stroke-width=\"2\" d=\"M412.27,-70.94C373.02,-64.94 277.67,-53.67 200.56,-71 185.48,-74.39 169.43,-80.96 157,-86.77\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"150.49,-89.9 155.44,-84.03 153.43,-87.93 156.58,-86.42 156.8,-86.87 157.02,-87.32 153.86,-88.83 158.16,-89.71 150.49,-89.9 150.49,-89.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-80.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"30.33,-63 7.37,-45 30.33,-27 53.29,-45 30.33,-63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M44.64,-51.93C61.66,-60.79 91.34,-76.25 111.59,-86.79\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"117.81,-90.03 110.15,-89.59 114.71,-88.41 111.6,-86.8 111.6,-86.8 111.6,-86.8 114.71,-88.41 113.06,-84 117.81,-90.03 117.81,-90.03\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M48.14,-40.54C64.89,-36.1 90.75,-29.24 109.54,-24.25\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"116.62,-22.38 110.66,-27.22 113.24,-23.27 109.85,-24.17 109.85,-24.17 109.85,-24.17 113.24,-23.27 109.04,-21.13 116.62,-22.38 116.62,-22.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;5 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>6&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M117.05,-11.84C106.03,-8.52 91.19,-5.87 78.66,-10 66.52,-14 54.94,-22.45 46.27,-30.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"40.77,-35.1 43.79,-28.05 43.35,-32.74 45.92,-30.37 45.92,-30.37 45.92,-30.37 43.35,-32.74 48.05,-32.69 40.77,-35.1 40.77,-35.1\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-13.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-244\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-316 207.93,-298 230.89,-280 253.85,-298 230.89,-316\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-294.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M150.34,-252.68C166.84,-262.08 193.18,-277.09 210.99,-287.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-290.73 209.49,-290 214.09,-289 211.05,-287.27 211.05,-287.27 211.05,-287.27 214.09,-289 212.61,-284.53 217.13,-290.73 217.13,-290.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-274.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>9</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-262 207.93,-244 230.89,-226 253.85,-244 230.89,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;9 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>7&#45;&gt;9</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M152.5,-244C165.82,-244 184.51,-244 200.18,-244\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-244 200.6,-247.15 204.1,-244 200.6,-244 200.6,-244 200.6,-244 204.1,-244 200.6,-240.85 207.6,-244 207.6,-244\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-251\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-247.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M246.04,-291.46C262.34,-283.94 289.39,-271.45 309.13,-262.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"315.52,-259.38 310.49,-265.18 312.34,-260.85 309.17,-262.32 309.17,-262.32 309.17,-262.32 312.34,-260.85 307.85,-259.46 315.52,-259.38 315.52,-259.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9&#45;&gt;10 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>9&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M252.49,-245.42C267.8,-246.47 288.87,-247.92 305.71,-249.08\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"313.11,-249.59 305.91,-252.25 309.62,-249.35 306.12,-249.11 306.12,-249.11 306.12,-249.11 309.62,-249.35 306.34,-245.96 313.11,-249.59 313.11,-249.59\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11 -->\n",
+       "<g id=\"node13\" class=\"node\">\n",
+       "<title>11</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"431.45,-233 401.29,-215 431.45,-197 461.62,-215 431.45,-233\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-211.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;11 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>10&#45;&gt;11</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M354.4,-243.89C369.13,-238.29 389.77,-230.45 405.84,-224.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"412.41,-221.85 406.98,-227.28 409.14,-223.1 405.87,-224.34 405.87,-224.34 405.87,-224.34 409.14,-223.1 404.75,-221.39 412.41,-221.85 412.41,-221.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-239.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;7 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>11&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M406.24,-211.9C363.91,-207.22 273.97,-200.5 200.56,-217 185.48,-220.39 169.43,-226.96 157,-232.77\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"150.49,-235.9 155.44,-230.03 153.65,-234.38 156.8,-232.87 156.8,-232.87 156.8,-232.87 153.65,-234.38 158.16,-235.71 150.49,-235.9 150.49,-235.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g id=\"node14\" class=\"node\">\n",
+       "<title>12</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"30.33,-224 0.17,-206 30.33,-188 60.5,-206 30.33,-224\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>12&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.53,-212.79C66.49,-219.13 91.85,-228.6 110.19,-235.44\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"117.08,-238.02 109.42,-238.52 113.8,-236.79 110.53,-235.57 110.53,-235.57 110.53,-235.57 113.8,-236.79 111.63,-232.62 117.08,-238.02 117.08,-238.02\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13 -->\n",
+       "<g id=\"node15\" class=\"node\">\n",
+       "<title>13</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-179\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">13</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;13 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>12&#45;&gt;13</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M51.93,-200.54C67.58,-196.38 89.25,-190.64 106.26,-186.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"113.24,-184.27 107.28,-189.11 109.86,-185.17 106.47,-186.07 106.47,-186.07 106.47,-186.07 109.86,-185.17 105.67,-183.02 113.24,-184.27 113.24,-184.27\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;12 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>13&#45;&gt;12</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M114.35,-171.49C103.69,-168.3 90.19,-166.11 78.66,-170 66.9,-173.97 55.74,-182.15 47.22,-189.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"41.77,-194.79 44.74,-187.72 44.33,-192.41 46.89,-190.02 46.89,-190.02 46.89,-190.02 44.33,-192.41 49.04,-192.33 41.77,-194.79 41.77,-194.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g id=\"node16\" class=\"node\">\n",
+       "<title>14</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">14</text>\n",
+       "</g>\n",
+       "<!-- 15 -->\n",
+       "<g id=\"node17\" class=\"node\">\n",
+       "<title>15</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-462 200.73,-444 230.89,-426 261.06,-444 230.89,-462\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-440.3\" font-family=\"Lato\" font-size=\"14.00\">15</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;15 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>14&#45;&gt;15</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M152.5,-399.9C168.25,-408.88 191.53,-422.14 208.44,-431.78\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"214.81,-435.4 207.16,-434.68 211.76,-433.67 208.72,-431.94 208.72,-431.94 208.72,-431.94 211.76,-433.67 210.28,-429.2 214.81,-435.4 214.81,-435.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-420.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16 -->\n",
+       "<g id=\"node18\" class=\"node\">\n",
+       "<title>16</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-408 200.73,-390 230.89,-372 261.06,-390 230.89,-408\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">16</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;16 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>14&#45;&gt;16</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M155.68,-390C166.6,-390 180.36,-390 193.05,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"200.37,-390 193.37,-393.15 196.87,-390 193.37,-390 193.37,-390 193.37,-390 196.87,-390 193.37,-386.85 200.37,-390 200.37,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 17 -->\n",
+       "<g id=\"node19\" class=\"node\">\n",
+       "<title>17</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">17</text>\n",
+       "</g>\n",
+       "<!-- 15&#45;&gt;17 -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>15&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M247.35,-435.8C263.94,-427 290.5,-412.91 309.78,-402.68\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"316.01,-399.37 311.31,-405.43 312.92,-401.01 309.83,-402.65 309.83,-402.65 309.83,-402.65 312.92,-401.01 308.35,-399.87 316.01,-399.37 316.01,-399.37\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-421.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16&#45;&gt;17 -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>16&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M261.06,-390C275.27,-390 292.25,-390 306.22,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"313.22,-390 306.22,-393.15 309.72,-390 306.22,-390 306.22,-390 306.22,-390 309.72,-390 306.22,-386.85 313.22,-390 313.22,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18 -->\n",
+       "<g id=\"node20\" class=\"node\">\n",
+       "<title>18</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"431.45,-378 401.29,-360 431.45,-342 461.62,-360 431.45,-378\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-356.3\" font-family=\"Lato\" font-size=\"14.00\">18</text>\n",
+       "</g>\n",
+       "<!-- 17&#45;&gt;18 -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>17&#45;&gt;18</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M355.31,-383.78C369.51,-379.29 388.85,-373.17 404.34,-368.26\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"411.16,-366.11 405.44,-371.22 407.83,-367.16 404.49,-368.22 404.49,-368.22 404.49,-368.22 407.83,-367.16 403.54,-365.21 411.16,-366.11 411.16,-366.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-380.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18&#45;&gt;14 -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>18&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M405.63,-357.3C363.12,-353.35 273.88,-347.97 200.56,-363 186.24,-365.94 171.09,-371.97 158.98,-377.6\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"152.59,-380.66 157.54,-374.79 155.75,-379.15 158.9,-377.63 158.9,-377.63 158.9,-377.63 155.75,-379.15 160.26,-380.48 152.59,-380.66 152.59,-380.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-356.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 19 -->\n",
+       "<g id=\"node21\" class=\"node\">\n",
+       "<title>19</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"30.33,-370 0.17,-352 30.33,-334 60.5,-352 30.33,-370\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-348.3\" font-family=\"Lato\" font-size=\"14.00\">19</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;14 -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>19&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.53,-358.79C65.58,-364.79 89.16,-373.59 107.18,-380.32\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"114.04,-382.88 106.38,-383.38 110.76,-381.65 107.48,-380.43 107.48,-380.43 107.48,-380.43 110.76,-381.65 108.58,-377.48 114.04,-382.88 114.04,-382.88\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-378.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20 -->\n",
+       "<g id=\"node22\" class=\"node\">\n",
+       "<title>20</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-318\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-314.3\" font-family=\"Lato\" font-size=\"14.00\">20</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;20 -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>19&#45;&gt;20</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M50.48,-345.6C66.44,-340.27 89.34,-332.62 106.99,-326.73\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"113.71,-324.48 108.07,-329.69 110.39,-325.59 107.07,-326.7 107.07,-326.7 107.07,-326.7 110.39,-325.59 106.07,-323.71 113.71,-324.48 113.71,-324.48\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20&#45;&gt;19 -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>20&#45;&gt;19</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M118.61,-305.5C107.54,-297.55 91.98,-289.82 78.66,-296 62.59,-303.46 50,-319.37 41.86,-332.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"38.22,-338.41 39.11,-330.78 40.02,-335.4 41.82,-332.4 41.82,-332.4 41.82,-332.4 40.02,-335.4 44.52,-334.02 38.22,-338.41 38.22,-338.41\"/>\n",
+       "<text text-anchor=\"start\" x=\"82.16\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"78.66\" y=\"-299.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 0x7fcbe4382370> >"
+      ]
+     },
+     "execution_count": 15,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "# 1) Solving the game locally\n",
+    "# Unreachable parts are ignored, all of them are \"won\" by the env,\n",
+    "# the associated strategy is the 0 edges indicating no strategy\n",
+    "spot.solve_parity_game(arena)\n",
+    "spot.highlight_strategy(arena)\n",
+    "print(arena.get_strategy())\n",
+    "arena"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "(0, 7, 10, 0, 16, 19, 0, 0, 8, 11, 0, 17, 20, 0, 3, 0, 0, 15, 0, 24, 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=\"334pt\" height=\"360pt\"\n",
+       " viewBox=\"0.00 0.00 334.23 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7092198581560284 0.7092198581560284) rotate(0) translate(4 502)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-502 465.79,-502 465.79,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"210.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"231.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"247.39\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"209.39\" y=\"-469.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-98\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-94.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=\"M31.41,-112.99C33.49,-112.68 79.37,-105.92 108.79,-101.58\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"115.88,-100.54 109.41,-104.68 112.41,-101.05 108.95,-101.56 108.95,-101.56 108.95,-101.56 112.41,-101.05 108.49,-98.44 115.88,-100.54 115.88,-100.54\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-170 207.93,-152 230.89,-134 253.85,-152 230.89,-170\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-148.3\" 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=\"M150.34,-106.68C166.84,-116.08 193.18,-131.09 210.99,-141.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-144.73 209.49,-144 214.09,-143 211.05,-141.27 211.05,-141.27 211.05,-141.27 214.09,-143 212.61,-138.53 217.13,-144.73 217.13,-144.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-116 207.93,-98 230.89,-80 253.85,-98 230.89,-116\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-94.3\" 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=\"M152.5,-98C165.82,-98 184.51,-98 200.18,-98\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-98 200.6,-101.15 204.1,-98 200.6,-98 200.6,-98 200.6,-98 204.1,-98 200.6,-94.85 207.6,-98 207.6,-98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</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=\"#33a02c\" stroke-width=\"2\" d=\"M246.04,-145.46C263.02,-137.62 291.69,-124.39 311.59,-115.2\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"317.97,-112.25 312.94,-118.04 315,-114.17 311.83,-115.64 311.62,-115.19 311.41,-114.73 314.58,-113.26 310.3,-112.33 317.97,-112.25 317.97,-112.25\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-132.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;3 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M252.49,-99.42C268.96,-100.55 292.08,-102.14 309.44,-103.33\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"316.49,-103.82 309.29,-106.48 312.96,-104.08 309.47,-103.84 309.5,-103.34 309.54,-102.84 313.03,-103.08 309.72,-100.2 316.49,-103.82 316.49,-103.82\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"431.45,-92 408.5,-74 431.45,-56 454.41,-74 431.45,-92\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-70.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;4 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M352.18,-99.6C367.59,-94.56 390.71,-87 407.83,-81.4\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"414.76,-79.13 409.09,-84.3 411.44,-80.22 408.11,-81.31 408.11,-81.31 408.11,-81.31 411.44,-80.22 407.13,-78.31 414.76,-79.13 414.76,-79.13\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\">1</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=\"#33a02c\" stroke-width=\"2\" d=\"M412.27,-70.94C373.02,-64.94 277.67,-53.67 200.56,-71 185.48,-74.39 169.43,-80.96 157,-86.77\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"150.49,-89.9 155.44,-84.03 153.43,-87.93 156.58,-86.42 156.8,-86.87 157.02,-87.32 153.86,-88.83 158.16,-89.71 150.49,-89.9 150.49,-89.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-80.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"30.33,-63 7.37,-45 30.33,-27 53.29,-45 30.33,-63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M44.64,-51.93C61.66,-60.79 91.34,-76.25 111.59,-86.79\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"117.81,-90.03 110.15,-89.59 114.47,-88.86 111.37,-87.24 111.6,-86.8 111.83,-86.35 114.94,-87.97 113.06,-84 117.81,-90.03 117.81,-90.03\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M48.14,-40.54C64.89,-36.1 90.75,-29.24 109.54,-24.25\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"116.62,-22.38 110.66,-27.22 113.24,-23.27 109.85,-24.17 109.85,-24.17 109.85,-24.17 113.24,-23.27 109.04,-21.13 116.62,-22.38 116.62,-22.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;5 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>6&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M117.05,-11.84C106.03,-8.52 91.19,-5.87 78.66,-10 66.52,-14 54.94,-22.45 46.27,-30.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"40.77,-35.1 43.79,-28.05 43.35,-32.74 45.92,-30.37 45.92,-30.37 45.92,-30.37 43.35,-32.74 48.05,-32.69 40.77,-35.1 40.77,-35.1\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-13.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-244\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-316 207.93,-298 230.89,-280 253.85,-298 230.89,-316\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-294.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;8 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>7&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M150.34,-252.68C166.84,-262.08 193.18,-277.09 210.99,-287.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"217.13,-290.73 209.49,-290 214.09,-289 211.05,-287.27 211.05,-287.27 211.05,-287.27 214.09,-289 212.61,-284.53 217.13,-290.73 217.13,-290.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-274.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>9</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"230.89,-262 207.93,-244 230.89,-226 253.85,-244 230.89,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-240.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;9 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>7&#45;&gt;9</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M152.5,-244C165.82,-244 184.51,-244 200.18,-244\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"207.6,-244 200.6,-247.15 204.1,-244 200.6,-244 200.6,-244 200.6,-244 204.1,-244 200.6,-240.85 207.6,-244 207.6,-244\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-251\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-247.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M246.04,-291.46C262.34,-283.94 289.39,-271.45 309.13,-262.33\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"315.52,-259.38 310.49,-265.18 312.55,-261.3 309.38,-262.77 309.17,-262.32 308.96,-261.86 312.13,-260.4 307.85,-259.46 315.52,-259.38 315.52,-259.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9&#45;&gt;10 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>9&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M252.49,-245.42C267.8,-246.47 288.87,-247.92 305.71,-249.08\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"313.11,-249.59 305.91,-252.25 309.58,-249.84 306.09,-249.6 306.12,-249.11 306.16,-248.61 309.65,-248.85 306.34,-245.96 313.11,-249.59 313.11,-249.59\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11 -->\n",
+       "<g id=\"node13\" class=\"node\">\n",
+       "<title>11</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"431.45,-233 401.29,-215 431.45,-197 461.62,-215 431.45,-233\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-211.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;11 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>10&#45;&gt;11</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M354.4,-243.89C369.13,-238.29 389.77,-230.45 405.84,-224.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"412.41,-221.85 406.98,-227.28 409.14,-223.1 405.87,-224.34 405.87,-224.34 405.87,-224.34 409.14,-223.1 404.75,-221.39 412.41,-221.85 412.41,-221.85\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-239.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;7 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>11&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M406.24,-211.9C363.91,-207.22 273.97,-200.5 200.56,-217 185.48,-220.39 169.43,-226.96 157,-232.77\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"150.49,-235.9 155.44,-230.03 153.43,-233.93 156.58,-232.42 156.8,-232.87 157.02,-233.32 153.86,-234.83 158.16,-235.71 150.49,-235.9 150.49,-235.9\"/>\n",
+       "<text text-anchor=\"start\" x=\"282.72\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"279.22\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g id=\"node14\" class=\"node\">\n",
+       "<title>12</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"30.33,-224 0.17,-206 30.33,-188 60.5,-206 30.33,-224\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-202.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;7 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>12&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M49.53,-212.79C66.49,-219.13 91.85,-228.6 110.19,-235.44\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"117.08,-238.02 109.42,-238.52 113.63,-237.26 110.35,-236.04 110.53,-235.57 110.7,-235.1 113.98,-236.32 111.63,-232.62 117.08,-238.02 117.08,-238.02\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13 -->\n",
+       "<g id=\"node15\" class=\"node\">\n",
+       "<title>13</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-179\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">13</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;13 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>12&#45;&gt;13</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M51.93,-200.54C67.58,-196.38 89.25,-190.64 106.26,-186.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"113.24,-184.27 107.28,-189.11 109.86,-185.17 106.47,-186.07 106.47,-186.07 106.47,-186.07 109.86,-185.17 105.67,-183.02 113.24,-184.27 113.24,-184.27\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-196.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;12 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>13&#45;&gt;12</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M114.35,-171.49C103.69,-168.3 90.19,-166.11 78.66,-170 66.9,-173.97 55.74,-182.15 47.22,-189.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"41.77,-194.79 44.74,-187.72 44.33,-192.41 46.89,-190.02 46.89,-190.02 46.89,-190.02 44.33,-192.41 49.04,-192.33 41.77,-194.79 41.77,-194.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g id=\"node16\" class=\"node\">\n",
+       "<title>14</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">14</text>\n",
+       "</g>\n",
+       "<!-- 15 -->\n",
+       "<g id=\"node17\" class=\"node\">\n",
+       "<title>15</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-462 200.73,-444 230.89,-426 261.06,-444 230.89,-462\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-440.3\" font-family=\"Lato\" font-size=\"14.00\">15</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;15 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>14&#45;&gt;15</title>\n",
+       "<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M152.5,-399.9C168.25,-408.88 191.53,-422.14 208.44,-431.78\"/>\n",
+       "<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"214.81,-435.4 207.16,-434.68 211.52,-434.11 208.48,-432.37 208.72,-431.94 208.97,-431.5 212.01,-433.24 210.28,-429.2 214.81,-435.4 214.81,-435.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-420.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16 -->\n",
+       "<g id=\"node18\" class=\"node\">\n",
+       "<title>16</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"230.89,-408 200.73,-390 230.89,-372 261.06,-390 230.89,-408\"/>\n",
+       "<text text-anchor=\"middle\" x=\"230.89\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">16</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;16 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>14&#45;&gt;16</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M155.68,-390C166.6,-390 180.36,-390 193.05,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"200.37,-390 193.37,-393.15 196.87,-390 193.37,-390 193.37,-390 193.37,-390 196.87,-390 193.37,-386.85 200.37,-390 200.37,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"178.06\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 17 -->\n",
+       "<g id=\"node19\" class=\"node\">\n",
+       "<title>17</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"334.67\" cy=\"-390\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"334.67\" y=\"-386.3\" font-family=\"Lato\" font-size=\"14.00\">17</text>\n",
+       "</g>\n",
+       "<!-- 15&#45;&gt;17 -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>15&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M247.35,-435.8C263.94,-427 290.5,-412.91 309.78,-402.68\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"316.01,-399.37 311.31,-405.43 312.92,-401.01 309.83,-402.65 309.83,-402.65 309.83,-402.65 312.92,-401.01 308.35,-399.87 316.01,-399.37 316.01,-399.37\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-421.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 16&#45;&gt;17 -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>16&#45;&gt;17</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M261.06,-390C275.27,-390 292.25,-390 306.22,-390\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"313.22,-390 306.22,-393.15 309.72,-390 306.22,-390 306.22,-390 306.22,-390 309.72,-390 306.22,-386.85 313.22,-390 313.22,-390\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-393.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18 -->\n",
+       "<g id=\"node20\" class=\"node\">\n",
+       "<title>18</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"431.45,-378 401.29,-360 431.45,-342 461.62,-360 431.45,-378\"/>\n",
+       "<text text-anchor=\"middle\" x=\"431.45\" y=\"-356.3\" font-family=\"Lato\" font-size=\"14.00\">18</text>\n",
+       "</g>\n",
+       "<!-- 17&#45;&gt;18 -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>17&#45;&gt;18</title>\n",
+       "<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M355.31,-383.78C369.51,-379.29 388.85,-373.17 404.34,-368.26\"/>\n",
+       "<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"411.16,-366.11 405.44,-371.22 407.98,-367.64 404.64,-368.69 404.49,-368.22 404.34,-367.74 407.68,-366.68 403.54,-365.21 411.16,-366.11 411.16,-366.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"378.62\" y=\"-380.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 18&#45;&gt;14 -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>18&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M405.63,-357.3C363.12,-353.35 273.88,-347.97 200.56,-363 186.24,-365.94 171.09,-371.97 158.98,-377.6\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"152.59,-380.66 157.54,-374.79 155.75,-379.15 158.9,-377.63 158.9,-377.63 158.9,-377.63 155.75,-379.15 160.26,-380.48 152.59,-380.66 152.59,-380.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"287.22\" y=\"-356.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 19 -->\n",
+       "<g id=\"node21\" class=\"node\">\n",
+       "<title>19</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"30.33,-370 0.17,-352 30.33,-334 60.5,-352 30.33,-370\"/>\n",
+       "<text text-anchor=\"middle\" x=\"30.33\" y=\"-348.3\" font-family=\"Lato\" font-size=\"14.00\">19</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;14 -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>19&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.53,-358.79C65.58,-364.79 89.16,-373.59 107.18,-380.32\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"114.04,-382.88 106.38,-383.38 110.76,-381.65 107.48,-380.43 107.48,-380.43 107.48,-380.43 110.76,-381.65 108.58,-377.48 114.04,-382.88 114.04,-382.88\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-378.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20 -->\n",
+       "<g id=\"node22\" class=\"node\">\n",
+       "<title>20</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"134.11\" cy=\"-318\" rx=\"21.4\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"134.11\" y=\"-314.3\" font-family=\"Lato\" font-size=\"14.00\">20</text>\n",
+       "</g>\n",
+       "<!-- 19&#45;&gt;20 -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>19&#45;&gt;20</title>\n",
+       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M50.48,-345.6C66.44,-340.27 89.34,-332.62 106.99,-326.73\"/>\n",
+       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"113.71,-324.48 108.07,-329.69 110.55,-326.07 107.23,-327.17 107.07,-326.7 106.91,-326.23 110.23,-325.12 106.07,-323.71 113.71,-324.48 113.71,-324.48\"/>\n",
+       "<text text-anchor=\"middle\" x=\"86.66\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 20&#45;&gt;19 -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>20&#45;&gt;19</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M118.61,-305.5C107.54,-297.55 91.98,-289.82 78.66,-296 62.59,-303.46 50,-319.37 41.86,-332.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"38.22,-338.41 39.11,-330.78 40.02,-335.4 41.82,-332.4 41.82,-332.4 41.82,-332.4 40.02,-335.4 44.52,-334.02 38.22,-338.41 38.22,-338.41\"/>\n",
+       "<text text-anchor=\"start\" x=\"82.16\" y=\"-314.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "<text text-anchor=\"start\" x=\"78.66\" y=\"-299.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 0x7fcbe4382370> >"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "# 1) Solving the game globally\n",
+    "# The whole automaton is considered in this case\n",
+    "spot.solve_parity_game(arena, True)\n",
+    "spot.highlight_strategy(arena)\n",
+    "print(arena.get_strategy())\n",
+    "arena"
+   ]
   }
  ],
  "metadata": {
@@ -1686,7 +2818,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.10.5"
+   "version": "3.10.7"
   }
  },
  "nbformat": 4,