diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc
index 1126ad8e0..df9ad6017 100644
--- a/spot/twaalgos/mealy_machine.cc
+++ b/spot/twaalgos/mealy_machine.cc
@@ -36,7 +36,9 @@
 #include <spot/twaalgos/game.hh>
 #include <spot/twaalgos/hoa.hh>
 #include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/relabel.hh>
 #include <spot/twaalgos/synthesis.hh>
+#include <spot/priv/partitioned_relabel.hh>
 
 #include <picosat/picosat.h>
 
@@ -869,7 +871,7 @@ namespace
            split_cstr_time, prob_init_build_time, sat_time,
            build_time, refine_time, total_time;
     long long n_classes, n_refinement, n_lit, n_clauses,
-              n_iteration, n_bisim_let, n_min_states, done;
+              n_iteration, n_letters_part, n_bisim_let, n_min_states, done;
     std::string task;
     const std::string instance;
 
@@ -892,6 +894,7 @@ namespace
       , n_lit{-1}
       , n_clauses{-1}
       , n_iteration{-1}
+      , n_letters_part{-1}
       , n_bisim_let{-1}
       , n_min_states{-1}
       , done{-1}
@@ -935,8 +938,8 @@ namespace
               << "player_incomp_time,incomp_time,split_all_let_time,"
               << "split_min_let_time,split_cstr_time,prob_init_build_time,"
               << "sat_time,build_time,refine_time,total_time,n_classes,"
-              << "n_refinement,n_lit,n_clauses,n_iteration,n_bisim_let,"
-              << "n_min_states,done\n";
+              << "n_refinement,n_lit,n_clauses,n_iteration,n_letters_part,"
+              << "n_bisim_let,n_min_states,done\n";
         }
 
       assert(!task.empty());
@@ -965,6 +968,7 @@ namespace
       f(ss, n_lit);
       f(ss, n_clauses);
       f(ss, n_iteration);
+      f(ss, n_letters_part);
       f(ss, n_bisim_let);
       f(ss, n_min_states);
       f(ss, done, false);
@@ -1280,8 +1284,8 @@ namespace
   }
 
   square_matrix<bool, true>
-  compute_incomp(const_twa_graph_ptr mm, const unsigned n_env,
-                 satprob_info& si)
+  compute_incomp_impl_(const_twa_graph_ptr mm, const unsigned n_env,
+                       satprob_info& si, bool is_partitioned)
   {
     const unsigned n_tot = mm->num_states();
 
@@ -1292,20 +1296,6 @@ namespace
     // Have two states already been checked for common pred
     square_matrix<bool, true> checked_pred(n_env, false);
 
-    // We also need a transposed_graph
-    auto mm_t = make_twa_graph(mm->get_dict());
-    mm_t->copy_ap_of(mm);
-    mm_t->new_states(n_env);
-
-    for (unsigned s = 0; s < n_env; ++s)
-      {
-        for (const auto& e_env : mm->out(s))
-          {
-            unsigned dst_env = mm->out(e_env.dst).begin()->dst;
-            mm_t->new_edge(dst_env, s, e_env.cond);
-          }
-      }
-
     // Utility function
     auto get_cond = [&mm](unsigned s)->const bdd&
       {return mm->out(s).begin()->cond; };
@@ -1367,15 +1357,28 @@ namespace
 #endif
     // direct incomp: Two env states can reach incompatible player states
     // under the same input
+    // The original graph mm is not sorted, and most of the
+    // sorting is not rentable
+    // However, bdd_have_common_assignment simply becomes equality
     auto direct_incomp = [&](unsigned s1, unsigned s2)
       {
         for (const auto& e1 : mm->out(s1))
           for (const auto& e2 : mm->out(s2))
             {
+              if (is_partitioned && (e1.cond != e2.cond))
+                continue;
               if (!is_p_incomp(e1.dst - n_env, e2.dst - n_env))
                 continue; //Compatible -> no prob
               // Reachable under same letter?
-              if (bdd_have_common_assignment(e1.cond, e2.cond))
+              if (is_partitioned) // -> Yes
+                {
+                  trace << s1 << " and " << s2 << " directly incomp "
+                        "due to successors " << e1.dst << " and " << e2.dst
+                        << '\n';
+                  return true;
+                }
+              else if (!is_partitioned
+                       && bdd_have_common_assignment(e1.cond, e2.cond))
                 {
                   trace << s1 << " and " << s2 << " directly incomp "
                         "due to successors " << e1.dst << " and " << e2.dst
@@ -1388,7 +1391,27 @@ namespace
 
     // If two states can reach an incompatible state
     // under the same input, then they are incompatible as well
-    auto tag_predec = [&](unsigned s1, unsigned s2)
+
+    // Version if the input is not partitioned
+    // We also need a transposed_graph
+    twa_graph_ptr mm_t = nullptr;
+    if (!is_partitioned)
+    {
+      mm_t = make_twa_graph(mm->get_dict());
+      mm_t->copy_ap_of(mm);
+      mm_t->new_states(n_env);
+
+      for (unsigned s = 0; s < n_env; ++s)
+        {
+          for (const auto& e_env : mm->out(s))
+            {
+              unsigned dst_env = mm->out(e_env.dst).begin()->dst;
+              mm_t->new_edge(dst_env, s, e_env.cond);
+            }
+        }
+    }
+
+    auto tag_predec_unpart = [&](unsigned s1, unsigned s2)
       {
         static std::vector<std::pair<unsigned, unsigned>> todo_;
         assert(todo_.empty());
@@ -1422,17 +1445,98 @@ namespace
         // Done tagging all pred
       };
 
+    // Version of taging taking advantaged of partitioned conditions
+    struct S
+    {
+    };
+    struct T
+    {
+      int id;
+    };
+    std::unique_ptr<digraph<S, T>> mm_t_part;
+    if (is_partitioned)
+      {
+        mm_t_part = std::make_unique<digraph<S, T>>(n_env, mm->num_edges());
+        mm_t_part->new_states(n_env);
+
+        for (unsigned s = 0; s < n_env; ++s)
+          {
+            for (const auto& e_env : mm->out(s))
+              {
+                unsigned dst_env = mm->out(e_env.dst).begin()->dst;
+                mm_t_part->new_edge(dst_env, s, e_env.cond.id());
+              }
+          }
+
+        // Now we need to sort the edge to ensure that
+        // the next algo works correctly
+        mm_t_part->sort_edges_srcfirst_([](const auto& e1, const auto& e2)
+                                          {return e1.id < e2.id; });
+        mm_t_part->chain_edges_();
+      }
+
+    auto tag_predec_part = [&](unsigned s1, unsigned s2)
+      {
+        static std::vector<std::pair<unsigned, unsigned>> todo_;
+        assert(todo_.empty());
+
+        todo_.emplace_back(s1, s2);
+
+        while (!todo_.empty())
+          {
+            auto [i, j] = todo_.back();
+            todo_.pop_back();
+            if (checked_pred.get(i, j))
+              continue;
+            // If predecs are already marked incomp
+            auto e_it_i = mm_t_part->out(i);
+            auto e_it_j = mm_t_part->out(j);
+
+            auto e_it_i_e = e_it_i.end();
+            auto e_it_j_e = e_it_j.end();
+
+            auto e_i = e_it_i.begin();
+            auto e_j = e_it_j.begin();
+
+            // Joint iteration over both edge groups
+            while ((e_i != e_it_i_e) && (e_j != e_it_j_e))
+              {
+                if (e_i->id < e_j->id)
+                  ++e_i;
+                else if (e_j->id < e_i->id)
+                  ++e_j;
+                else
+                  {
+                    assert(e_j->id == e_i->id);
+                    trace << e_i->dst << " and " << e_j->dst << " tagged incomp"
+                            " due to " << e_i->id << '\n';
+                    inc_env.set(e_i->dst, e_j->dst, true);
+                    todo_.emplace_back(e_i->dst, e_j->dst);
+                    ++e_i;
+                    ++e_j;
+                  }
+              }
+            checked_pred.set(i, j, true);
+          }
+        // Done tagging all pred
+      };
+
     for (unsigned s1 = 0; s1 < n_env; ++s1)
       for (unsigned s2 = s1 + 1; s2 < n_env; ++s2)
         {
           if (inc_env.get(s1, s2))
             continue; // Already done
+
           // Check if they are incompatible for some letter
           // We have to check all pairs of edges
           if (direct_incomp(s1, s2))
             {
               inc_env.set(s1, s2, true);
-              tag_predec(s1, s2);
+              if (is_partitioned)
+                tag_predec_part(s1, s2);
+              else
+                tag_predec_unpart(s1, s2);
+
             }
         }
 
@@ -1442,9 +1546,38 @@ namespace
 #endif
     si.incomp_time = si.restart();
     return inc_env;
+  } // incomp no partition
+
+  square_matrix<bool, true>
+  compute_incomp(const_twa_graph_ptr mm, const unsigned n_env,
+                 satprob_info& si, int max_letter_mult)
+  {
+    // Try to generate a graph with partitioned env transitions
+    auto mm2 = make_twa_graph(mm, twa::prop_set::all());
+    set_state_players(mm2, get_state_players(mm));
+    set_synthesis_outputs(mm2, get_synthesis_outputs(mm));
+
+    // todo get a good value for cutoff
+    auto relabel_maps
+        = partitioned_game_relabel_here(mm2, true, false, true,
+                                        false, -1u, max_letter_mult);
+    bool succ = !relabel_maps.env_map.empty();
+
+    si.n_letters_part = relabel_maps.env_map.size();
+
+#ifdef TRACE
+    if (succ)
+      std::cout << "Relabeling succesfull with " << relabel_maps.env_map.size()
+                << " letters\n";
+    else
+      std::cout << "Relabeling aborted\n";
+#endif
+
+    return compute_incomp_impl_(succ ? const_twa_graph_ptr(mm2) : mm,
+                                n_env, si, succ);
   }
 
-    struct part_sol_t
+  struct part_sol_t
   {
     std::vector<unsigned> psol;
     std::vector<unsigned> is_psol;
@@ -1602,6 +1735,11 @@ namespace
     return std::make_pair(n_group, which_group);
   }
 
+  // Helper function
+  // Computes the set of all original letters implied by the leaves
+  // This avoids transposing the graph
+
+
   // Computes the letters of each group
   // Letters here means bdds such that for all valid
   // assignments of the bdd we go to the same dst from the same source
@@ -1611,7 +1749,9 @@ namespace
   {
     //To avoid recalc
     std::set<int> all_bdd;
-    std::set<int> treated_bdd;
+    std::vector<bdd> all_bdd_v;
+    std::unordered_map<unsigned, unsigned> node2idx;
+
     std::unordered_multimap<size_t, std::pair<unsigned, std::set<int>>>
         sigma_map;
 
@@ -1649,6 +1789,11 @@ namespace
             continue;
           else
             {
+              // Store bdds as vector for compatibility
+              all_bdd_v.clear(); // Note: sorted automatically by id
+              std::transform(all_bdd.begin(), all_bdd.end(),
+                            std::back_inserter(all_bdd_v),
+                            [](int i){return bdd_from_int(i); });
               // Insert it already into the sigma_map
               trace << "Group " << groupidx << " generates a new alphabet\n";
               sigma_map.emplace(std::piecewise_construct,
@@ -1658,62 +1803,60 @@ namespace
             }
         }
 
+        // Result
         red.share_sigma_with.push_back(groupidx);
         red.all_letters.emplace_back();
         auto& group_letters = red.all_letters.back();
 
-        treated_bdd.clear();
+        // Compute it
+        auto this_part = try_partition_me(all_bdd_v, -1u);
+        assert(this_part.relabel_succ);
 
-        for (unsigned s = 0; s < n_env; ++s)
+        // Transform it
+        // group_letters is pair<new_letter, set of implied orig letters as id>
+        // There are as many new_letters as treated bdds in the partition
+        group_letters.clear();
+        group_letters.reserve(this_part.treated.size());
+        node2idx.clear();
+        node2idx.reserve(this_part.treated.size());
+
+        for (const auto& [label, node] : this_part.treated)
           {
-            if (red.which_group[s] != groupidx)
-              continue;
-            for (const auto& e : mmw->out(s))
-              {
-                bdd rcond = e.cond;
-                const int econd_id = rcond.id();
-                trace << rcond << " - " << econd_id << std::endl;
-                if (treated_bdd.count(econd_id))
-                  {
-                    trace << "Already treated" << std::endl;
-                    continue;
-                  }
-                treated_bdd.insert(econd_id);
-
-                assert(rcond != bddfalse && "Deactivated edges are forbiden");
-                // Check against all currently used "letters"
-                const size_t osize = group_letters.size();
-                for (size_t i = 0; i < osize; ++i)
-                  {
-                    if (group_letters[i].first == rcond)
-                      {
-                        rcond = bddfalse;
-                        group_letters[i].second.insert(econd_id);
-                        break;
-                      }
-                    bdd inter = group_letters[i].first & rcond;
-                    if (inter == bddfalse)
-                      continue; // No intersection
-                    if (group_letters[i].first == inter)
-                      group_letters[i].second.insert(econd_id);
-                    else
-                      {
-                        group_letters[i].first -= inter;
-                        group_letters.emplace_back(inter,
-                                                   group_letters[i].second);
-                        group_letters.back().second.insert(econd_id);
-                      }
-
-                    rcond -= inter;
-                    // Early exit?
-                    if (rcond == bddfalse)
-                      break;
-                  }
-                // Leftovers?
-                if (rcond != bddfalse)
-                  group_letters.emplace_back(rcond, std::set<int>{econd_id});
-              }
+            node2idx[node] = group_letters.size();
+            group_letters.emplace_back(std::piecewise_construct,
+                                       std::forward_as_tuple(label),
+                                       std::forward_as_tuple());
           }
+
+        // Go through the graph for each original letter
+        auto search_leaves
+            = [&ig = *this_part.ig, &group_letters, &node2idx]
+                (int orig_letter_id, unsigned s, auto&& search_leaves_) -> void
+          {
+            if (ig.state_storage(s).succ == 0)
+              {
+                // Leaf
+                unsigned idx = node2idx[s];
+                auto& setidx = group_letters[idx].second;
+                setidx.emplace_hint(setidx.end(), orig_letter_id);
+              }
+            else
+              {
+                // Traverse
+                for (const auto& e : ig.out(s))
+                  search_leaves_(orig_letter_id, e.dst, search_leaves_);
+              }
+          };
+
+        const unsigned Norig = all_bdd_v.size();
+        for (unsigned s = 0; s < Norig; ++s)
+          search_leaves(all_bdd_v[s].id(), s, search_leaves);
+
+        // Verify that all letters imply at least one original letter
+        assert(std::all_of(group_letters.begin(), group_letters.end(),
+                           [](const auto& l){return !l.second.empty(); }));
+
+
 #ifdef TRACE
         trace << "this group letters" << std::endl;
         auto sp = [&](const auto& c)
@@ -3467,6 +3610,7 @@ namespace
         for (unsigned letter_idx = 0; letter_idx < n_ml; ++letter_idx)
           {
             const auto& ml_list = group_map[letter_idx];
+            assert(ml_list.begin() != ml_list.end());
             // Incompatibility is commutative
             // new / new constraints
             const auto it_end = ml_list.end();
@@ -3794,12 +3938,9 @@ namespace
         return minmach;
       } // while loop
   } // try_build_machine
-} // namespace
 
-namespace spot
-{
-  twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
-                               int premin)
+  twa_graph_ptr minimize_mealy_(const const_twa_graph_ptr& mm,
+                               int premin, int max_letter_mult)
   {
     bdd outputs = ensure_mealy("minimize_mealy", mm);
 
@@ -3866,8 +4007,9 @@ namespace spot
     si.reorg_time = si.restart();
 
     // Compute incompatibility based on bdd
-    auto incompmat = compute_incomp(mmw, n_env, si);
+    auto incompmat = compute_incomp(mmw, n_env, si, max_letter_mult);
 #ifdef TRACE
+    std::cerr << "Final incomp mat\n";
     incompmat.print(std::cerr);
 #endif
 
@@ -3944,6 +4086,15 @@ namespace spot
       minmachine));
     return minmachine;
   }
+} // namespace
+
+namespace spot
+{
+  twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
+                               int premin)
+  {
+    return minimize_mealy_(mm, premin, 10);
+  }
 
   twa_graph_ptr
   minimize_mealy(const const_twa_graph_ptr& mm,
@@ -3970,7 +4121,8 @@ namespace spot
       sat_dimacs_file
         = std::make_unique<fwrapper>(dimacsfile);
     sat_instance_name = si.opt.get_str("satinstancename");
-    auto res = minimize_mealy(mm, si.minimize_lvl-4);
+    auto res = minimize_mealy_(mm, si.minimize_lvl-4,
+                               si.opt.get("max_letter_mult", 10));
     sat_csv_file.reset();
     sat_dimacs_file.reset();
     return res;
@@ -4161,7 +4313,7 @@ namespace spot
         reduce_mealy_here(m, minimize_lvl == 2);
       }
     else if (3 <= minimize_lvl)
-      m = minimize_mealy(m, minimize_lvl - 4);
+      m = minimize_mealy(m, si);
 
     // Convert to demanded output format
     bool is_split = m->get_named_prop<region_t>("state-player");
diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index 88e22ff04..4e38efd5b 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -37,6 +37,7 @@
 
 
 #include <algorithm>
+#include <string>
 
 // Helper function/structures for split_2step
 namespace{
@@ -1935,4 +1936,98 @@ namespace spot
     return res;
   }
 
+  namespace
+  {
+    const std::string in_mark_s("__AP_IN__");
+    const std::string out_mark_s("__AP_OUT__");
+  }
+
+  game_relabeling_map
+  partitioned_game_relabel_here(twa_graph_ptr& arena,
+                                bool relabel_env,
+                                bool relabel_play,
+                                bool split_env,
+                                bool split_play,
+                                unsigned max_letter,
+                                unsigned max_letter_mult)
+  {
+    if (!arena)
+      throw std::runtime_error("arena is null.");
+    auto& arena_r = *arena;
+
+    const auto& sp = get_state_players(arena);
+    bdd all_ap = arena->ap_vars();
+
+    if (std::find_if(arena->ap().cbegin(), arena->ap().cend(),
+                     [](const auto& ap)
+                       {
+                         return ap.ap_name() == out_mark_s
+                                || ap.ap_name() == in_mark_s;
+                       }) != arena->ap().cend())
+      throw std::runtime_error("partitioned_game_relabel_here(): "
+                               "You can not use "
+                               + in_mark_s + " or " + out_mark_s +
+                               " as propositions if relabeling.");
+
+    bdd out_mark = bdd_ithvar(arena_r.register_ap(out_mark_s));
+    bdd in_mark = bdd_ithvar(arena_r.register_ap(in_mark_s));
+
+    bdd outs = get_synthesis_outputs(arena) & out_mark;
+    bdd ins = bdd_exist(all_ap, outs) & in_mark;
+
+    for (auto& e : arena_r.edges())
+      e.cond = e.cond & (sp[e.src] ? out_mark : in_mark);
+
+    game_relabeling_map res;
+
+    if (relabel_env)
+      res.env_map
+        = partitioned_relabel_here(arena, split_env, max_letter,
+                                   max_letter_mult, ins, "__nv_in");
+    if (relabel_play)
+      res.player_map
+        = partitioned_relabel_here(arena, split_play, max_letter,
+                                   max_letter_mult, outs, "__nv_out");
+    return res;
+  }
+
+  void
+  relabel_game_here(twa_graph_ptr& arena,
+                    game_relabeling_map& rel_maps)
+  {
+    if (!arena)
+      throw std::runtime_error("arena is null.");
+    auto& arena_r = *arena;
+
+    // Check that it was partitioned_game_relabel_here
+    if (!((std::find_if(arena->ap().cbegin(), arena->ap().cend(),
+                        [](const auto& ap)
+                          { return ap.ap_name() == out_mark_s; })
+             != arena->ap().cend())
+          && (std::find_if(arena->ap().cbegin(), arena->ap().cend(),
+                           [](const auto& ap)
+                             { return ap.ap_name() == in_mark_s; }))
+               != arena->ap().cend()))
+      throw std::runtime_error("relabel_game_here(): " +
+                               in_mark_s + " or " + out_mark_s +
+                               " not registered with arena. "
+                               "Not relabeled?");
+
+    if (!rel_maps.env_map.empty())
+      relabel_here(arena, &rel_maps.env_map);
+    if (!rel_maps.player_map.empty())
+      relabel_here(arena, &rel_maps.player_map);
+
+    bdd dummy_ap = bdd_ithvar(arena_r.register_ap(in_mark_s))
+                   & bdd_ithvar(arena_r.register_ap(out_mark_s));
+
+    for (auto& e : arena_r.edges())
+      e.cond = bdd_exist(e.cond, dummy_ap);
+
+    arena_r.unregister_ap(arena_r.register_ap(in_mark_s));
+    arena_r.unregister_ap(arena_r.register_ap(out_mark_s));
+
+    return;
+  }
+
 } // spot
diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh
index b1b7fdf1d..2d9c0600a 100644
--- a/spot/twaalgos/synthesis.hh
+++ b/spot/twaalgos/synthesis.hh
@@ -21,6 +21,7 @@
 
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/game.hh>
+#include <spot/twaalgos/relabel.hh>
 #include <bddx.h>
 
 namespace spot
@@ -256,4 +257,39 @@ namespace spot
   SPOT_API bool
   solve_game(twa_graph_ptr arena, synthesis_info& gi);
 
+  struct SPOT_API game_relabeling_map
+  {
+    relabeling_map env_map;
+    relabeling_map player_map;
+  };
+
+  /// \ingroup synthesis
+  /// \brief Tries to relabel a SPLIT game \a arena using fresh propositions.
+  /// Can be applied to env or player depending on \a relabel_env
+  /// and \a relabel_play. The arguments \a split_env and \a split_play
+  /// determine whether or not env and player edges are to
+  /// be split into several transitions labelled by letters not conditions.
+  ///
+  /// \return pair of relabeling_map, first is for env, second is for player.
+  /// The maps are empty if no relabeling was performed
+  /// \note Can also be applied to split mealy machine.
+  /// \note partitioned_relabel_here can not be used directly if there are
+  /// T (true conditions)
+  SPOT_API game_relabeling_map
+  partitioned_game_relabel_here(twa_graph_ptr& arena,
+                                bool relabel_env,
+                                bool relabel_play,
+                                bool split_env = false,
+                                bool split_play = false,
+                                unsigned max_letter = -1u,
+                                unsigned max_letter_mult = -1u);
+
+  /// \ingroup synthesis
+  /// \brief Undoes a relabeling done by partitioned_game_relabel_here.
+  /// A dedicated function is necessary in order to remove the
+  /// variables tagging env and player conditions
+  SPOT_API void
+  relabel_game_here(twa_graph_ptr& arena,
+                    game_relabeling_map& rel_maps);
+
 }
diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb
index 9d7fe7d96..ebeeaacb7 100644
--- a/tests/python/_mealy.ipynb
+++ b/tests/python/_mealy.ipynb
@@ -129,7 +129,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35aaa030> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f86481a2690> >"
       ]
      },
      "execution_count": 4,
@@ -209,7 +209,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35aaa900> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85f45cbb70> >"
       ]
      },
      "execution_count": 6,
@@ -283,7 +283,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35aaa900> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85f45cbb70> >"
       ]
      },
      "execution_count": 8,
@@ -387,7 +387,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35ac20c0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f861bfc8ae0> >"
       ]
      },
      "execution_count": 9,
@@ -532,7 +532,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35ac2720> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85f45efde0> >"
       ]
      },
      "execution_count": 10,
@@ -584,13 +584,13 @@
        "      <th>split_cstr_time</th>\n",
        "      <th>prob_init_build_time</th>\n",
        "      <th>...</th>\n",
-       "      <th>refine_time</th>\n",
        "      <th>total_time</th>\n",
        "      <th>n_classes</th>\n",
        "      <th>n_refinement</th>\n",
        "      <th>n_lit</th>\n",
        "      <th>n_clauses</th>\n",
        "      <th>n_iteration</th>\n",
+       "      <th>n_letters_part</th>\n",
        "      <th>n_bisim_let</th>\n",
        "      <th>n_min_states</th>\n",
        "      <th>done</th>\n",
@@ -600,15 +600,15 @@
        "    <tr>\n",
        "      <th>0</th>\n",
        "      <td>presat</td>\n",
-       "      <td>25643.3</td>\n",
-       "      <td>1.112e-06</td>\n",
-       "      <td>4.588e-06</td>\n",
-       "      <td>9.888e-06</td>\n",
-       "      <td>4.549e-06</td>\n",
-       "      <td>1.5929e-05</td>\n",
-       "      <td>9.338e-06</td>\n",
-       "      <td>5.901e-06</td>\n",
-       "      <td>6.7276e-05</td>\n",
+       "      <td>3868.95</td>\n",
+       "      <td>3.282e-06</td>\n",
+       "      <td>1.4388e-05</td>\n",
+       "      <td>0.000129765</td>\n",
+       "      <td>1.3759e-05</td>\n",
+       "      <td>9.499e-06</td>\n",
+       "      <td>8.73e-06</td>\n",
+       "      <td>9.01e-06</td>\n",
+       "      <td>6.6209e-05</td>\n",
        "      <td>...</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -616,7 +616,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
-       "      <td>NaN</td>\n",
+       "      <td>3</td>\n",
        "      <td>2</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -634,40 +634,40 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
-       "      <td>NaN</td>\n",
-       "      <td>0.000282709</td>\n",
+       "      <td>0.000743251</td>\n",
        "      <td>2</td>\n",
        "      <td>0</td>\n",
        "      <td>7</td>\n",
        "      <td>12</td>\n",
        "      <td>0</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "      <td>4</td>\n",
        "      <td>1</td>\n",
        "    </tr>\n",
        "  </tbody>\n",
        "</table>\n",
-       "<p>2 rows × 22 columns</p>\n",
+       "<p>2 rows × 23 columns</p>\n",
        "</div>"
       ],
       "text/plain": [
        "     task premin_time reorg_time partsol_time player_incomp_time incomp_time  \\\n",
-       "0  presat     25643.3  1.112e-06    4.588e-06          9.888e-06   4.549e-06   \n",
+       "0  presat     3868.95  3.282e-06   1.4388e-05        0.000129765  1.3759e-05   \n",
        "1     sat         NaN        NaN          NaN                NaN         NaN   \n",
        "\n",
        "  split_all_let_time split_min_let_time split_cstr_time prob_init_build_time  \\\n",
-       "0         1.5929e-05          9.338e-06       5.901e-06           6.7276e-05   \n",
+       "0          9.499e-06           8.73e-06        9.01e-06           6.6209e-05   \n",
        "1                NaN                NaN             NaN                  NaN   \n",
        "\n",
-       "   ... refine_time   total_time n_classes n_refinement n_lit n_clauses  \\\n",
-       "0  ...         NaN          NaN       NaN          NaN   NaN       NaN   \n",
-       "1  ...         NaN  0.000282709         2            0     7        12   \n",
+       "   ...   total_time n_classes n_refinement n_lit n_clauses n_iteration  \\\n",
+       "0  ...          NaN       NaN          NaN   NaN       NaN         NaN   \n",
+       "1  ...  0.000743251         2            0     7        12           0   \n",
        "\n",
-       "  n_iteration n_bisim_let n_min_states done  \n",
-       "0         NaN           2          NaN  NaN  \n",
-       "1           0         NaN            4    1  \n",
+       "  n_letters_part n_bisim_let n_min_states done  \n",
+       "0              3           2          NaN  NaN  \n",
+       "1            NaN         NaN            4    1  \n",
        "\n",
-       "[2 rows x 22 columns]"
+       "[2 rows x 23 columns]"
       ]
      },
      "metadata": {},
@@ -758,7 +758,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc88735f00> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f861bfc8630> >"
       ]
      },
      "execution_count": 11,
@@ -861,7 +861,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc6157fe40> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f861bf9fb40> >"
       ]
      },
      "execution_count": 12,
@@ -1000,7 +1000,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc6157f210> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f861bf9f210> >"
       ]
      },
      "execution_count": 13,
@@ -1051,13 +1051,13 @@
        "      <th>split_cstr_time</th>\n",
        "      <th>prob_init_build_time</th>\n",
        "      <th>...</th>\n",
-       "      <th>refine_time</th>\n",
        "      <th>total_time</th>\n",
        "      <th>n_classes</th>\n",
        "      <th>n_refinement</th>\n",
        "      <th>n_lit</th>\n",
        "      <th>n_clauses</th>\n",
        "      <th>n_iteration</th>\n",
+       "      <th>n_letters_part</th>\n",
        "      <th>n_bisim_let</th>\n",
        "      <th>n_min_states</th>\n",
        "      <th>done</th>\n",
@@ -1067,15 +1067,15 @@
        "    <tr>\n",
        "      <th>0</th>\n",
        "      <td>presat</td>\n",
-       "      <td>25643.4</td>\n",
-       "      <td>1.683e-06</td>\n",
-       "      <td>5.611e-06</td>\n",
-       "      <td>2.66e-05</td>\n",
-       "      <td>1.2e-07</td>\n",
-       "      <td>3.647e-06</td>\n",
-       "      <td>8.365e-06</td>\n",
-       "      <td>3.747e-06</td>\n",
-       "      <td>2.5538e-05</td>\n",
+       "      <td>3869.08</td>\n",
+       "      <td>3.213e-06</td>\n",
+       "      <td>9.079e-06</td>\n",
+       "      <td>9.5752e-05</td>\n",
+       "      <td>5.168e-06</td>\n",
+       "      <td>5.727e-06</td>\n",
+       "      <td>7.543e-06</td>\n",
+       "      <td>1.5784e-05</td>\n",
+       "      <td>4.0507e-05</td>\n",
        "      <td>...</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -1083,7 +1083,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
-       "      <td>NaN</td>\n",
+       "      <td>1</td>\n",
        "      <td>1</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -1102,7 +1102,6 @@
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
        "      <td>NaN</td>\n",
-       "      <td>NaN</td>\n",
        "      <td>1</td>\n",
        "      <td>0</td>\n",
        "      <td>3</td>\n",
@@ -1111,6 +1110,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "    </tr>\n",
        "    <tr>\n",
        "      <th>2</th>\n",
@@ -1125,7 +1125,6 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
-       "      <td>4.4884e-05</td>\n",
        "      <td>NaN</td>\n",
        "      <td>1</td>\n",
        "      <td>1</td>\n",
@@ -1135,6 +1134,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "    </tr>\n",
        "    <tr>\n",
        "      <th>3</th>\n",
@@ -1149,48 +1149,48 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
-       "      <td>NaN</td>\n",
-       "      <td>0.000200344</td>\n",
+       "      <td>0.000399073</td>\n",
        "      <td>2</td>\n",
        "      <td>0</td>\n",
        "      <td>17</td>\n",
        "      <td>29</td>\n",
        "      <td>1</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "      <td>4</td>\n",
        "      <td>1</td>\n",
        "    </tr>\n",
        "  </tbody>\n",
        "</table>\n",
-       "<p>4 rows × 22 columns</p>\n",
+       "<p>4 rows × 23 columns</p>\n",
        "</div>"
       ],
       "text/plain": [
        "         task premin_time reorg_time partsol_time player_incomp_time  \\\n",
-       "0      presat     25643.4  1.683e-06    5.611e-06           2.66e-05   \n",
+       "0      presat     3869.08  3.213e-06    9.079e-06         9.5752e-05   \n",
        "1         sat         NaN        NaN          NaN                NaN   \n",
        "2  refinement         NaN        NaN          NaN                NaN   \n",
        "3         sat         NaN        NaN          NaN                NaN   \n",
        "\n",
        "  incomp_time split_all_let_time split_min_let_time split_cstr_time  \\\n",
-       "0     1.2e-07          3.647e-06          8.365e-06       3.747e-06   \n",
+       "0   5.168e-06          5.727e-06          7.543e-06      1.5784e-05   \n",
        "1         NaN                NaN                NaN             NaN   \n",
        "2         NaN                NaN                NaN             NaN   \n",
        "3         NaN                NaN                NaN             NaN   \n",
        "\n",
-       "  prob_init_build_time  ... refine_time   total_time n_classes n_refinement  \\\n",
-       "0           2.5538e-05  ...         NaN          NaN       NaN          NaN   \n",
-       "1                  NaN  ...         NaN          NaN         1            0   \n",
-       "2                  NaN  ...  4.4884e-05          NaN         1            1   \n",
-       "3                  NaN  ...         NaN  0.000200344         2            0   \n",
+       "  prob_init_build_time  ...   total_time n_classes n_refinement n_lit  \\\n",
+       "0           4.0507e-05  ...          NaN       NaN          NaN   NaN   \n",
+       "1                  NaN  ...          NaN         1            0     3   \n",
+       "2                  NaN  ...          NaN         1            1    10   \n",
+       "3                  NaN  ...  0.000399073         2            0    17   \n",
        "\n",
-       "  n_lit n_clauses n_iteration n_bisim_let n_min_states done  \n",
-       "0   NaN       NaN         NaN           1          NaN  NaN  \n",
-       "1     3         6           0         NaN          NaN  NaN  \n",
-       "2    10        16         NaN         NaN          NaN  NaN  \n",
-       "3    17        29           1         NaN            4    1  \n",
+       "  n_clauses n_iteration n_letters_part n_bisim_let n_min_states done  \n",
+       "0       NaN         NaN              1           1          NaN  NaN  \n",
+       "1         6           0            NaN         NaN          NaN  NaN  \n",
+       "2        16         NaN            NaN         NaN          NaN  NaN  \n",
+       "3        29           1            NaN         NaN            4    1  \n",
        "\n",
-       "[4 rows x 22 columns]"
+       "[4 rows x 23 columns]"
       ]
      },
      "metadata": {},
@@ -1200,6 +1200,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
+      "Number of variables\n",
       "0    NaN\n",
       "1      3\n",
       "2     10\n",
@@ -1285,7 +1286,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc35ac22a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f861bfcdc00> >"
       ]
      },
      "execution_count": 14,
@@ -1297,6 +1298,7 @@
     "si = spot.synthesis_info()\n",
     "si.minimize_lvl = 3\n",
     "aut_ms, table = spot.minimize_mealy(aut_s, si, display_log=True, return_log=True)\n",
+    "print(\"Number of variables\")\n",
     "print(table[\"n_lit\"])\n",
     "aut_ms"
    ]
@@ -1347,13 +1349,13 @@
        "      <th>split_cstr_time</th>\n",
        "      <th>prob_init_build_time</th>\n",
        "      <th>...</th>\n",
-       "      <th>refine_time</th>\n",
        "      <th>total_time</th>\n",
        "      <th>n_classes</th>\n",
        "      <th>n_refinement</th>\n",
        "      <th>n_lit</th>\n",
        "      <th>n_clauses</th>\n",
        "      <th>n_iteration</th>\n",
+       "      <th>n_letters_part</th>\n",
        "      <th>n_bisim_let</th>\n",
        "      <th>n_min_states</th>\n",
        "      <th>done</th>\n",
@@ -1363,15 +1365,15 @@
        "    <tr>\n",
        "      <th>0</th>\n",
        "      <td>presat</td>\n",
-       "      <td>25643.5</td>\n",
-       "      <td>1.563e-06</td>\n",
-       "      <td>5.4e-06</td>\n",
-       "      <td>2.0519e-05</td>\n",
-       "      <td>1.3e-07</td>\n",
-       "      <td>3.968e-06</td>\n",
-       "      <td>9.698e-06</td>\n",
-       "      <td>7.624e-06</td>\n",
-       "      <td>3.211e-05</td>\n",
+       "      <td>3869.14</td>\n",
+       "      <td>2.863e-06</td>\n",
+       "      <td>9.08e-06</td>\n",
+       "      <td>6.0622e-05</td>\n",
+       "      <td>4.679e-06</td>\n",
+       "      <td>5.308e-06</td>\n",
+       "      <td>8.59e-06</td>\n",
+       "      <td>7.962e-06</td>\n",
+       "      <td>4.0159e-05</td>\n",
        "      <td>...</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -1379,7 +1381,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
-       "      <td>NaN</td>\n",
+       "      <td>1</td>\n",
        "      <td>1</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
@@ -1398,7 +1400,6 @@
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
        "      <td>NaN</td>\n",
-       "      <td>NaN</td>\n",
        "      <td>1</td>\n",
        "      <td>0</td>\n",
        "      <td>3</td>\n",
@@ -1407,6 +1408,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "    </tr>\n",
        "    <tr>\n",
        "      <th>2</th>\n",
@@ -1421,7 +1423,6 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
-       "      <td>4.4633e-05</td>\n",
        "      <td>NaN</td>\n",
        "      <td>1</td>\n",
        "      <td>1</td>\n",
@@ -1431,6 +1432,7 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "    </tr>\n",
        "    <tr>\n",
        "      <th>3</th>\n",
@@ -1445,48 +1447,48 @@
        "      <td>NaN</td>\n",
        "      <td>NaN</td>\n",
        "      <td>...</td>\n",
-       "      <td>NaN</td>\n",
-       "      <td>0.000280675</td>\n",
+       "      <td>0.000416464</td>\n",
        "      <td>2</td>\n",
        "      <td>0</td>\n",
        "      <td>17</td>\n",
        "      <td>29</td>\n",
        "      <td>1</td>\n",
        "      <td>NaN</td>\n",
+       "      <td>NaN</td>\n",
        "      <td>4</td>\n",
        "      <td>1</td>\n",
        "    </tr>\n",
        "  </tbody>\n",
        "</table>\n",
-       "<p>4 rows × 22 columns</p>\n",
+       "<p>4 rows × 23 columns</p>\n",
        "</div>"
       ],
       "text/plain": [
        "         task premin_time reorg_time partsol_time player_incomp_time  \\\n",
-       "0      presat     25643.5  1.563e-06      5.4e-06         2.0519e-05   \n",
+       "0      presat     3869.14  2.863e-06     9.08e-06         6.0622e-05   \n",
        "1         sat         NaN        NaN          NaN                NaN   \n",
        "2  refinement         NaN        NaN          NaN                NaN   \n",
        "3         sat         NaN        NaN          NaN                NaN   \n",
        "\n",
        "  incomp_time split_all_let_time split_min_let_time split_cstr_time  \\\n",
-       "0     1.3e-07          3.968e-06          9.698e-06       7.624e-06   \n",
+       "0   4.679e-06          5.308e-06           8.59e-06       7.962e-06   \n",
        "1         NaN                NaN                NaN             NaN   \n",
        "2         NaN                NaN                NaN             NaN   \n",
        "3         NaN                NaN                NaN             NaN   \n",
        "\n",
-       "  prob_init_build_time  ... refine_time   total_time n_classes n_refinement  \\\n",
-       "0            3.211e-05  ...         NaN          NaN       NaN          NaN   \n",
-       "1                  NaN  ...         NaN          NaN         1            0   \n",
-       "2                  NaN  ...  4.4633e-05          NaN         1            1   \n",
-       "3                  NaN  ...         NaN  0.000280675         2            0   \n",
+       "  prob_init_build_time  ...   total_time n_classes n_refinement n_lit  \\\n",
+       "0           4.0159e-05  ...          NaN       NaN          NaN   NaN   \n",
+       "1                  NaN  ...          NaN         1            0     3   \n",
+       "2                  NaN  ...          NaN         1            1    10   \n",
+       "3                  NaN  ...  0.000416464         2            0    17   \n",
        "\n",
-       "  n_lit n_clauses n_iteration n_bisim_let n_min_states done  \n",
-       "0   NaN       NaN         NaN           1          NaN  NaN  \n",
-       "1     3         6           0         NaN          NaN  NaN  \n",
-       "2    10        16         NaN         NaN          NaN  NaN  \n",
-       "3    17        29           1         NaN            4    1  \n",
+       "  n_clauses n_iteration n_letters_part n_bisim_let n_min_states done  \n",
+       "0       NaN         NaN              1           1          NaN  NaN  \n",
+       "1         6           0            NaN         NaN          NaN  NaN  \n",
+       "2        16         NaN            NaN         NaN          NaN  NaN  \n",
+       "3        29           1            NaN         NaN            4    1  \n",
        "\n",
-       "[4 rows x 22 columns]"
+       "[4 rows x 23 columns]"
       ]
      },
      "metadata": {},
@@ -1570,10 +1572,118 @@
     "    "
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "b10213b8",
+   "metadata": {},
+   "source": [
+    "# Testing partitioned relabeling"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "id": "fd5ca506",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Conditions in orig machine:  8\n",
+      "Conditions in relabeled machine:  13\n"
+     ]
+    }
+   ],
+   "source": [
+    "def get_mealy():\n",
+    "    return spot.split_2step(spot.automaton(\"\"\"HOA: v1\n",
+    "States: 2\n",
+    "Start: 0\n",
+    "AP: 11 \"u0accel0accel\" \"u0accel0f1dcon23p81b\" \"u0accel0f1dcon231b\" \"u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b\" \"u0gear0gear\" \"u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b\" \"u0steer0f1dsteering0angle0trackpos1b\" \"u0steer0steer\" \"p0p0gt0rpm0f1dcon5523231b\" \"p0p0lt0rpm0f1dcon32323231b\" \"p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b\"\n",
+    "acc-name: all\n",
+    "Acceptance: 0 t\n",
+    "properties: trans-labels explicit-labels state-acc deterministic\n",
+    "controllable-AP: 0 1 2 3 4 5 6 7\n",
+    "--BODY--\n",
+    "State: 0\n",
+    "[!0&!1&2&!3&4&!5&6&!7&!8&!9&!10] 0\n",
+    "[!0&1&!2&!3&4&!5&6&!7&!8&!9&10] 0\n",
+    "[!0&!1&2&!3&!4&5&6&!7&!8&9&!10] 0\n",
+    "[!0&1&!2&!3&!4&5&6&!7&!8&9&10] 0\n",
+    "[!0&!1&2&3&!4&!5&6&!7&8&!9&!10] 0\n",
+    "[!0&1&!2&3&!4&!5&6&!7&8&!9&10] 0\n",
+    "[!0&!1&2&!3&!4&5&!6&7&8&9 | !0&!1&2&!3&!4&5&6&!7&8&9 | !0&!1&2&!3&4&!5&!6&7&8&9 | !0&!1&2&!3&4&!5&6&!7&8&9 | !0&!1&2&3&!4&!5&!6&7&8&9 | !0&!1&2&3&!4&!5&6&!7&8&9 | !0&1&!2&!3&!4&5&!6&7&8&9 | !0&1&!2&!3&!4&5&6&!7&8&9 | !0&1&!2&!3&4&!5&!6&7&8&9 | !0&1&!2&!3&4&!5&6&!7&8&9 | !0&1&!2&3&!4&!5&!6&7&8&9 | !0&1&!2&3&!4&!5&6&!7&8&9 | 0&!1&!2&!3&!4&5&!6&7&8&9 | 0&!1&!2&!3&!4&5&6&!7&8&9 | 0&!1&!2&!3&4&!5&!6&7&8&9 | 0&!1&!2&!3&4&!5&6&!7&8&9 | 0&!1&!2&3&!4&!5&!6&7&8&9 | 0&!1&!2&3&!4&!5&6&!7&8&9] 1\n",
+    "State: 1\n",
+    "[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 1\n",
+    "--END--\"\"\"))\n",
+    "\n",
+    "def env_conditions(m):\n",
+    "    sp = spot.get_state_players(m)\n",
+    "    conds = []\n",
+    "    for e in m.edges():\n",
+    "        if sp[e.src]:\n",
+    "            continue\n",
+    "        if not e.cond in conds:\n",
+    "            conds.append(e.cond)\n",
+    "    return conds\n",
+    "print(\"Conditions in orig machine: \", len(env_conditions(get_mealy())))\n",
+    "ms = get_mealy()\n",
+    "# Relabel only env\n",
+    "spot.partitioned_game_relabel_here(ms, True, False, True, False)\n",
+    "print(\"Conditions in relabeled machine: \", len(env_conditions(ms)))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "id": "ee29da67",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Partitioned env letters: 13\n"
+     ]
+    }
+   ],
+   "source": [
+    "si = spot.synthesis_info()\n",
+    "si.minimize_lvl = 3\n",
+    "# Turn on relabeling\n",
+    "si.opt.set(\"max_letter_mult\", 100000)\n",
+    "\n",
+    "mm, log = spot.minimize_mealy(get_mealy(), si, return_log=True)\n",
+    "print(\"Partitioned env letters:\", log[\"n_letters_part\"][0])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "id": "0aec8019",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Partitioned env letters: 0\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Turn off relabeling\n",
+    "si.opt.set(\"max_letter_mult\", 0)\n",
+    "\n",
+    "mm, log = spot.minimize_mealy(get_mealy(), si, return_log=True)\n",
+    "print(\"Partitioned env letters:\", log[\"n_letters_part\"][0])"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "5c9fe115",
+   "id": "a92f4f43",
    "metadata": {},
    "outputs": [],
    "source": []
diff --git a/tests/python/_partitioned_relabel.ipynb b/tests/python/_partitioned_relabel.ipynb
index a9c1c7af7..b7f1c4380 100644
--- a/tests/python/_partitioned_relabel.ipynb
+++ b/tests/python/_partitioned_relabel.ipynb
@@ -121,7 +121,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b0311a80> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415fbd0> >"
       ]
      },
      "execution_count": 2,
@@ -248,7 +248,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b0311a80> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415fbd0> >"
       ]
      },
      "execution_count": 3,
@@ -353,7 +353,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b0311a80> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415fbd0> >"
       ]
      },
      "execution_count": 4,
@@ -457,7 +457,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c0d50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415bf30> >"
       ]
      },
      "metadata": {},
@@ -611,7 +611,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c0d50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415bf30> >"
       ]
      },
      "execution_count": 5,
@@ -769,7 +769,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c0d50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936415bf30> >"
       ]
      },
      "execution_count": 6,
@@ -886,7 +886,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c90f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936c3c6090> >"
       ]
      },
      "metadata": {},
@@ -1015,7 +1015,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c90f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936c3c6090> >"
       ]
      },
      "execution_count": 7,
@@ -1184,7 +1184,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f65b02c90f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f936c3c6090> >"
       ]
      },
      "execution_count": 8,
@@ -1198,6 +1198,1135 @@
     "print(aut.to_str(\"hoa\"))\n",
     "aut"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ef77c2ee",
+   "metadata": {},
+   "source": [
+    "# Concerning games and Mealy machines\n",
+    "\n",
+    "Games and split mealy machines have both: defined outputs and states that either belong to player or env.\n",
+    "Relabeling is done separately for env and player transitions (over inputs and outputs respectively).\n",
+    "\n",
+    "The problem is that T (bddtrue) is ambiguous, as it may be over the inputs or outputs.\n",
+    "\n",
+    "We therefore introduce a dedicated function for this matter."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "id": "296a93d3",
+   "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=\"3059pt\" height=\"242pt\"\n",
+       " viewBox=\"0.00 0.00 3059.00 242.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 238)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-238 3055,-238 3055,4 -4,4\"/>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"1525.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-14.3\" font-family=\"Times,serif\" 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=\"M1470.65,-18C1472.17,-18 1484.6,-18 1497.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1497.44,-21.5 1507.44,-18 1497.44,-14.5 1497.44,-21.5\"/>\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=\"M1524.05,-36.15C1523.83,-45.54 1524.31,-54 1525.5,-54 1526.22,-54 1526.69,-50.86 1526.89,-46.28\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1530.39,-46.17 1526.95,-36.15 1523.39,-46.13 1530.39,-46.17\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1523.09,-35.98C1521.81,-53.2 1522.61,-72 1525.5,-72 1527.83,-72 1528.8,-59.83 1528.42,-46.1\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1531.91,-45.79 1527.91,-35.98 1524.92,-46.14 1531.91,-45.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1522.46,-36.08C1519.78,-60.41 1520.79,-90 1525.5,-90 1529.57,-90 1530.88,-67.95 1529.43,-46.26\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1532.9,-45.73 1528.54,-36.08 1525.92,-46.35 1532.9,-45.73\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-93.8\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1522.02,-36.11C1517.75,-67.24 1518.91,-108 1525.5,-108 1531.4,-108 1532.95,-75.38 1530.15,-46.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1533.6,-45.64 1528.98,-36.11 1526.65,-46.45 1533.6,-45.64\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-111.8\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1521.75,-35.8C1515.71,-73.55 1516.96,-126 1525.5,-126 1533.3,-126 1535.02,-82.18 1530.65,-45.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1534.1,-45.22 1529.25,-35.8 1527.16,-46.19 1534.1,-45.22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-129.8\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1521.51,-35.77C1513.69,-79.97 1515.02,-144 1525.5,-144 1535.2,-144 1537.06,-89.13 1531.08,-45.9\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1534.5,-45.11 1529.49,-35.77 1527.58,-46.19 1534.5,-45.11\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1525.5\" y=\"-147.8\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b / !u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"2181.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2181.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1543.66,-18C1632.7,-18 2042.3,-18 2152.91,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2153.22,-21.5 2163.22,-18 2153.22,-14.5 2153.22,-21.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1853.5\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b / (label too long)</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2163.38,-21.1C2100.03,-33.69 2106.07,-54 2181.5,-54 2252.81,-54 2262.11,-35.85 2209.39,-23.23\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2210.14,-19.81 2199.62,-21.1 2208.65,-26.65 2210.14,-19.81\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2181.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1 / (label too long)</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 0x7f936415f510> >"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "HOA: v1\n",
+      "States: 9\n",
+      "Start: 0\n",
+      "AP: 11 \"u0accel0accel\" \"u0accel0f1dcon23p81b\" \"u0accel0f1dcon231b\" \"u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b\" \"u0gear0gear\" \"u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b\" \"u0steer0f1dsteering0angle0trackpos1b\" \"u0steer0steer\" \"p0p0gt0rpm0f1dcon5523231b\" \"p0p0lt0rpm0f1dcon32323231b\" \"p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b\"\n",
+      "acc-name: all\n",
+      "Acceptance: 0 t\n",
+      "properties: trans-labels explicit-labels state-acc deterministic\n",
+      "spot-state-player: 0 0 1 1 1 1 1 1 1\n",
+      "controllable-AP: 0 1 2 3 4 5 6 7\n",
+      "--BODY--\n",
+      "State: 0\n",
+      "[!8&!9&!10] 2\n",
+      "[!8&!9&10] 3\n",
+      "[!8&9&!10] 4\n",
+      "[!8&9&10] 5\n",
+      "[8&!9&!10] 6\n",
+      "[8&!9&10] 7\n",
+      "[8&9] 8\n",
+      "State: 1\n",
+      "[t] 8\n",
+      "State: 2\n",
+      "[!0&!1&2&!3&4&!5&6&!7] 0\n",
+      "State: 3\n",
+      "[!0&1&!2&!3&4&!5&6&!7] 0\n",
+      "State: 4\n",
+      "[!0&!1&2&!3&!4&5&6&!7] 0\n",
+      "State: 5\n",
+      "[!0&1&!2&!3&!4&5&6&!7] 0\n",
+      "State: 6\n",
+      "[!0&!1&2&3&!4&!5&6&!7] 0\n",
+      "State: 7\n",
+      "[!0&1&!2&3&!4&!5&6&!7] 0\n",
+      "State: 8\n",
+      "[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 1\n",
+      "--END--\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=\"2276pt\" height=\"681pt\"\n",
+       " viewBox=\"0.00 0.00 2276.00 681.31\" 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 677.31)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-677.31 2272,-677.31 2272,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1134\" y=\"-658.11\" font-family=\"Times,serif\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"middle\" x=\"1134\" y=\"-643.11\" font-family=\"Times,serif\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"56\" cy=\"-353.31\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-349.61\" font-family=\"Times,serif\" 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,-353.31C2.67,-353.31 15.1,-353.31 27.63,-353.31\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"27.94,-356.81 37.94,-353.31 27.94,-349.81 27.94,-356.81\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-574.31 2034,-556.31 2061,-538.31 2088,-556.31 2061,-574.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-552.61\" font-family=\"Times,serif\" 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=\"M57.22,-371.39C58.21,-417.08 63.52,-535.26 92,-559.31 245.53,-688.96 1778.82,-577.79 2026.34,-558.92\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.82,-562.4 2036.52,-558.14 2026.28,-555.42 2026.82,-562.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-624.11\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-509.31 2034,-491.31 2061,-473.31 2088,-491.31 2061,-509.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-487.61\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M59.13,-371.06C63.42,-403.34 74.22,-469.63 92,-483.31 131.81,-513.95 1760.2,-495.04 2024.06,-491.77\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2024.28,-495.26 2034.23,-491.64 2024.19,-488.26 2024.28,-495.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-504.11\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-428.31 2034,-410.31 2061,-392.31 2088,-410.31 2061,-428.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-406.61\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;4 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>0&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M62.79,-370.07C68.18,-382.82 77.58,-399.46 92,-407.31 136.12,-431.33 1760.9,-413.74 2024.14,-410.73\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2024.34,-414.23 2034.29,-410.61 2024.26,-407.23 2024.34,-414.23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-423.11\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-352.31 2034,-334.31 2061,-316.31 2088,-334.31 2061,-352.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-330.61\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.01,-353.15C251.93,-351.46 1770.39,-337.06 2024.12,-334.65\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2024.29,-338.15 2034.26,-334.56 2024.23,-331.15 2024.29,-338.15\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-356.11\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-279.31 2034,-261.31 2061,-243.31 2088,-261.31 2061,-279.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-257.61\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;6 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>0&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M60.38,-335.71C64.62,-319 73.69,-294.77 92,-283.31 134.56,-256.68 1758.95,-260.41 2023.7,-261.2\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2023.9,-264.7 2033.91,-261.23 2023.92,-257.7 2023.9,-264.7\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-287.11\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-208.31 2034,-190.31 2061,-172.31 2088,-190.31 2061,-208.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-186.61\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;7 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>0&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.53,-335.39C62,-299.63 71.77,-221.44 92,-205.31 131.28,-173.99 1760.12,-187.57 2024.05,-189.97\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2024.19,-193.48 2034.23,-190.07 2024.26,-186.48 2024.19,-193.48\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-209.11\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-143.31 2034,-125.31 2061,-107.31 2088,-125.31 2061,-143.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-121.61\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;8 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>0&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.92,-335.29C57.14,-286.59 60.66,-154.2 92,-127.31 396.88,134.26 1802.14,-83.01 2029.03,-120.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2028.78,-123.65 2039.22,-121.82 2029.92,-116.74 2028.78,-123.65\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-131.11\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2044.47,-549.21C2036.21,-545.8 2025.76,-542.09 2016,-540.31 1963.41,-530.75 133.32,-553.21 92,-519.31 71.06,-502.14 62.14,-423.96 58.78,-381.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.27,-380.99 58.04,-371.28 55.29,-381.51 62.27,-380.99\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-544.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;0 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>3&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2048.14,-481.58C2039.74,-475.33 2027.88,-467.75 2016,-464.31 1964.66,-449.44 136.21,-468.35 92,-438.31 73.2,-425.54 64.49,-400.67 60.45,-381.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"63.89,-380.44 58.7,-371.2 56.99,-381.65 63.89,-380.44\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-468.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;0 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>4&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2046.74,-401.69C2038.31,-396.72 2026.96,-390.96 2016,-388.31 1808.18,-338.17 300.67,-415.83 92,-369.31 88.5,-368.53 84.94,-367.38 81.48,-366.04\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"82.75,-362.77 72.19,-361.94 79.93,-369.18 82.75,-362.77\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-392.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2045.82,-326.43C2037.43,-322.22 2026.43,-317.47 2016,-315.31 1963.66,-304.49 140.95,-293.85 92,-315.31 84.66,-318.53 78.18,-324.13 72.85,-330.06\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"69.88,-328.18 66.33,-338.16 75.33,-332.57 69.88,-328.18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-319.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;0 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>6&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2045.87,-253.02C2037.5,-248.59 2026.5,-243.59 2016,-241.31 1963.77,-230 135.06,-209.65 92,-241.31 66.03,-260.4 58.79,-298.67 57.05,-325.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"53.55,-325.16 56.61,-335.3 60.54,-325.46 53.55,-325.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-245.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;0 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>7&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2047.67,-180.99C2039.25,-175.23 2027.55,-168.36 2016,-165.31 1964.33,-151.66 133.1,-131.15 92,-165.31 67.96,-185.29 60.35,-277.62 58,-325.04\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"54.5,-325.1 57.55,-335.24 61.49,-325.41 54.5,-325.1\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-169.11\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"2250\" cy=\"-125.31\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2250\" y=\"-121.61\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;1 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>8&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2088,-125.31C2123.2,-125.31 2185.72,-125.31 2221.62,-125.31\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2221.84,-128.81 2231.84,-125.31 2221.84,-121.81 2221.84,-128.81\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2160\" y=\"-129.11\" font-family=\"Times,serif\" font-size=\"14.00\">(label too long)</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2234.28,-115.77C2228.25,-112.39 2221.04,-109.02 2214,-107.31 2167.35,-96.02 2153.1,-98.05 2106,-107.31 2099.3,-108.63 2092.34,-110.97 2085.99,-113.54\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2084.37,-110.43 2076.62,-117.65 2087.19,-116.84 2084.37,-110.43\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2160\" y=\"-111.11\" font-family=\"Times,serif\" 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 0x7f936415f990> >"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "HOA: v1\n",
+      "States: 9\n",
+      "Start: 0\n",
+      "AP: 21 \"u0accel0accel\" \"u0accel0f1dcon23p81b\" \"u0accel0f1dcon231b\" \"u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b\" \"u0gear0gear\" \"u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b\" \"u0steer0f1dsteering0angle0trackpos1b\" \"u0steer0steer\" \"p0p0gt0rpm0f1dcon5523231b\" \"p0p0lt0rpm0f1dcon32323231b\" \"p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b\" \"__AP_OUT__\" \"__AP_IN__\" \"__nv_in0\" \"__nv_in1\" \"__nv_in2\" \"__nv_in3\" \"__nv_out0\" \"__nv_out1\" \"__nv_out2\" \"__nv_out3\"\n",
+      "acc-name: all\n",
+      "Acceptance: 0 t\n",
+      "properties: trans-labels explicit-labels state-acc deterministic\n",
+      "spot-state-player: 0 0 1 1 1 1 1 1 1\n",
+      "controllable-AP: 0 1 2 3 4 5 6 7\n",
+      "--BODY--\n",
+      "State: 0\n",
+      "[!13&!14&!15&!16] 2\n",
+      "[13&!14&!15&!16] 3\n",
+      "[!13&14&!15&!16] 4\n",
+      "[13&14&!15&!16] 5\n",
+      "[!13&!14&15&!16] 6\n",
+      "[13&!14&15&!16] 7\n",
+      "[!13&14&15&!16] 8\n",
+      "[13&14&15&!16] 2\n",
+      "[!13&!14&!15&16] 3\n",
+      "[13&!14&!15&16] 4\n",
+      "[!13&14&!15&16] 5\n",
+      "[13&14&!15&16] 6\n",
+      "[!13&!14&15&16] 7\n",
+      "State: 1\n",
+      "[13&14&15&!16] 8\n",
+      "[!13&!14&!15&16] 8\n",
+      "[13&!14&!15&16] 8\n",
+      "[!13&14&!15&16] 8\n",
+      "[13&14&!15&16] 8\n",
+      "[!13&!14&15&16] 8\n",
+      "[!13&14&15&!16] 8\n",
+      "State: 2\n",
+      "[!17&!18&!19&!20 | !17&18&19&!20] 0\n",
+      "State: 3\n",
+      "[17&!18&!19&!20 | 17&18&19&!20] 0\n",
+      "State: 4\n",
+      "[!17&!18&!19&20 | !17&18&!19&!20] 0\n",
+      "State: 5\n",
+      "[17&!18&!19&20 | 17&18&!19&!20] 0\n",
+      "State: 6\n",
+      "[!17&!18&19&!20 | !17&18&!19&20] 0\n",
+      "State: 7\n",
+      "[17&!18&19&!20 | 17&18&!19&20] 0\n",
+      "State: 8\n",
+      "[!17&!18&20 | 18&19&!20 | !19&20] 1\n",
+      "--END--\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=\"1754pt\" height=\"977pt\"\n",
+       " viewBox=\"0.00 0.00 1754.00 976.79\" 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 972.79)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-972.79 1750,-972.79 1750,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"873\" y=\"-953.59\" font-family=\"Times,serif\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"middle\" x=\"873\" y=\"-938.59\" font-family=\"Times,serif\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"56\" cy=\"-538.79\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-535.09\" font-family=\"Times,serif\" 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,-538.79C2.67,-538.79 15.1,-538.79 27.63,-538.79\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"27.94,-542.29 37.94,-538.79 27.94,-535.29 27.94,-542.29\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-860.79 870,-842.79 897,-824.79 924,-842.79 897,-860.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-839.09\" font-family=\"Times,serif\" 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=\"M57.6,-556.95C59.93,-621.7 69.37,-838.51 92,-858.79 217.75,-971.54 685.67,-888.1 852,-858.79 858.26,-857.69 864.79,-855.77 870.86,-853.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.4,-856.79 880.48,-849.94 869.89,-850.26 872.4,-856.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-919.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.89,-556.81C61.02,-616.19 72.35,-802.99 92,-820.79 107.65,-834.97 830.91,-838.81 852,-839.79 855.29,-839.95 858.71,-840.13 862.14,-840.34\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.06,-843.84 872.26,-840.99 862.51,-836.85 862.06,-843.84\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-843.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; __nv_in1 &amp; __nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-746.79 870,-728.79 897,-710.79 924,-728.79 897,-746.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-725.09\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.22,-556.87C58.21,-602.56 63.52,-720.75 92,-744.79 124.26,-772.03 810.42,-752.12 852,-744.79 858.26,-743.69 864.79,-741.77 870.86,-739.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.4,-742.79 880.48,-735.94 869.89,-736.26 872.4,-742.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-761.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.03,-556.95C60.67,-596.36 69.18,-687.76 92,-706.79 108.22,-720.32 830.91,-724.81 852,-725.79 855.29,-725.95 858.71,-726.13 862.14,-726.34\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.06,-729.84 872.26,-726.99 862.51,-722.85 862.06,-729.84\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-729.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-632.79 870,-614.79 897,-596.79 924,-614.79 897,-632.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-611.09\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;4 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>0&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.06,-557C60.41,-578.73 67.94,-614.21 92,-630.79 126.76,-654.76 810.42,-638.12 852,-630.79 858.26,-629.69 864.79,-627.77 870.86,-625.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.4,-628.79 880.48,-621.94 869.89,-622.26 872.4,-628.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-646.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;4 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>0&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M62.84,-555.46C68.26,-568.16 77.67,-584.77 92,-592.79 128.85,-613.43 809.81,-609.83 852,-611.79 855.29,-611.95 858.71,-612.13 862.14,-612.34\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.06,-615.84 872.26,-612.99 862.51,-608.85 862.06,-615.84\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-615.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-518.79 870,-500.79 897,-482.79 924,-500.79 897,-518.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-497.09\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.22,-538.65C183.05,-537.68 773.25,-531.79 852,-516.79 858.24,-515.6 864.77,-513.65 870.83,-511.51\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.37,-514.67 880.46,-507.83 869.87,-508.13 872.37,-514.67\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-541.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M65.51,-523.31C71.56,-514.03 80.61,-503.05 92,-497.79 168.68,-462.43 767.6,-494.92 852,-497.79 855.47,-497.91 859.1,-498.08 862.71,-498.28\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.52,-501.78 872.72,-498.91 862.96,-494.79 862.52,-501.78\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-501.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-404.79 870,-386.79 897,-368.79 924,-386.79 897,-404.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-383.09\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;6 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>0&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.77,-520.64C57.56,-495.21 63.19,-449.66 92,-427.79 125.65,-402.26 810.52,-410.81 852,-402.79 858.24,-401.59 864.77,-399.63 870.83,-397.49\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.36,-400.65 880.46,-393.81 869.87,-394.11 872.36,-400.65\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-431.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; __nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;6 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>0&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.31,-520.88C61.44,-483.82 70.72,-400.8 92,-383.79 124.98,-357.43 809.8,-382.36 852,-383.79 855.47,-383.91 859.1,-384.08 862.71,-384.28\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.52,-387.78 872.72,-384.91 862.96,-380.79 862.52,-387.78\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-387.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-290.79 870,-272.79 897,-254.79 924,-272.79 897,-290.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-269.09\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;7 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>0&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.03,-520.8C57.53,-472.82 61.72,-343.66 92,-316.79 123.61,-288.76 810.53,-296.89 852,-288.79 858.24,-287.58 864.76,-285.61 870.83,-283.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"872.36,-286.63 880.45,-279.79 869.86,-280.09 872.36,-286.63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-320.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; !__nv_in1 &amp; __nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;7 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>0&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.99,-520.79C61.33,-463.22 73.07,-286.42 92,-269.79 123.72,-241.93 809.8,-268.36 852,-269.79 855.47,-269.91 859.1,-270.08 862.71,-270.28\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"862.52,-273.78 872.72,-270.91 862.96,-266.79 862.52,-273.78\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-273.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; __nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"897,-214.79 870,-196.79 897,-178.79 924,-196.79 897,-214.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897\" y=\"-193.09\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;8 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>0&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.5,-520.61C59.53,-453.62 68.2,-223.38 92,-201.79 322.33,7.16 760.71,-143.8 870.55,-186.48\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"869.28,-189.74 879.87,-190.14 871.84,-183.22 869.28,-189.74\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-205.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; __nv_in1 &amp; __nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M887.38,-830.99C879.43,-821.17 866.67,-807.85 852,-801.79 773.9,-769.55 155.03,-833.06 92,-776.79 61.42,-749.49 57.16,-624.06 56.83,-567.09\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"60.33,-566.97 56.81,-556.98 53.33,-566.98 60.33,-566.97\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-805.59\" font-family=\"Times,serif\" font-size=\"14.00\">(!__nv_out0 &amp; !__nv_out1 &amp; !__nv_out2 &amp; !__nv_out3) | (!__nv_out0 &amp; __nv_out1 &amp; __nv_out2 &amp; !__nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;0 -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>3&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M887.38,-716.99C879.43,-707.18 866.67,-693.86 852,-687.79 773.92,-655.5 158.55,-713.86 92,-661.79 63.63,-639.59 57.16,-596.12 56.23,-567.26\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"59.73,-566.95 56.11,-556.99 52.73,-567.03 59.73,-566.95\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-691.59\" font-family=\"Times,serif\" font-size=\"14.00\">(__nv_out0 &amp; !__nv_out1 &amp; !__nv_out2 &amp; !__nv_out3) | (__nv_out0 &amp; __nv_out1 &amp; __nv_out2 &amp; !__nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;0 -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>4&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M887.39,-602.96C879.45,-593.12 866.69,-579.79 852,-573.79 773.79,-541.87 174.31,-573.79 92,-554.79 88.51,-553.99 84.94,-552.82 81.49,-551.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"82.76,-548.21 72.2,-547.36 79.93,-554.61 82.76,-548.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-577.59\" font-family=\"Times,serif\" font-size=\"14.00\">(!__nv_out0 &amp; __nv_out1 &amp; !__nv_out2 &amp; !__nv_out3) | (!__nv_out0 &amp; !__nv_out1 &amp; !__nv_out2 &amp; __nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M886.98,-489.06C878.96,-479.68 866.32,-467.22 852,-461.79 812.52,-446.82 127.5,-438.93 92,-461.79 75.33,-472.52 66.51,-493.35 61.9,-510.64\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"58.38,-510.29 59.53,-520.82 65.2,-511.87 58.38,-510.29\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-465.59\" font-family=\"Times,serif\" font-size=\"14.00\">(__nv_out0 &amp; __nv_out1 &amp; !__nv_out2 &amp; !__nv_out3) | (__nv_out0 &amp; !__nv_out1 &amp; !__nv_out2 &amp; __nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;0 -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>6&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M886.06,-375.56C877.87,-367.22 865.45,-356.49 852,-351.79 812.14,-337.87 124.49,-324.82 92,-351.79 68.07,-371.66 60.41,-463.5 58.03,-510.67\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"54.52,-510.67 57.56,-520.82 61.52,-510.99 54.52,-510.67\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-355.59\" font-family=\"Times,serif\" font-size=\"14.00\">(!__nv_out0 &amp; !__nv_out1 &amp; __nv_out2 &amp; !__nv_out3) | (!__nv_out0 &amp; __nv_out1 &amp; !__nv_out2 &amp; __nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;0 -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>7&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M886.06,-261.56C877.87,-253.22 865.45,-242.49 852,-237.79 812.14,-223.87 123.53,-209.71 92,-237.79 71.77,-255.8 61.44,-439.61 58.17,-510.82\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"54.67,-510.71 57.72,-520.86 61.67,-511.03 54.67,-510.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"472\" y=\"-241.59\" font-family=\"Times,serif\" font-size=\"14.00\">(__nv_out0 &amp; !__nv_out1 &amp; __nv_out2 &amp; !__nv_out3) | (__nv_out0 &amp; __nv_out1 &amp; !__nv_out2 &amp; __nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"1728\" cy=\"-196.79\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1728\" y=\"-193.09\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;1 -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>8&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M905.53,-209.36C911.14,-219.08 918.7,-232.98 924,-245.79 934.47,-271.13 919.97,-288.48 942,-304.79 1209.89,-503.15 1422.4,-500.82 1692,-304.79 1716.83,-286.74 1724.4,-250.68 1726.52,-225.2\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1730.03,-225.21 1727.14,-215.02 1723.04,-224.79 1730.03,-225.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-455.59\" font-family=\"Times,serif\" font-size=\"14.00\">(!__nv_out0 &amp; !__nv_out1 &amp; __nv_out3) | (__nv_out1 &amp; __nv_out2 &amp; !__nv_out3) | (!__nv_out2 &amp; __nv_out3)</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1724.03,-214.51C1720.06,-231.97 1711.15,-257.74 1692,-269.79 1656.74,-291.99 978.28,-290.29 942,-269.79 936.86,-266.89 921.01,-239.2 909.81,-218.78\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"912.75,-216.86 904.9,-209.75 906.6,-220.2 912.75,-216.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-289.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; __nv_in1 &amp; __nv_in2 &amp; !__nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1717.12,-211.14C1710.91,-218.83 1702.16,-227.58 1692,-231.79 1653.51,-247.74 981.34,-245.53 942,-231.79 932.12,-228.34 922.8,-221.64 915.3,-215.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"917.6,-212.38 907.94,-208.02 912.77,-217.45 917.6,-212.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-246.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1709.85,-196.79C1607.64,-196.79 1078.36,-196.79 934.26,-196.79\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"934.18,-193.29 924.18,-196.79 934.18,-200.29 934.18,-193.29\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-200.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; !__nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1712.69,-186.93C1706.6,-183.3 1699.24,-179.63 1692,-177.79 1611.23,-157.28 1023.61,-160.93 942,-177.79 935.16,-179.21 928.07,-181.74 921.63,-184.5\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"919.76,-181.51 912.18,-188.91 922.72,-187.86 919.76,-181.51\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-181.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1721.02,-180.07C1715.57,-167.59 1706.18,-151.42 1692,-143.79 1655.31,-124.05 979.72,-126.09 942,-143.79 928.33,-150.21 917.45,-163.19 909.92,-174.7\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"906.8,-173.09 904.61,-183.45 912.79,-176.71 906.8,-173.09\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-147.59\" font-family=\"Times,serif\" font-size=\"14.00\">__nv_in0 &amp; __nv_in1 &amp; !__nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1725.52,-178.82C1722.75,-158.18 1714.8,-125.2 1692,-109.79 1657.47,-86.47 977.49,-87.97 942,-109.79 920.29,-123.14 908.9,-150.88 903.2,-171.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"899.8,-170.64 900.77,-181.19 906.59,-172.33 899.8,-170.64\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-113.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; !__nv_in1 &amp; __nv_in2 &amp; __nv_in3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1724.58,-179.02C1719.96,-148.1 1708.83,-86.5 1692,-73.79 1559,26.64 1078.26,22.18 942,-73.79 911.42,-95.33 901.98,-140.17 899.13,-169.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"895.62,-169.44 898.33,-179.68 902.59,-169.98 895.62,-169.44\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1317\" y=\"-77.59\" font-family=\"Times,serif\" font-size=\"14.00\">!__nv_in0 &amp; __nv_in1 &amp; __nv_in2 &amp; !__nv_in3</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 0x7f936415f990> >"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "# Strategy torquesimple_acd as mealy machine\n",
+    "\n",
+    "aut = spot.automaton(\"\"\"HOA: v1\n",
+    "States: 2\n",
+    "Start: 0\n",
+    "AP: 11 \"u0accel0accel\" \"u0accel0f1dcon23p81b\" \"u0accel0f1dcon231b\" \"u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b\" \"u0gear0gear\" \"u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b\" \"u0steer0f1dsteering0angle0trackpos1b\" \"u0steer0steer\" \"p0p0gt0rpm0f1dcon5523231b\" \"p0p0lt0rpm0f1dcon32323231b\" \"p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b\"\n",
+    "acc-name: all\n",
+    "Acceptance: 0 t\n",
+    "properties: trans-labels explicit-labels state-acc deterministic\n",
+    "controllable-AP: 0 1 2 3 4 5 6 7\n",
+    "--BODY--\n",
+    "State: 0\n",
+    "[!0&!1&2&!3&4&!5&6&!7&!8&!9&!10] 0\n",
+    "[!0&1&!2&!3&4&!5&6&!7&!8&!9&10] 0\n",
+    "[!0&!1&2&!3&!4&5&6&!7&!8&9&!10] 0\n",
+    "[!0&1&!2&!3&!4&5&6&!7&!8&9&10] 0\n",
+    "[!0&!1&2&3&!4&!5&6&!7&8&!9&!10] 0\n",
+    "[!0&1&!2&3&!4&!5&6&!7&8&!9&10] 0\n",
+    "[!0&!1&2&!3&!4&5&!6&7&8&9 | !0&!1&2&!3&!4&5&6&!7&8&9 | !0&!1&2&!3&4&!5&!6&7&8&9 | !0&!1&2&!3&4&!5&6&!7&8&9 | !0&!1&2&3&!4&!5&!6&7&8&9 | !0&!1&2&3&!4&!5&6&!7&8&9 | !0&1&!2&!3&!4&5&!6&7&8&9 | !0&1&!2&!3&!4&5&6&!7&8&9 | !0&1&!2&!3&4&!5&!6&7&8&9 | !0&1&!2&!3&4&!5&6&!7&8&9 | !0&1&!2&3&!4&!5&!6&7&8&9 | !0&1&!2&3&!4&!5&6&!7&8&9 | 0&!1&!2&!3&!4&5&!6&7&8&9 | 0&!1&!2&!3&!4&5&6&!7&8&9 | 0&!1&!2&!3&4&!5&!6&7&8&9 | 0&!1&!2&!3&4&!5&6&!7&8&9 | 0&!1&!2&3&!4&!5&!6&7&8&9 | 0&!1&!2&3&!4&!5&6&!7&8&9] 1\n",
+    "State: 1\n",
+    "[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 1\n",
+    "--END--\"\"\")\n",
+    "\n",
+    "display(aut)\n",
+    "\n",
+    "# Convert to split mealy machine\n",
+    "auts = spot.split_2step(aut)\n",
+    "print(auts.to_str(\"hoa\"))\n",
+    "display(auts)\n",
+    "\n",
+    "# Relabel both, inputs and outputs\n",
+    "# You can choose the split option and stopping criteria as before\n",
+    "rel_dicts = spot.partitioned_game_relabel_here(auts, True, True, True, False, 10000, 10000)\n",
+    "print(auts.to_str(\"hoa\"))\n",
+    "display(auts)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "id": "7ec02ff5",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "HOA: v1\n",
+      "States: 9\n",
+      "Start: 0\n",
+      "AP: 11 \"u0accel0accel\" \"u0accel0f1dcon23p81b\" \"u0accel0f1dcon231b\" \"u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b\" \"u0gear0gear\" \"u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b\" \"u0steer0f1dsteering0angle0trackpos1b\" \"u0steer0steer\" \"p0p0gt0rpm0f1dcon5523231b\" \"p0p0lt0rpm0f1dcon32323231b\" \"p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b\"\n",
+      "acc-name: all\n",
+      "Acceptance: 0 t\n",
+      "properties: trans-labels explicit-labels state-acc deterministic\n",
+      "spot-state-player: 0 0 1 1 1 1 1 1 1\n",
+      "controllable-AP: 0 1 2 3 4 5 6 7\n",
+      "--BODY--\n",
+      "State: 0\n",
+      "[f] 2\n",
+      "[f] 3\n",
+      "[f] 4\n",
+      "[f] 5\n",
+      "[f] 6\n",
+      "[f] 7\n",
+      "[8&9] 8\n",
+      "[!8&!9&!10] 2\n",
+      "[!8&!9&10] 3\n",
+      "[!8&9&!10] 4\n",
+      "[!8&9&10] 5\n",
+      "[8&!9&!10] 6\n",
+      "[8&!9&10] 7\n",
+      "State: 1\n",
+      "[!8&!9&!10] 8\n",
+      "[!8&!9&10] 8\n",
+      "[!8&9&!10] 8\n",
+      "[!8&9&10] 8\n",
+      "[8&!9&!10] 8\n",
+      "[8&!9&10] 8\n",
+      "[8&9] 8\n",
+      "State: 2\n",
+      "[!0&!1&2&!3&4&!5&6&!7] 0\n",
+      "State: 3\n",
+      "[!0&1&!2&!3&4&!5&6&!7] 0\n",
+      "State: 4\n",
+      "[!0&!1&2&!3&!4&5&6&!7] 0\n",
+      "State: 5\n",
+      "[!0&1&!2&!3&!4&5&6&!7] 0\n",
+      "State: 6\n",
+      "[!0&!1&2&3&!4&!5&6&!7] 0\n",
+      "State: 7\n",
+      "[!0&1&!2&3&!4&!5&6&!7] 0\n",
+      "State: 8\n",
+      "[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 1\n",
+      "--END--\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=\"3282pt\" height=\"985pt\"\n",
+       " viewBox=\"0.00 0.00 3282.00 984.69\" 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 980.69)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-980.69 3278,-980.69 3278,4 -4,4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1637\" y=\"-961.49\" font-family=\"Times,serif\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"middle\" x=\"1637\" y=\"-946.49\" font-family=\"Times,serif\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"56\" cy=\"-531.69\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-527.99\" font-family=\"Times,serif\" 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,-531.69C2.67,-531.69 15.1,-531.69 27.63,-531.69\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"27.94,-535.19 37.94,-531.69 27.94,-528.19 27.94,-535.19\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-853.69 2034,-835.69 2061,-817.69 2088,-835.69 2061,-853.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-831.99\" font-family=\"Times,serif\" 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=\"M57.6,-549.85C59.93,-614.6 69.37,-831.41 92,-851.69 251.17,-994.4 1805.46,-888.78 2016,-851.69 2022.26,-850.59 2028.79,-848.67 2034.86,-846.53\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.4,-849.69 2044.48,-842.84 2033.89,-843.16 2036.4,-849.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-927.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.88,-549.72C60.98,-609.13 72.22,-796.04 92,-813.69 111.94,-831.49 1989.3,-831.65 2016,-832.69 2019.47,-832.83 2023.09,-833.01 2026.71,-833.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-836.71 2036.72,-833.85 2026.96,-829.73 2026.52,-836.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-836.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-739.69 2034,-721.69 2061,-703.69 2088,-721.69 2061,-739.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-717.99\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.22,-549.77C58.21,-595.46 63.52,-713.64 92,-737.69 132.83,-772.17 1963.37,-746.97 2016,-737.69 2022.26,-736.59 2028.79,-734.67 2034.86,-732.53\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.4,-735.69 2044.48,-728.84 2033.89,-729.16 2036.4,-735.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-758.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.01,-549.87C60.61,-589.34 69.04,-680.83 92,-699.69 112.65,-716.65 1989.3,-717.65 2016,-718.69 2019.47,-718.83 2023.09,-719.01 2026.71,-719.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-722.71 2036.72,-719.85 2026.96,-715.73 2026.52,-722.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-722.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-625.69 2034,-607.69 2061,-589.69 2088,-607.69 2061,-625.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-603.99\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;4 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>0&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.06,-549.9C60.41,-571.63 67.94,-607.11 92,-623.69 136,-654.03 1963.37,-632.97 2016,-623.69 2022.26,-622.59 2028.79,-620.67 2034.86,-618.53\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.4,-621.69 2044.48,-614.84 2033.89,-615.16 2036.4,-621.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-642.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;4 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>0&#45;&gt;4</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M62.81,-548.42C68.21,-561.15 77.61,-577.78 92,-585.69 138.83,-611.45 1962.59,-602.61 2016,-604.69 2019.47,-604.83 2023.09,-605.01 2026.71,-605.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-608.71 2036.72,-605.85 2026.96,-601.73 2026.52,-608.71\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-608.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>5</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-511.69 2034,-493.69 2061,-475.69 2088,-493.69 2061,-511.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-489.99\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.17,-531.67C261.19,-531.35 1914.98,-528.08 2016,-509.69 2022.25,-508.56 2028.79,-506.62 2034.85,-504.48\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.39,-507.64 2044.47,-500.8 2033.88,-501.1 2036.39,-507.64\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-534.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;5 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>0&#45;&gt;5</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M65.51,-516.21C71.56,-506.93 80.61,-495.94 92,-490.69 140.53,-468.31 1962.59,-488.87 2016,-490.69 2019.47,-490.81 2023.1,-490.98 2026.71,-491.18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-494.68 2036.72,-491.81 2026.96,-487.69 2026.52,-494.68\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-494.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-397.69 2034,-379.69 2061,-361.69 2088,-379.69 2061,-397.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-375.99\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;6 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>0&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.91,-513.53C57.88,-488.61 63.78,-444.53 92,-423.69 135,-391.95 1963.43,-405.35 2016,-395.69 2022.25,-394.55 2028.78,-392.61 2034.85,-390.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.38,-393.63 2044.47,-386.78 2033.88,-387.09 2036.38,-393.63\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-427.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;6 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>0&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M58.31,-513.78C61.44,-476.72 70.72,-393.7 92,-376.69 133.75,-343.32 1962.59,-374.87 2016,-376.69 2019.47,-376.81 2023.1,-376.98 2026.71,-377.18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-380.68 2036.72,-377.81 2026.96,-373.69 2026.52,-380.68\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-380.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-283.69 2034,-265.69 2061,-247.69 2088,-265.69 2061,-283.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-261.99\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;7 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>0&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.88,-513.37C57,-463.86 60.28,-329.24 92,-301.69 132.35,-266.65 1963.41,-291.24 2016,-281.69 2022.25,-280.56 2028.79,-278.63 2034.85,-276.49\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2036.39,-279.65 2044.47,-272.8 2033.88,-273.11 2036.39,-279.65\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-305.49\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;7 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>0&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.99,-513.69C61.33,-456.12 73.07,-279.32 92,-262.69 132.15,-227.42 1962.59,-260.87 2016,-262.69 2019.47,-262.81 2023.1,-262.98 2026.71,-263.18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2026.52,-266.68 2036.72,-263.81 2026.96,-259.69 2026.52,-266.68\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-266.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"2061,-207.69 2034,-189.69 2061,-171.69 2088,-189.69 2061,-207.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2061\" y=\"-185.99\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;8 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>0&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.45,-513.54C59.32,-445.56 67.54,-208.79 92,-186.69 390.19,82.78 1802.42,-145.58 2029.23,-184.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2028.68,-187.79 2039.12,-186.03 2029.86,-180.89 2028.68,-187.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-190.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2051.41,-823.81C2043.48,-813.94 2030.74,-800.59 2016,-794.69 1966.38,-774.84 132.22,-808.9 92,-773.69 60.57,-746.18 56.78,-617.93 56.71,-560.1\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"60.21,-559.86 56.73,-549.85 53.21,-559.84 60.21,-559.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-798.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;0 -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>3&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2051.41,-709.81C2043.48,-699.94 2030.73,-686.6 2016,-680.69 1966.39,-660.82 134.36,-690.29 92,-657.69 76.58,-645.82 66.11,-593.34 60.88,-559.97\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"64.32,-559.25 59.37,-549.88 57.39,-560.29 64.32,-559.25\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-684.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;0 -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>4&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2051.41,-595.81C2043.49,-585.93 2030.74,-572.58 2016,-566.69 1916.73,-527.04 196.33,-570.95 92,-547.69 88.5,-546.91 84.94,-545.76 81.48,-544.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"82.75,-541.16 72.19,-540.32 79.93,-547.56 82.75,-541.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-570.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;0 -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>5&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2049.59,-482.77C2041.34,-474.94 2029.04,-465.04 2016,-460.69 1965.3,-443.79 137.38,-432.47 92,-460.69 76.68,-470.22 67.87,-488.64 62.92,-504.33\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"59.51,-503.56 60.2,-514.13 66.25,-505.43 59.51,-503.56\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-464.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; !u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;0 -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>6&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2050.91,-368.26C2042.86,-359.11 2030.19,-346.97 2016,-341.69 1965.91,-323.06 133.07,-307.5 92,-341.69 67.67,-361.95 60.19,-455.67 57.94,-503.47\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"54.43,-503.61 57.5,-513.75 61.42,-503.91 54.43,-503.61\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-345.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; !u0accel0f1dcon23p81b &amp; u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;0 -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>7&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2050.98,-253.96C2042.96,-244.58 2030.32,-232.12 2016,-226.69 1966.03,-207.74 131.89,-191.12 92,-226.69 71.52,-244.96 61.34,-431.19 58.14,-503.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"54.64,-503.38 57.7,-513.52 61.63,-503.68 54.64,-503.38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1054\" y=\"-230.49\" font-family=\"Times,serif\" font-size=\"14.00\">!u0accel0accel &amp; u0accel0f1dcon23p81b &amp; !u0accel0f1dcon231b &amp; !u0gear0f1dmax0f1dcon241b0f1dsub0gear0f1dcon241b1b1b &amp; u0gear0f1dmin0f1dcon61b0f1dadd0gear0f1dcon241b1b1b &amp; !u0gear0gear &amp; u0steer0f1dsteering0angle0trackpos1b &amp; !u0steer0steer</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"3256\" cy=\"-189.69\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"3256\" y=\"-185.99\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;1 -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>8&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M2069.44,-202.3C2074.99,-212.04 2082.54,-225.95 2088,-238.69 2097.96,-261.95 2085.48,-277.9 2106,-292.69 2507.66,-582.19 2817.51,-581.02 3220,-292.69 3243.54,-275.83 3251.44,-242.22 3253.99,-217.98\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"3257.48,-218.16 3254.8,-207.91 3250.5,-217.6 3257.48,-218.16\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-512.49\" font-family=\"Times,serif\" font-size=\"14.00\">(label too long)</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3252.03,-207.41C3248.06,-224.87 3239.15,-250.64 3220,-262.69 3193.81,-279.18 2132.94,-277.91 2106,-262.69 2100.86,-259.79 2085.01,-232.1 2073.81,-211.67\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2076.75,-209.76 2068.9,-202.65 2070.6,-213.1 2076.75,-209.76\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-277.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3245.12,-204.04C3238.91,-211.73 3230.16,-220.48 3220,-224.69 3162.82,-248.38 2164.43,-245.1 2106,-224.69 2096.12,-221.24 2086.8,-214.54 2079.3,-207.92\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2081.6,-205.28 2071.94,-200.92 2076.77,-210.35 2081.6,-205.28\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-244.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3237.69,-189.69C3107.51,-189.69 2282.02,-189.69 2098.24,-189.69\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2098.03,-186.19 2088.03,-189.69 2098.03,-193.19 2098.03,-186.19\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-193.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3240.69,-179.83C3234.6,-176.2 3227.24,-172.53 3220,-170.69 3100.03,-140.23 2227.22,-145.64 2106,-170.69 2099.16,-172.11 2092.07,-174.64 2085.63,-177.4\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2083.76,-174.41 2076.18,-181.81 2086.72,-180.76 2083.76,-174.41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-174.49\" font-family=\"Times,serif\" font-size=\"14.00\">!p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3250.05,-172.55C3245,-158.52 3235.63,-139.59 3220,-130.69 3193.11,-115.38 2133.66,-116.82 2106,-130.69 2090.93,-138.25 2079.7,-153.7 2072.36,-166.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2069.16,-165.46 2067.71,-175.95 2075.39,-168.66 2069.16,-165.46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-134.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; !p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3253.7,-171.69C3251.11,-150.62 3243.33,-116.59 3220,-100.69 3168.85,-65.85 2158.57,-68.04 2106,-100.69 2083.95,-114.39 2072.62,-142.76 2067.02,-163.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2063.57,-163.2 2064.66,-173.74 2070.38,-164.83 2063.57,-163.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-104.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; !p0p0lt0rpm0f1dcon32323231b &amp; p0p0lt0speed0f1dsub0target2speed0f1dmultp0f1dabs0steer1b0f1dcon248881b1b1b</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;8 -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>1&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M3253.02,-171.92C3248.93,-138.84 3238.36,-69.88 3220,-55.69 3122.04,19.97 2206.25,16.91 2106,-55.69 2072.65,-79.85 2064.13,-130.09 2062.21,-161.73\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"2058.69,-161.93 2061.77,-172.07 2065.69,-162.22 2058.69,-161.93\"/>\n",
+       "<text text-anchor=\"middle\" x=\"2663\" y=\"-59.49\" font-family=\"Times,serif\" font-size=\"14.00\">p0p0gt0rpm0f1dcon5523231b &amp; p0p0lt0rpm0f1dcon32323231b</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 0x7f936415f990> >"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "# Undo relabel\n",
+    "spot.relabel_game_here(auts, rel_dicts)\n",
+    "print(auts.to_str(\"hoa\"))\n",
+    "display(auts)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "id": "48c2283b",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "True\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Check if we do actually obtain the same automaton\n",
+    "\n",
+    "print(spot.are_equivalent(aut, spot.unsplit_2step(auts)))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "id": "2b8d907e",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n",
+      "True\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Test all options for equivalence\n",
+    "for relabel_env in [True, False]:\n",
+    "    for relabel_player in [True, False]:\n",
+    "        for split_env in [True, False]:\n",
+    "            for split_player in [True, False]:\n",
+    "                auts = spot.split_2step(aut)\n",
+    "                rel_dicts = spot.partitioned_game_relabel_here(auts, relabel_env, relabel_player, split_env, split_player, 10000, 10000)\n",
+    "                spot.relabel_game_here(auts, rel_dicts)\n",
+    "                print(spot.are_equivalent(aut, spot.unsplit_2step(auts)))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "17a32a72",
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {
diff --git a/tests/python/except.py b/tests/python/except.py
index e531882dd..03076c01b 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -373,4 +373,22 @@ except RuntimeError as e:
     tc.assertIn("The given prefix for new variables",
                 str(e))
 else:
-    report_missing_exception()
\ No newline at end of file
+    report_missing_exception()
+
+# Relabeling games must not use the
+# globally reserved aps
+aut = spot.make_twa_graph()
+aut.new_states(2)
+apin = buddy.bdd_ithvar(aut.register_ap("__AP_IN__"))
+apout = buddy.bdd_ithvar(aut.register_ap("__AP_OUT__"))
+aut.new_edge(0,1,apin & apout)
+aut.new_edge(1,0,buddy.bdd_not(apin & apout))
+spot.set_state_players(aut, [False, True])
+
+try:
+    spot.partitioned_game_relabel_here(aut, True, True)
+except RuntimeError as e:
+    tc.assertIn("You can not use __AP_IN__ or __AP_OUT__",
+                str(e))
+else:
+    report_missing_exception()