diff --git a/doc/org/tut24.org b/doc/org/tut24.org
index 8768053e8..220ff2796 100644
--- a/doc/org/tut24.org
+++ b/doc/org/tut24.org
@@ -107,7 +107,7 @@ for (unsigned s = 0; s < n; ++s)
 
 #+RESULTS: nonalt-one
 #+begin_example
-Initial state: 4294967292
+Initial state: 4294967295
 State 0:
   edge(0 -> 0)
     label = a
diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy
index 0ec23f95d..047ed40fc 100644
--- a/spot/parseaut/parseaut.yy
+++ b/spot/parseaut/parseaut.yy
@@ -2423,6 +2423,8 @@ namespace spot
     fix_acceptance(r);
     fix_initial_state(r);
     fix_properties(r);
+    if (r.h->aut && r.h->aut->is_alternating())
+      r.h->aut->merge_univ_dests();
     return r.h;
   };
 
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index 018268def..4fcae4d31 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -43,10 +43,66 @@ namespace spot
     delete namer;
   }
 
+    /// \brief Merge universal destinations
+    ///
+    /// If several states have the same universal destination, merge
+    /// them all.  Also remove unused destination, and any redundant
+    /// state in each destination.
+  void twa_graph::merge_univ_dests()
+  {
+    auto& g = get_graph();
+    auto& dests = g.dests_vector();
+    auto& edges = g.edge_vector();
+
+    std::vector<unsigned> old_dests;
+    std::swap(dests, old_dests);
+    std::vector<unsigned> seen(old_dests.size(), -1U);
+    std::map<std::vector<unsigned>, unsigned> uniq;
+
+    auto fixup = [&](unsigned& in_dst)
+      {
+        unsigned dst = in_dst;
+        if ((int) dst >= 0)       // not a universal edge
+          return;
+        dst = ~dst;
+        unsigned& nd = seen[dst];
+        if (nd == -1U)
+          {
+            std::vector<unsigned>
+              tmp(old_dests.data() + dst + 1,
+                  old_dests.data() + dst + 1 + old_dests[dst]);
+            std::sort(tmp.begin(), tmp.end());
+            tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
+            auto p = uniq.emplace(tmp, 0);
+            if (!p.second)
+              {
+                nd = p.first->second;
+              }
+            else
+              {
+                nd = g.new_univ_dests(tmp.begin(), tmp.end());
+                p.first->second = nd;
+              }
+          }
+        in_dst = nd;
+      };
+
+    unsigned tend = edges.size();
+    for (unsigned t = 1; t < tend; t++)
+      {
+        if (g.is_dead_edge(t))
+          continue;
+        fixup(edges[t].dst);
+      }
+    fixup(init_number_);
+  }
+
   void twa_graph::merge_edges()
   {
     set_named_prop("highlight-edges", nullptr);
     g_.remove_dead_edges_();
+    if (is_alternating())
+      merge_univ_dests();
 
     typedef graph_t::edge_storage_t tr_t;
     g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index 8df858da5..ccab488ab 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -521,6 +521,11 @@ namespace spot
     /// extremities and acceptance.
     void merge_edges();
 
+    /// \brief marge common universal destination
+    ///
+    /// This is already called by merge_edges().
+    void merge_univ_dests();
+
     /// \brief Remove all dead states
     ///
     /// Dead states are all the states that cannot be part of
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index aa808d97f..274fa9031 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -360,10 +360,14 @@ namespace spot
         return bdd_format_formula(aut_->get_dict(), label);
       }
 
+      std::set<int> done;
+
       void
       print_dst(int dst, const char* style = nullptr)
       {
-        os_ << "    " << dst << " [label=<>,width=0,height=0,shape=none]\n";
+        if (!done.emplace(dst).second)
+          return;
+        os_ << "    " << dst << " [label=<>,shape=point]\n";
         for (unsigned d: aut_->univ_dests(dst))
           {
             os_ << "    " << dst << " -> " << d;
@@ -465,7 +469,7 @@ namespace spot
           }
         else
           {
-            os_ << " [dir=none]\n";
+            os_ << " [arrowhead=onormal]\n";
             print_dst(init);
           }
       }
@@ -626,11 +630,10 @@ namespace spot
                 os_ << ", " << highlight;
               }
           }
-        // No arrow tip of the common part of a universal transition
-        if ((int)t.dst < 0)
-          os_ << ", dir=none";
+        if (aut_->is_univ_dest(t.dst))
+          os_ << ", arrowhead=onormal";
         os_ << "]\n";
-        if ((int)t.dst < 0)     // Universal destination
+        if (aut_->is_univ_dest(t.dst))
           print_dst(t.dst, highlight.c_str());
       }
 
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 345dd7203..65343b2a4 100644
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -61,34 +61,34 @@ digraph G {
   label="Fin(⓿)"
   labelloc="t"
   I [label="", style=invis, width=0]
-  I -> -11 [dir=none]
-    -11 [label=<>,width=0,height=0,shape=none]
+  I -> -11 [arrowhead=onormal]
+    -11 [label=<>,shape=point]
     -11 -> 0
     -11 -> 2
   subgraph cluster_0 {
   color=green
   label=""
-  6 [label="t"]
+  2 [label="G(a)"]
   }
   subgraph cluster_1 {
   color=red
   label=""
-  4 [label="F(b)\n⓿"]
+  1 [label="FG(a)\n⓿"]
   }
   subgraph cluster_2 {
   color=green
   label=""
-  3 [label="GF(b)"]
+  6 [label="t"]
   }
   subgraph cluster_3 {
-  color=green
-  label=""
-  2 [label="G(a)"]
-  }
-  subgraph cluster_4 {
   color=red
   label=""
-  1 [label="FG(a)\n⓿"]
+  4 [label="F(b)\n⓿"]
+  }
+  subgraph cluster_4 {
+  color=green
+  label=""
+  3 [label="GF(b)"]
   }
   subgraph cluster_5 {
   color=red
@@ -100,23 +100,23 @@ digraph G {
   label=""
   0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
   }
-  0 -> -1 [label="b", dir=none]
-    -1 [label=<>,width=0,height=0,shape=none]
-    -1 -> 3
+  0 -> -1 [label="b", arrowhead=onormal]
+    -1 [label=<>,shape=point]
     -1 -> 1
-  0 -> -4 [label="a & !b", style=bold, color="#F15854", dir=none]
-    -4 [label=<>,width=0,height=0,shape=none]
-    -4 -> 5 [style=bold, color="#F15854"]
-    -4 -> 3 [style=bold, color="#F15854"]
+    -1 -> 3
+  0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal]
+    -4 [label=<>,shape=point]
     -4 -> 1 [style=bold, color="#F15854"]
+    -4 -> 3 [style=bold, color="#F15854"]
+    -4 -> 5 [style=bold, color="#F15854"]
   1 -> 2 [label="a"]
   1 -> 1 [label="1"]
   2 -> 2 [label="a"]
   3 -> 3 [label="b"]
-  3 -> -8 [label="!b", style=bold, color="#FAA43A", dir=none]
-    -8 [label=<>,width=0,height=0,shape=none]
-    -8 -> 4 [style=bold, color="#FAA43A"]
+  3 -> -8 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal]
+    -8 [label=<>,shape=point]
     -8 -> 3 [style=bold, color="#FAA43A"]
+    -8 -> 4 [style=bold, color="#FAA43A"]
   4 -> 6 [label="b"]
   4 -> 4 [label="!b"]
   5 -> 6 [label="b"]
@@ -147,7 +147,7 @@ AP: 1 "a"
 properties: trans-labels explicit-labels state-acc univ-branch very-weak
 --BODY--
 State: 0 "GF(a)"
- [t] 1&0
+ [t] 0&1
 State: 1 "F(a)" {0}
  [(0)] 2
  [t] 1
@@ -172,7 +172,7 @@ properties: univ-branch trans-labels explicit-labels state-acc complete
 properties: very-weak
 --BODY--
 State: 0 {0}
-[t] 1&0
+[t] 0&1
 State: 1
 [0] 2
 [t] 1
diff --git a/tests/core/complete.test b/tests/core/complete.test
index e69042b79..007e86747 100755
--- a/tests/core/complete.test
+++ b/tests/core/complete.test
@@ -203,7 +203,7 @@ properties: deterministic very-weak
 --BODY--
 State: 0
 [!0 | 1] 0
-[0&!1] 1&0
+[0&!1] 0&1
 State: 1 {0}
 [0&!1] 1
 [!0 | 1] 1
diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test
index 0cdf97ea6..270624432 100755
--- a/tests/core/parseaut.test
+++ b/tests/core/parseaut.test
@@ -1946,7 +1946,7 @@ State: 5 "F!((c2))" {0}
 [t] 5
 State: 6 "GF!((c1))"
 [!1] 6
-[t] 7&6
+[t] 6&7
 State: 7 "F!((c1))" {0}
 [!1] 11
 [t] 7
@@ -1954,9 +1954,9 @@ State: 8 "((!((c1)) U (!((c1)) && !((p1)))) R F!((p2)))"
 [!0&!1&!2] 11
 [!1&!2] 10
 [!0&!1] 9
-[!1] 10&9
+[!1] 9&10
 [!0] 8
-[t] 10&8
+[t] 8&10
 State: 9 "(!((c1)) U (!((c1)) && !((p1))))" {0}
 [!1&!2] 11
 [!1] 9
@@ -2407,8 +2407,8 @@ properties: univ-branch trans-labels explicit-labels state-acc
 properties: very-weak
 --BODY--
 State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
-[0] 3&1
-[!0&1] 5&3&1
+[0] 1&3
+[!0&1] 1&3&5
 State: 1 "FG(a)" {0}
 [1] 2
 [t] 1
@@ -2416,7 +2416,7 @@ State: 2 "G(a)"
 [1] 2
 State: 3 "GF(b)"
 [0] 3
-[!0] 4&3
+[!0] 3&4
 State: 4 "F(b)" {0}
 [0] 6
 [!0] 4
@@ -2438,18 +2438,18 @@ properties: deterministic
 State: 0
 [!0&!1] 0&1
 [0&!1] 1
-[!0&1] 0&2&1
+[!0&1] 0&1&2
 [0&1] 0&1
 State: 1
 [!0&!1] 0&1
-[0&!1] 2&1
+[0&!1] 1&2
 [!0&1] 2
-[0&1] 1&1
+[0&1] 1
 State: 2
 [!0&!1] 0&1
-[0&!1] 2&1
+[0&!1] 1&2
 [!0&1] 2
-[0&1] 0&2&1
+[0&1] 0&1&2
 --END--
 EOF
 
@@ -2613,8 +2613,8 @@ properties: univ-branch trans-labels explicit-labels state-acc
 properties: very-weak
 --BODY--
 State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
-[0] 3&1
-[!0&1] 5&3&1
+[0] 1&3
+[!0&1] 1&3&5
 State: 1 "FG(a)" {0}
 [1] 2
 [t] 1
@@ -2622,7 +2622,7 @@ State: 2 "G(a)"
 [1] 2
 State: 3 "GF(b)"
 [0] 3
-[!0] 4&3
+[!0] 3&4
 State: 4 "F(b)" {0}
 [0] 6
 [!0] 4
@@ -2644,18 +2644,18 @@ properties: deterministic
 State: 0
 [!0&!1] 0&1
 [0&!1] 1
-[!0&1] 0&2&1
+[!0&1] 0&1&2
 [0&1] 0&1
 State: 1
 [!0&!1] 0&1
-[0&!1] 2&1
+[0&!1] 1&2
 [!0&1] 2
-[0&1] 1&1
+[0&1] 1
 State: 2
 [!0&!1] 0&1
-[0&!1] 2&1
+[0&!1] 1&2
 [!0&1] 2
-[0&1] 0&2&1
+[0&1] 0&1&2
 --END--
 EOF
 
diff --git a/tests/python/_altscc.ipynb b/tests/python/_altscc.ipynb
index d448119ef..1a5da1624 100644
--- a/tests/python/_altscc.ipynb
+++ b/tests/python/_altscc.ipynb
@@ -41,7 +41,7 @@
      "language": "python",
      "metadata": {},
      "outputs": [],
-     "prompt_number": 2
+     "prompt_number": 1
     },
     {
      "cell_type": "code",
@@ -69,7 +69,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 12,
+       "prompt_number": 2,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -77,77 +77,78 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"219pt\" height=\"154pt\"\n",
-        " viewBox=\"0.00 0.00 219.00 154.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"222pt\" height=\"154pt\"\n",
+        " viewBox=\"0.00 0.00 221.60 154.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 1) rotate(0) translate(4 150)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-150 215,-150 215,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"84.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
-        "<text text-anchor=\"start\" x=\"106.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"122.5\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-150 217.6,-150 217.6,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"85.8\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+        "<text text-anchor=\"start\" x=\"107.8\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"123.8\" y=\"-131.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" stroke=\"green\" points=\"151,-8 151,-108 203,-108 203,-8 151,-8\"/>\n",
+        "<polygon fill=\"none\" stroke=\"green\" points=\"153.6,-8 153.6,-108 205.6,-108 205.6,-8 153.6,-8\"/>\n",
         "</g>\n",
         "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" stroke=\"red\" points=\"68,-30 68,-115 120,-115 120,-30 68,-30\"/>\n",
+        "<polygon fill=\"none\" stroke=\"red\" points=\"70.6,-30 70.6,-115 122.6,-115 122.6,-30 70.6,-30\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- &#45;1 -->\n",
         "<g id=\"node2\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"39,-27.5 38,-27.5 38,-26.5 39,-26.5 39,-27.5\"/>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"39.8\" cy=\"-27\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
         "<!-- I&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.10614,-27C3.20855,-27 35.8616,-27 37.9003,-27\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.10844,-27C2.6468,-27 20.196,-27 30.7973,-27\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"30.9213,-29.4501 37.9213,-27 30.9212,-24.5501 30.9213,-29.4501\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"94\" cy=\"-56\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"94\" y=\"-52.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"96.6\" cy=\"-56\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"96.6\" y=\"-52.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.1549,-27.0832C40.9145,-28.0282 57.3371,-36.8477 71.5878,-44.5008\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"77.9221,-47.9026 70.2648,-47.3658 74.8386,-46.2466 71.7551,-44.5907 71.7551,-44.5907 71.7551,-44.5907 74.8386,-46.2466 73.2455,-41.8155 77.9221,-47.9026 77.9221,-47.9026\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M41.7512,-27.5033C45.6352,-29.5588 60.7141,-37.5385 73.9308,-44.5327\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"80.2121,-47.8568 72.5516,-47.3667 77.1186,-46.2197 74.025,-44.5826 74.025,-44.5826 74.025,-44.5826 77.1186,-46.2197 75.4985,-41.7984 80.2121,-47.8568 80.2121,-47.8568\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"177\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"177\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"179.6\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"179.6\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.0466,-26.9978C40.0034,-26.9519 55.5083,-26.2153 68,-26 91.1077,-25.6017 96.947,-24.3617 120,-26 130.461,-26.7434 141.938,-28.2585 151.763,-29.7722\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"158.911,-30.9167 151.501,-32.9203 155.455,-30.3633 151.999,-29.8099 151.999,-29.8099 151.999,-29.8099 155.455,-30.3633 152.497,-26.6995 158.911,-30.9167 158.911,-30.9167\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M41.9364,-26.9481C45.8913,-26.7705 59.4203,-26.1875 70.6,-26 93.7079,-25.6124 99.547,-24.3617 122.6,-26 133.061,-26.7434 144.538,-28.2585 154.363,-29.7722\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"161.511,-30.9167 154.101,-32.9203 158.055,-30.3633 154.599,-29.8099 154.599,-29.8099 154.599,-29.8099 158.055,-30.3633 155.097,-26.6995 161.511,-30.9167 161.511,-30.9167\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M87.6208,-73.0373C86.3189,-82.8579 88.4453,-92 94,-92 98.166,-92 100.404,-86.8576 100.713,-80.1433\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"100.379,-73.0373 103.854,-79.8818 100.543,-76.5335 100.708,-80.0296 100.708,-80.0296 100.708,-80.0296 100.543,-76.5335 97.561,-80.1774 100.379,-73.0373 100.379,-73.0373\"/>\n",
-        "<text text-anchor=\"start\" x=\"90.5\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M90.2208,-73.0373C88.9189,-82.8579 91.0453,-92 96.6,-92 100.766,-92 103.004,-86.8576 103.313,-80.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"102.979,-73.0373 106.454,-79.8818 103.143,-76.5335 103.308,-80.0296 103.308,-80.0296 103.308,-80.0296 103.143,-76.5335 100.161,-80.1774 102.979,-73.0373 102.979,-73.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"93.1\" y=\"-95.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M111.783,-51.4416C123.591,-48.2346 139.551,-43.8996 152.606,-40.3538\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"159.515,-38.4773 153.586,-43.352 156.138,-39.3947 152.76,-40.3121 152.76,-40.3121 152.76,-40.3121 156.138,-39.3947 151.934,-37.2723 159.515,-38.4773 159.515,-38.4773\"/>\n",
-        "<text text-anchor=\"start\" x=\"130\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M114.383,-51.4416C126.191,-48.2346 142.151,-43.8996 155.206,-40.3538\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"162.115,-38.4773 156.186,-43.352 158.738,-39.3947 155.36,-40.3121 155.36,-40.3121 155.36,-40.3121 158.738,-39.3947 154.534,-37.2723 162.115,-38.4773 162.115,-38.4773\"/>\n",
+        "<text text-anchor=\"start\" x=\"132.6\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M169.969,-50.6641C168.406,-60.625 170.75,-70 177,-70 181.688,-70 184.178,-64.7266 184.471,-57.8876\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"184.031,-50.6641 187.601,-57.4598 184.244,-54.1576 184.456,-57.6511 184.456,-57.6511 184.456,-57.6511 184.244,-54.1576 181.312,-57.8425 184.031,-50.6641 184.031,-50.6641\"/>\n",
-        "<text text-anchor=\"start\" x=\"172.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "<text text-anchor=\"start\" x=\"169\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M172.569,-50.6641C171.006,-60.625 173.35,-70 179.6,-70 184.288,-70 186.778,-64.7266 187.071,-57.8876\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"186.631,-50.6641 190.201,-57.4598 186.844,-54.1576 187.056,-57.6511 187.056,-57.6511 187.056,-57.6511 186.844,-54.1576 183.912,-57.8425 186.631,-50.6641 186.631,-50.6641\"/>\n",
+        "<text text-anchor=\"start\" x=\"175.1\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "<text text-anchor=\"start\" x=\"171.6\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76dc5d7090> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7620378330> >"
        ]
       }
      ],
-     "prompt_number": 12
+     "prompt_number": 2
     },
     {
      "cell_type": "markdown",
@@ -180,7 +181,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 17,
+       "prompt_number": 3,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -188,84 +189,72 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"151pt\" height=\"192pt\"\n",
-        " viewBox=\"0.00 0.00 151.00 192.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"154pt\" height=\"192pt\"\n",
+        " viewBox=\"0.00 0.00 153.60 192.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 1) rotate(0) translate(4 188)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-188 147,-188 147,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"49\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"74\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"90\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-188 149.6,-188 149.6,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"50.3\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"75.3\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"91.3\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" stroke=\"green\" points=\"83,-8 83,-93 135,-93 135,-8 83,-8\"/>\n",
+        "<polygon fill=\"none\" stroke=\"green\" points=\"85.6,-8 85.6,-93 137.6,-93 137.6,-8 85.6,-8\"/>\n",
         "</g>\n",
         "<g id=\"clust2\" class=\"cluster\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" stroke=\"red\" points=\"83,-101 83,-153 135,-153 135,-101 83,-101\"/>\n",
+        "<polygon fill=\"none\" stroke=\"red\" points=\"85.6,-101 85.6,-153 137.6,-153 137.6,-101 85.6,-101\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
-        "<!-- &#45;4 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>&#45;4</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"39,-47.5 38,-47.5 38,-46.5 39,-46.5 39,-47.5\"/>\n",
+        "<!-- &#45;1 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>&#45;1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"39.8\" cy=\"-82\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
-        "<!-- I&#45;&gt;&#45;4 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;&#45;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.10614,-47C3.20855,-47 35.8616,-47 37.9003,-47\"/>\n",
+        "<!-- I&#45;&gt;&#45;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;&#45;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.10844,-82C2.6468,-82 20.196,-82 30.7973,-82\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"30.9213,-84.4501 37.9213,-82 30.9212,-79.5501 30.9213,-84.4501\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"109\" cy=\"-127\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"109\" y=\"-123.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"111.6\" cy=\"-127\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"111.6\" y=\"-123.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
-        "<!-- &#45;4&#45;&gt;0 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>&#45;4&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.05,-47.058C40.4721,-48.7067 71.8975,-85.142 91.8267,-108.248\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"96.6206,-113.806 89.6633,-110.563 94.3346,-111.156 92.0486,-108.506 92.0486,-108.506 92.0486,-108.506 94.3346,-111.156 94.434,-106.448 96.6206,-113.806 96.6206,-113.806\"/>\n",
+        "<!-- &#45;1&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M41.2389,-83.4339C42.8255,-88.3703 48.7502,-104.807 59.6,-113 67.3475,-118.85 77.3952,-122.256 86.5214,-124.239\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"93.5814,-125.543 86.1255,-127.369 90.1396,-124.907 86.6979,-124.272 86.6979,-124.272 86.6979,-124.272 90.1396,-124.907 87.2703,-121.174 93.5814,-125.543 93.5814,-125.543\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"109\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"109\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"111.6\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"111.6\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
-        "<!-- &#45;4&#45;&gt;1 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>&#45;4&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.05,-46.9906C40.3003,-46.755 64.7431,-42.1498 84.1745,-38.4889\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"91.0544,-37.1926 84.7587,-41.5843 87.6149,-37.8407 84.1755,-38.4888 84.1755,-38.4888 84.1755,-38.4888 87.6149,-37.8407 83.5922,-35.3932 91.0544,-37.1926 91.0544,-37.1926\"/>\n",
-        "</g>\n",
-        "<!-- &#45;1 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"39,-109.5 38,-109.5 38,-108.5 39,-108.5 39,-109.5\"/>\n",
+        "<!-- &#45;1&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M41.5839,-81.4609C46.3474,-78.1852 71.8242,-60.6653 90.4426,-47.8618\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"96.4539,-43.728 92.471,-50.2899 93.57,-45.7112 90.6861,-47.6944 90.6861,-47.6944 90.6861,-47.6944 93.57,-45.7112 88.9012,-45.0989 96.4539,-43.728 96.4539,-43.728\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M90.5814,-126.381C80.5252,-125.592 67.7752,-123.842 57,-120 48.7209,-117.048 40.1448,-109.963 39.1051,-109.089\"/>\n",
-        "<text text-anchor=\"start\" x=\"61.5\" y=\"-142.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
-        "<text text-anchor=\"start\" x=\"57\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M98.8419,-113.981C94.4601,-108.857 89.5866,-102.816 85.6,-97 80.4256,-89.4515 83.4876,-83.6411 75.6,-79 67.3683,-74.1565 56.0932,-76.4083 48.6353,-78.8582\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"47.3759,-76.7198 41.7465,-81.5482 49.1582,-81.2841 47.3759,-76.7198\"/>\n",
+        "<text text-anchor=\"start\" x=\"64.1\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"59.6\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M101.332,-50.2903C99.4831,-60.3892 102.039,-70 109,-70 114.221,-70 116.964,-64.5939 117.229,-57.6304\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"116.668,-50.2903 120.342,-57.0299 116.935,-53.7801 117.201,-57.2699 117.201,-57.2699 117.201,-57.2699 116.935,-53.7801 114.06,-57.5099 116.668,-50.2903 116.668,-50.2903\"/>\n",
-        "<text text-anchor=\"start\" x=\"104.5\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "</g>\n",
-        "<!-- &#45;1&#45;&gt;0 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.05,-109.013C40.3075,-109.341 65.0281,-115.79 84.5129,-120.873\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"91.4014,-122.67 83.833,-123.951 88.0148,-121.786 84.6281,-120.903 84.6281,-120.903 84.6281,-120.903 88.0148,-121.786 85.4233,-117.855 91.4014,-122.67 91.4014,-122.67\"/>\n",
-        "</g>\n",
-        "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.05,-108.946C40.457,-107.416 71.2357,-73.9612 91.1902,-52.2715\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"96.0058,-47.0372 93.5845,-54.3215 93.636,-49.613 91.2663,-52.1888 91.2663,-52.1888 91.2663,-52.1888 93.636,-49.613 88.9481,-50.056 96.0058,-47.0372 96.0058,-47.0372\"/>\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M103.932,-50.2903C102.083,-60.3892 104.639,-70 111.6,-70 116.821,-70 119.564,-64.5939 119.829,-57.6304\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"119.268,-50.2903 122.942,-57.0299 119.535,-53.7801 119.801,-57.2699 119.801,-57.2699 119.801,-57.2699 119.535,-53.7801 116.66,-57.5099 119.268,-50.2903 119.268,-50.2903\"/>\n",
+        "<text text-anchor=\"start\" x=\"107.1\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76dc5d71b0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7620378870> >"
        ]
       }
      ],
-     "prompt_number": 17
+     "prompt_number": 3
     },
     {
      "cell_type": "code",
@@ -292,7 +281,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 16,
+       "prompt_number": 4,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -300,87 +289,75 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"219pt\" height=\"199pt\"\n",
-        " viewBox=\"0.00 0.00 219.00 198.77\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 194.773)\">\n",
+        "<svg width=\"181pt\" height=\"170pt\"\n",
+        " viewBox=\"0.00 0.00 181.00 169.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 165.8)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-194.773 215,-194.773 215,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"83\" y=\"-176.573\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"108\" y=\"-176.573\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"124\" y=\"-176.573\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-165.8 177,-165.8 177,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"64\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"89\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"105\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" stroke=\"green\" points=\"68,-59.7728 68,-159.773 203,-159.773 203,-59.7728 68,-59.7728\"/>\n",
+        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-8 30,-108 165,-108 165,-8 30,-8\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
-        "<!-- &#45;4 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>&#45;4</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"39,-57.2728 38,-57.2728 38,-56.2728 39,-56.2728 39,-57.2728\"/>\n",
+        "<!-- &#45;1 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>&#45;1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-137\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
-        "<!-- I&#45;&gt;&#45;4 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;&#45;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.10614,-56.7728C3.20855,-56.7728 35.8616,-56.7728 37.9003,-56.7728\"/>\n",
+        "<!-- I&#45;&gt;&#45;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;&#45;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-137C3.52733,-137 32.5548,-137 46.9758,-137\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"47.1189,-139.45 54.1189,-137 47.1188,-134.55 47.1189,-139.45\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"94\" cy=\"-85.7728\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"94\" y=\"-82.0728\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-34\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-30.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
-        "<!-- &#45;4&#45;&gt;0 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>&#45;4&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.1549,-56.856C40.9145,-57.8009 57.3371,-66.6205 71.5878,-74.2736\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"77.9221,-77.6754 70.2648,-77.1386 74.8386,-76.0194 71.7551,-74.3634 71.7551,-74.3634 71.7551,-74.3634 74.8386,-76.0194 73.2455,-71.5883 77.9221,-77.6754 77.9221,-77.6754\"/>\n",
+        "<!-- &#45;1&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M56,-135.01C56,-109.75 56,-84.4902 56,-59.2301\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"56,-52.1055 59.1501,-59.1054 56,-55.6055 56.0001,-59.1055 56.0001,-59.1055 56.0001,-59.1055 56,-55.6055 52.8501,-59.1055 56,-52.1055 56,-52.1055\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"177\" cy=\"-85.7728\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"177\" y=\"-82.0728\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-82\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"139\" y=\"-78.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
-        "<!-- &#45;4&#45;&gt;1 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>&#45;4&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M39.1194,-56.759C41.5706,-56.4798 81.2702,-52.1167 112,-58.7728 126.718,-61.9607 142.306,-68.4629 154.412,-74.2876\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"160.753,-77.4284 153.082,-77.1437 157.616,-75.8748 154.48,-74.3211 154.48,-74.3211 154.48,-74.3211 157.616,-75.8748 155.878,-71.4984 160.753,-77.4284 160.753,-77.4284\"/>\n",
+        "<!-- &#45;1&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M58.1975,-136.505C63.6262,-134.235 86.3798,-124.441 103,-113 108.892,-108.944 114.875,-104.007 120.188,-99.2761\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"125.655,-94.275 122.616,-101.324 123.072,-96.6375 120.49,-99.0001 120.49,-99.0001 120.49,-99.0001 123.072,-96.6375 118.364,-96.676 125.655,-94.275 125.655,-94.275\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M87.6208,-102.81C86.3189,-112.631 88.4453,-121.773 94,-121.773 98.166,-121.773 100.404,-116.63 100.713,-109.916\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"100.379,-102.81 103.854,-109.655 100.543,-106.306 100.708,-109.802 100.708,-109.802 100.708,-109.802 100.543,-106.306 97.561,-109.95 100.379,-102.81 100.379,-102.81\"/>\n",
-        "<text text-anchor=\"start\" x=\"90.5\" y=\"-140.573\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
-        "<text text-anchor=\"start\" x=\"86\" y=\"-125.573\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-51.0373C48.3189,-60.8579 50.4453,-70 56,-70 60.166,-70 62.4036,-64.8576 62.7128,-58.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-51.0373 65.8541,-57.8818 62.5434,-54.5335 62.7076,-58.0296 62.7076,-58.0296 62.7076,-58.0296 62.5434,-54.5335 59.561,-58.1774 62.3792,-51.0373 62.3792,-51.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"52.5\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M112.178,-85.7728C123.669,-85.7728 138.959,-85.7728 151.693,-85.7728\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"158.847,-85.7728 151.847,-88.9229 155.347,-85.7728 151.847,-85.7729 151.847,-85.7729 151.847,-85.7729 155.347,-85.7728 151.847,-82.6229 158.847,-85.7728 158.847,-85.7728\"/>\n",
-        "<text text-anchor=\"start\" x=\"130\" y=\"-89.5728\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
-        "</g>\n",
-        "<!-- &#45;1 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"94.5,-11.2728 93.5,-11.2728 93.5,-10.2728 94.5,-10.2728 94.5,-11.2728\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M72.6567,-41.0787C81.7089,-45.355 93.2089,-51.105 103,-57 108.128,-60.0874 113.476,-63.6923 118.403,-67.188\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"124.372,-71.5104 116.855,-69.9558 121.537,-69.4575 118.702,-67.4046 118.702,-67.4046 118.702,-67.4046 121.537,-69.4575 120.55,-64.8533 124.372,-71.5104 124.372,-71.5104\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M173.048,-67.9081C169.091,-50.2821 160.197,-24.2233 141,-11.7728 124.379,-0.993136 96.7913,-10.1606 95.0833,-10.7441\"/>\n",
-        "<text text-anchor=\"start\" x=\"131\" y=\"-15.5728\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "</g>\n",
-        "<!-- &#45;1&#45;&gt;0 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M94,-11.3587C94,-27.8063 94,-44.254 94,-60.7016\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"94,-67.7506 90.8501,-60.7506 94,-64.2506 94.0001,-60.7506 94.0001,-60.7506 94.0001,-60.7506 94,-64.2506 97.1501,-60.7507 94,-67.7506 94,-67.7506\"/>\n",
-        "</g>\n",
-        "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M95.083,-10.7203C96.7853,-9.65207 124.283,7.26784 141,-3.77277 160.012,-16.3291 168.732,-41.5556 172.71,-60.7309\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"174.014,-67.7447 169.637,-61.4385 173.374,-64.3037 172.734,-60.8627 172.734,-60.8627 172.734,-60.8627 173.374,-64.3037 175.831,-60.2868 174.014,-67.7447 174.014,-67.7447\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M120.788,-83.8666C111.67,-85.4769 100.608,-88.4653 92,-94 84.4423,-98.8591 69.2944,-119.499 61.6458,-130.319\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"59.6115,-128.953 57.6175,-136.096 63.6309,-131.756 59.6115,-128.953\"/>\n",
+        "<text text-anchor=\"start\" x=\"93\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76dc5d7180> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7620378390> >"
        ]
       }
      ],
-     "prompt_number": 16
+     "prompt_number": 4
     },
     {
      "cell_type": "code",
@@ -407,7 +384,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 30,
+       "prompt_number": 5,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -415,74 +392,75 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"186pt\" height=\"153pt\"\n",
-        " viewBox=\"0.00 0.00 186.00 152.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 148.5)\">\n",
+        "<svg width=\"186pt\" height=\"155pt\"\n",
+        " viewBox=\"0.00 0.00 186.00 154.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 150.8)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-148.5 182,-148.5 182,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"66.5\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"91.5\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"107.5\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-150.8 182,-150.8 182,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"66.5\" y=\"-132.6\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"91.5\" y=\"-132.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"107.5\" y=\"-132.6\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-28.5 30,-113.5 170,-113.5 170,-28.5 30,-28.5\"/>\n",
+        "<polygon fill=\"none\" stroke=\"green\" points=\"30,-30.8 30,-115.8 170,-115.8 170,-30.8 30,-30.8\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-54.5\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-56.8\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-53.1\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-54.5C2.79388,-54.5 17.1543,-54.5 30.6317,-54.5\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-54.5 30.9419,-57.6501 34.4419,-54.5 30.9419,-54.5001 30.9419,-54.5001 30.9419,-54.5001 34.4419,-54.5 30.9418,-51.3501 37.9419,-54.5 37.9419,-54.5\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-56.8C2.79388,-56.8 17.1543,-56.8 30.6317,-56.8\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-56.8 30.9419,-59.9501 34.4419,-56.8 30.9419,-56.8001 30.9419,-56.8001 30.9419,-56.8001 34.4419,-56.8 30.9418,-53.6501 37.9419,-56.8 37.9419,-56.8\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-71.5373C48.3189,-81.3579 50.4453,-90.5 56,-90.5 60.166,-90.5 62.4036,-85.3576 62.7128,-78.6433\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-71.5373 65.8541,-78.3818 62.5434,-75.0335 62.7076,-78.5296 62.7076,-78.5296 62.7076,-78.5296 62.5434,-75.0335 59.561,-78.6774 62.3792,-71.5373 62.3792,-71.5373\"/>\n",
-        "<text text-anchor=\"start\" x=\"52.5\" y=\"-94.3\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-73.8373C48.3189,-83.6579 50.4453,-92.8 56,-92.8 60.166,-92.8 62.4036,-87.6576 62.7128,-80.9433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-73.8373 65.8541,-80.6818 62.5434,-77.3335 62.7076,-80.8296 62.7076,-80.8296 62.7076,-80.8296 62.5434,-77.3335 59.561,-80.9774 62.3792,-73.8373 62.3792,-73.8373\"/>\n",
+        "<text text-anchor=\"start\" x=\"52.5\" y=\"-96.6\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-54.5\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"144\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-56.8\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"144\" y=\"-53.1\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.4034,-54.5C87.1928,-54.5 104.732,-54.5 118.874,-54.5\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"125.916,-54.5 118.916,-57.6501 122.416,-54.5 118.916,-54.5001 118.916,-54.5001 118.916,-54.5001 122.416,-54.5 118.916,-51.3501 125.916,-54.5 125.916,-54.5\"/>\n",
-        "<text text-anchor=\"start\" x=\"94.5\" y=\"-73.3\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-58.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.4034,-56.8C87.1928,-56.8 104.732,-56.8 118.874,-56.8\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"125.916,-56.8 118.916,-59.9501 122.416,-56.8 118.916,-56.8001 118.916,-56.8001 118.916,-56.8001 122.416,-56.8 118.916,-53.6501 125.916,-56.8 125.916,-56.8\"/>\n",
+        "<text text-anchor=\"start\" x=\"94.5\" y=\"-75.6\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-60.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"56.5,-1 55.5,-1 55.5,-0 56.5,-0 56.5,-1\"/>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-1.8\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M128.436,-45.3549C104.425,-30.2785 58.9748,-1.73997 57.0623,-0.539139\"/>\n",
-        "<text text-anchor=\"start\" x=\"95.5\" y=\"-36.3\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M128.216,-47.3452C109.582,-35.428 78.2908,-15.4162 64.2282,-6.42267\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"65.183,-4.12514 57.9658,-2.41768 62.543,-8.25315 65.183,-4.12514\"/>\n",
+        "<text text-anchor=\"start\" x=\"95.5\" y=\"-38.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M56,-1.34375C56,-10.6098 56,-19.8758 56,-29.1418\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"56,-36.2275 52.8501,-29.2275 56,-32.7275 56.0001,-29.2275 56.0001,-29.2275 56.0001,-29.2275 56,-32.7275 59.1501,-29.2276 56,-36.2275 56,-36.2275\"/>\n",
+        "<g id=\"edge5\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M56,-3.94844C56,-13.1613 56,-22.3742 56,-31.5871\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"56,-38.6323 52.8501,-31.6322 56,-35.1323 56.0001,-31.6323 56.0001,-31.6323 56.0001,-31.6323 56,-35.1323 59.1501,-31.6323 56,-38.6323 56,-38.6323\"/>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M57.0885,-0.5174C58.9055,-0.877388 88.2848,-6.83508 108,-19.5 114.864,-23.9094 121.451,-29.8619 127.021,-35.6065\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"131.831,-40.7735 124.756,-37.7958 129.446,-38.2116 127.061,-35.6496 127.061,-35.6496 127.061,-35.6496 129.446,-38.2116 129.367,-33.5034 131.831,-40.7735 131.831,-40.7735\"/>\n",
+        "<g id=\"edge6\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M58.3605,-2.07433C64.5216,-3.36203 90.2737,-9.23561 108,-20.8 115.043,-25.3947 121.748,-31.6386 127.37,-37.6363\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"132.206,-43.0208 125.185,-39.9183 129.867,-40.4171 127.528,-37.8133 127.528,-37.8133 127.528,-37.8133 129.867,-40.4171 129.872,-35.7083 132.206,-43.0208 132.206,-43.0208\"/>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76dc5d7de0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76203783c0> >"
        ]
       }
      ],
-     "prompt_number": 30
+     "prompt_number": 5
     },
     {
      "cell_type": "code",
@@ -509,7 +487,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 31,
+       "prompt_number": 6,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -517,75 +495,76 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"186pt\" height=\"168pt\"\n",
-        " viewBox=\"0.00 0.00 186.00 167.96\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 163.96)\">\n",
+        "<svg width=\"186pt\" height=\"170pt\"\n",
+        " viewBox=\"0.00 0.00 186.00 169.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 165.8)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-163.96 182,-163.96 182,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"66.5\" y=\"-145.76\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"91.5\" y=\"-145.76\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"107.5\" y=\"-145.76\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-165.8 182,-165.8 182,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"66.5\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"91.5\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"107.5\" y=\"-147.6\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" stroke=\"orange\" points=\"30,-28.9597 30,-128.96 170,-128.96 170,-28.9597 30,-28.9597\"/>\n",
+        "<polygon fill=\"none\" stroke=\"orange\" points=\"30,-30.8 30,-130.8 170,-130.8 170,-30.8 30,-30.8\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-54.9597\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-51.2597\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-56.8\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-53.1\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-54.9597C2.79388,-54.9597 17.1543,-54.9597 30.6317,-54.9597\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-54.9597 30.9419,-58.1098 34.4419,-54.9598 30.9419,-54.9598 30.9419,-54.9598 30.9419,-54.9598 34.4419,-54.9598 30.9418,-51.8098 37.9419,-54.9597 37.9419,-54.9597\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-56.8C2.79388,-56.8 17.1543,-56.8 30.6317,-56.8\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-56.8 30.9419,-59.9501 34.4419,-56.8 30.9419,-56.8001 30.9419,-56.8001 30.9419,-56.8001 34.4419,-56.8 30.9418,-53.6501 37.9419,-56.8 37.9419,-56.8\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-71.997C48.3189,-81.8176 50.4453,-90.9597 56,-90.9597 60.166,-90.9597 62.4036,-85.8173 62.7128,-79.103\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-71.997 65.8541,-78.8416 62.5434,-75.4932 62.7076,-78.9893 62.7076,-78.9893 62.7076,-78.9893 62.5434,-75.4932 59.561,-79.1371 62.3792,-71.997 62.3792,-71.997\"/>\n",
-        "<text text-anchor=\"start\" x=\"52.5\" y=\"-109.76\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
-        "<text text-anchor=\"start\" x=\"48\" y=\"-94.7597\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-73.8373C48.3189,-83.6579 50.4453,-92.8 56,-92.8 60.166,-92.8 62.4036,-87.6576 62.7128,-80.9433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-73.8373 65.8541,-80.6818 62.5434,-77.3335 62.7076,-80.8296 62.7076,-80.8296 62.7076,-80.8296 62.5434,-77.3335 59.561,-80.9774 62.3792,-73.8373 62.3792,-73.8373\"/>\n",
+        "<text text-anchor=\"start\" x=\"52.5\" y=\"-111.6\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"48\" y=\"-96.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-54.9597\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"144\" y=\"-51.2597\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-56.8\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"144\" y=\"-53.1\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.4034,-54.9597C87.1928,-54.9597 104.732,-54.9597 118.874,-54.9597\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"125.916,-54.9597 118.916,-58.1098 122.416,-54.9598 118.916,-54.9598 118.916,-54.9598 118.916,-54.9598 122.416,-54.9598 118.916,-51.8098 125.916,-54.9597 125.916,-54.9597\"/>\n",
-        "<text text-anchor=\"start\" x=\"94.5\" y=\"-58.7597\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.4034,-56.8C87.1928,-56.8 104.732,-56.8 118.874,-56.8\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"125.916,-56.8 118.916,-59.9501 122.416,-56.8 118.916,-56.8001 118.916,-56.8001 118.916,-56.8001 122.416,-56.8 118.916,-53.6501 125.916,-56.8 125.916,-56.8\"/>\n",
+        "<text text-anchor=\"start\" x=\"94.5\" y=\"-60.6\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"56.5,-1.45972 55.5,-1.45972 55.5,-0.459718 56.5,-0.459718 56.5,-1.45972\"/>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-1.8\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M131.723,-41.7008C125.318,-34.8036 116.831,-26.6488 108,-20.9597 88.1721,-8.18576 58.8985,-1.39181 57.0882,-0.979667\"/>\n",
-        "<text text-anchor=\"start\" x=\"95.5\" y=\"-39.7597\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-24.7597\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M131.685,-43.6003C125.268,-36.7206 116.782,-28.5634 108,-22.8 94.1305,-13.6981 75.6755,-7.29775 65.1938,-4.11103\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"65.7549,-1.72327 58.3508,-2.15071 64.4054,-6.4338 65.7549,-1.72327\"/>\n",
+        "<text text-anchor=\"start\" x=\"95.5\" y=\"-41.6\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-26.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M56,-1.80347C56,-11.0695 56,-20.3355 56,-29.6015\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"56,-36.6873 52.8501,-29.6872 56,-33.1873 56.0001,-29.6873 56.0001,-29.6873 56.0001,-29.6873 56,-33.1873 59.1501,-29.6873 56,-36.6873 56,-36.6873\"/>\n",
+        "<g id=\"edge5\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M56,-3.94844C56,-13.1613 56,-22.3742 56,-31.5871\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"56,-38.6323 52.8501,-31.6322 56,-35.1323 56.0001,-31.6323 56.0001,-31.6323 56.0001,-31.6323 56,-35.1323 59.1501,-31.6323 56,-38.6323 56,-38.6323\"/>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M57.0904,-0.9493C58.9447,-0.740081 88.9129,2.42946 108,-8.95972 117.662,-14.7252 125.575,-24.2646 131.417,-33.166\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"135.127,-39.1724 128.768,-34.872 133.287,-36.1946 131.448,-33.2168 131.448,-33.2168 131.448,-33.2168 133.287,-36.1946 134.128,-31.5615 135.127,-39.1724 135.127,-39.1724\"/>\n",
+        "<g id=\"edge6\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M58.3854,-1.69527C64.6542,-1.28831 90.8043,-0.315741 108,-10.8 117.607,-16.6573 125.513,-26.2081 131.364,-35.0934\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"135.083,-41.0848 128.715,-36.7985 133.237,-38.111 131.391,-35.1373 131.391,-35.1373 131.391,-35.1373 133.237,-38.111 134.068,-33.4761 135.083,-41.0848 135.083,-41.0848\"/>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f76dc5d7f00> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7620378360> >"
        ]
       }
      ],
-     "prompt_number": 31
+     "prompt_number": 6
     },
     {
      "cell_type": "code",
diff --git a/tests/python/alternating.py b/tests/python/alternating.py
index a2ed3c7e5..d1bb47f9a 100755
--- a/tests/python/alternating.py
+++ b/tests/python/alternating.py
@@ -73,6 +73,11 @@ State: 2
 aut2 = spot.automaton(h)
 h2 = aut2.to_str('hoa')
 print(h2)
+assert h != h2
+
+# This will sort destination groups
+aut.merge_univ_dests()
+h = aut.to_str('hoa')
 assert h == h2
 
 aut2.set_univ_init_state([0, 1])
@@ -90,7 +95,7 @@ State: 0
 [0] 1&2 {0}
 [1] 0&1
 State: 1
-[0&1] 0&2&1
+[0&1] 0&1&2
 State: 2
 [0 | 1] 2
 --END--"""
@@ -121,7 +126,7 @@ State: 0
 [0] 1&2 {0}
 [1] 0&1
 State: 1
-[0&1] 0&2&1
+[0&1] 0&1&2
 State: 2
 [0 | 1] 2
 State: 3
diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb
index ca231e52c..b9aea5adc 100644
--- a/tests/python/alternation.ipynb
+++ b/tests/python/alternation.ipynb
@@ -84,130 +84,132 @@
        "output_type": "pyout",
        "prompt_number": 2,
        "svg": [
-        "<svg height=\"213pt\" viewBox=\"0.00 0.00 475.48 212.74\" width=\"475pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 208.74)\">\n",
+        "<svg height=\"205pt\" viewBox=\"0.00 0.00 478.08 204.87\" width=\"478pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 200.87)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-208.74 471.48,-208.74 471.48,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"211.24\" y=\"-190.54\">Fin(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.24\" y=\"-190.54\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"252.24\" y=\"-190.54\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-200.87 474.08,-200.87 474.08,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.54\" y=\"-182.67\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"237.54\" y=\"-182.67\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.54\" y=\"-182.67\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"56\" cy=\"-81.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-78.1701\">0</text>\n",
+        "<ellipse cx=\"56\" cy=\"-82.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-79.1701\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.15491,-81.8701C2.79388,-81.8701 17.1543,-81.8701 30.6317,-81.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-81.8701 30.9419,-85.0202 34.4419,-81.8701 30.9419,-81.8702 30.9419,-81.8702 30.9419,-81.8702 34.4419,-81.8701 30.9418,-78.7202 37.9419,-81.8701 37.9419,-81.8701\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-82.8701C2.79388,-82.8701 17.1543,-82.8701 30.6317,-82.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-82.8701 30.9419,-86.0202 34.4419,-82.8701 30.9419,-82.8702 30.9419,-82.8702 30.9419,-82.8702 34.4419,-82.8701 30.9418,-79.7202 37.9419,-82.8701 37.9419,-82.8701\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>-1</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"120,-82.3701 119,-82.3701 119,-81.3701 120,-81.3701 120,-82.3701\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"120.8\" cy=\"-82.8701\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;&#45;1 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;-1</title>\n",
-        "<path d=\"M74.2705,-81.8701C92.0425,-81.8701 117.359,-81.8701 118.924,-81.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-85.6701\">1</text>\n",
-        "</g>\n",
-        "<!-- 3 -->\n",
-        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
-        "<ellipse cx=\"183.87\" cy=\"-121.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179.37\" y=\"-125.67\">3</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.87\" y=\"-110.67\">\u24ff</text>\n",
-        "</g>\n",
-        "<!-- &#45;1&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge3\"><title>-1-&gt;3</title>\n",
-        "<path d=\"M120.046,-81.899C121.052,-82.5396 138.562,-93.6801 154.84,-104.037\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"160.749,-107.796 153.152,-106.696 157.796,-105.917 154.843,-104.038 154.843,-104.038 154.843,-104.038 157.796,-105.917 156.534,-101.38 160.749,-107.796 160.749,-107.796\" stroke=\"black\"/>\n",
+        "<path d=\"M74.1604,-82.8701C86.2355,-82.8701 101.875,-82.8701 111.357,-82.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"111.602,-85.3202 118.602,-82.8701 111.602,-80.4202 111.602,-85.3202\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-86.6701\">1</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
-        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
-        "<ellipse cx=\"183.87\" cy=\"-25.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179.37\" y=\"-22.1701\">1</text>\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"186.47\" cy=\"-122.87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.97\" y=\"-119.17\">1</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge4\"><title>-1-&gt;1</title>\n",
-        "<path d=\"M120.046,-81.8295C121.259,-80.7489 146.435,-58.3241 164.542,-42.1952\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"169.901,-37.4224 166.769,-44.4305 167.287,-39.7503 164.673,-42.0783 164.673,-42.0783 164.673,-42.0783 167.287,-39.7503 162.578,-39.7261 169.901,-37.4224 169.901,-37.4224\" stroke=\"black\"/>\n",
+        "<g class=\"edge\" id=\"edge3\"><title>-1-&gt;1</title>\n",
+        "<path d=\"M122.905,-83.5643C127.862,-86.6782 148.509,-99.6497 164.747,-109.851\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"170.933,-113.737 163.33,-112.681 167.969,-111.875 165.005,-110.013 165.005,-110.013 165.005,-110.013 167.969,-111.875 166.681,-107.346 170.933,-113.737 170.933,-113.737\" stroke=\"black\"/>\n",
         "</g>\n",
-        "<!-- 3&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
-        "<path d=\"M175.67,-147.691C175.207,-158.048 177.94,-166.74 183.87,-166.74 188.317,-166.74 190.967,-161.851 191.818,-155.037\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"192.07,-147.691 194.978,-154.795 191.95,-151.189 191.83,-154.687 191.83,-154.687 191.83,-154.687 191.95,-151.189 188.682,-154.579 192.07,-147.691 192.07,-147.691\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179.37\" y=\"-170.54\">1</text>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"186.47\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.97\" y=\"-30.6701\">3</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"178.47\" y=\"-15.6701\">\u24ff</text>\n",
         "</g>\n",
-        "<!-- 4 -->\n",
-        "<g class=\"node\" id=\"node9\"><title>4</title>\n",
-        "<ellipse cx=\"277.74\" cy=\"-121.87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"277.74\" y=\"-118.17\">4</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;4</title>\n",
-        "<path d=\"M210.951,-121.87C223.988,-121.87 239.668,-121.87 252.449,-121.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"259.598,-121.87 252.598,-125.02 256.098,-121.87 252.598,-121.87 252.598,-121.87 252.598,-121.87 256.098,-121.87 252.598,-118.72 259.598,-121.87 259.598,-121.87\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.74\" y=\"-125.67\">a</text>\n",
+        "<!-- &#45;1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>-1-&gt;3</title>\n",
+        "<path d=\"M122.515,-82.2412C126.32,-78.8944 144.614,-62.8039 160.509,-48.8246\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"165.782,-44.1862 162.606,-51.1745 163.154,-46.4977 160.526,-48.8092 160.526,-48.8092 160.526,-48.8092 163.154,-46.4977 158.446,-46.4439 165.782,-44.1862 165.782,-44.1862\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
-        "<path d=\"M176.202,-42.1603C174.353,-52.2592 176.909,-61.8701 183.87,-61.8701 189.091,-61.8701 191.834,-56.464 192.099,-49.5004\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"191.538,-42.1603 195.212,-48.9 191.805,-45.6502 192.071,-49.14 192.071,-49.14 192.071,-49.14 191.805,-45.6502 188.93,-49.38 191.538,-42.1603 191.538,-42.1603\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179.37\" y=\"-65.6701\">b</text>\n",
+        "<path d=\"M178.802,-139.16C176.953,-149.259 179.509,-158.87 186.47,-158.87 191.691,-158.87 194.434,-153.464 194.699,-146.5\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"194.138,-139.16 197.812,-145.9 194.405,-142.65 194.671,-146.14 194.671,-146.14 194.671,-146.14 194.405,-142.65 191.53,-146.38 194.138,-139.16 194.138,-139.16\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.97\" y=\"-162.67\">b</text>\n",
         "</g>\n",
         "<!-- &#45;4 -->\n",
         "<g class=\"node\" id=\"node6\"><title>-4</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"278.24,-27.3701 277.24,-27.3701 277.24,-26.3701 278.24,-26.3701 278.24,-27.3701\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"280.34\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;4 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;-4</title>\n",
-        "<path d=\"M202.15,-26.0582C227.931,-26.3388 273.762,-26.8376 276.602,-26.8686\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228.74\" y=\"-30.6701\">!b</text>\n",
+        "<path d=\"M204.75,-120.801C224.684,-118.414 256.603,-114.592 271.37,-112.824\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"271.836,-115.236 278.495,-111.971 271.253,-110.371 271.836,-115.236\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.34\" y=\"-120.67\">!b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
+        "<path d=\"M178.27,-52.6914C177.807,-63.0476 180.54,-71.7401 186.47,-71.7401 190.917,-71.7401 193.567,-66.8506 194.418,-60.0368\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"194.67,-52.6914 197.578,-59.7953 194.55,-56.1893 194.43,-59.6873 194.43,-59.6873 194.43,-59.6873 194.55,-56.1893 191.282,-59.5793 194.67,-52.6914 194.67,-52.6914\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.97\" y=\"-75.5401\">1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>4</title>\n",
+        "<ellipse cx=\"280.34\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"280.34\" y=\"-23.1701\">4</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;4</title>\n",
+        "<path d=\"M213.551,-26.8701C226.588,-26.8701 242.268,-26.8701 255.049,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"262.198,-26.8701 255.198,-30.0202 258.698,-26.8701 255.198,-26.8702 255.198,-26.8702 255.198,-26.8702 258.698,-26.8701 255.198,-23.7202 262.198,-26.8701 262.198,-26.8701\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.34\" y=\"-30.6701\">a</text>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>-4-&gt;1</title>\n",
-        "<path d=\"M276.684,-26.8633C275.531,-26.7259 256.851,-24.5165 241.74,-23.8701 231.018,-23.4114 219.155,-23.7021 209.05,-24.1888\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"202.044,-24.57 208.863,-21.0443 205.539,-24.3798 209.034,-24.1896 209.034,-24.1896 209.034,-24.1896 205.539,-24.3798 209.205,-27.335 202.044,-24.57 202.044,-24.57\" stroke=\"black\"/>\n",
+        "<g class=\"edge\" id=\"edge7\"><title>-4-&gt;1</title>\n",
+        "<path d=\"M278.146,-111.763C272.722,-111.298 249.866,-109.583 231.34,-111.87 224.587,-112.704 217.379,-114.233 210.798,-115.892\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"203.954,-117.717 209.907,-112.87 207.336,-116.815 210.718,-115.914 210.718,-115.914 210.718,-115.914 207.336,-116.815 211.529,-118.957 203.954,-117.717 203.954,-117.717\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node7\"><title>2</title>\n",
-        "<ellipse cx=\"359.61\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"355.11\" y=\"-30.6701\">2</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351.61\" y=\"-15.6701\">\u24ff</text>\n",
+        "<ellipse cx=\"362.21\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"357.71\" y=\"-115.67\">2</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"354.21\" y=\"-100.67\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>-4-&gt;2</title>\n",
-        "<path d=\"M278.798,-26.8701C280.131,-26.8701 304.225,-26.8701 325.594,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"332.699,-26.8701 325.699,-30.0202 329.199,-26.8701 325.699,-26.8702 325.699,-26.8702 325.699,-26.8702 329.199,-26.8701 325.699,-23.7202 332.699,-26.8701 332.699,-26.8701\" stroke=\"black\"/>\n",
+        "<g class=\"edge\" id=\"edge8\"><title>-4-&gt;2</title>\n",
+        "<path d=\"M282.237,-111.87C286.877,-111.87 308.694,-111.87 328.223,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"335.279,-111.87 328.279,-115.02 331.779,-111.87 328.279,-111.87 328.279,-111.87 328.279,-111.87 331.779,-111.87 328.279,-108.72 335.279,-111.87 335.279,-111.87\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
-        "<path d=\"M351.411,-52.6914C350.947,-63.0476 353.68,-71.7401 359.61,-71.7401 364.057,-71.7401 366.707,-66.8506 367.558,-60.0368\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"367.81,-52.6914 370.718,-59.7953 367.69,-56.1893 367.57,-59.6873 367.57,-59.6873 367.57,-59.6873 367.69,-56.1893 364.422,-59.5793 367.81,-52.6914 367.81,-52.6914\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"353.11\" y=\"-75.5401\">!b</text>\n",
+        "<path d=\"M354.011,-137.691C353.547,-148.048 356.28,-156.74 362.21,-156.74 366.657,-156.74 369.307,-151.851 370.158,-145.037\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"370.41,-137.691 373.318,-144.795 370.29,-141.189 370.17,-144.687 370.17,-144.687 370.17,-144.687 370.29,-141.189 367.022,-144.579 370.41,-137.691 370.41,-137.691\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"355.71\" y=\"-160.54\">!b</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g class=\"node\" id=\"node8\"><title>5</title>\n",
-        "<ellipse cx=\"449.48\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"449.48\" y=\"-23.1701\">5</text>\n",
+        "<ellipse cx=\"452.08\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"452.08\" y=\"-108.17\">5</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>2-&gt;5</title>\n",
-        "<path d=\"M386.499,-26.8701C398.376,-26.8701 412.382,-26.8701 424.073,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"431.375,-26.8701 424.375,-30.0202 427.875,-26.8701 424.375,-26.8702 424.375,-26.8702 424.375,-26.8702 427.875,-26.8701 424.375,-23.7202 431.375,-26.8701 431.375,-26.8701\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.48\" y=\"-30.6701\">b</text>\n",
+        "<path d=\"M389.099,-111.87C400.976,-111.87 414.982,-111.87 426.673,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"433.975,-111.87 426.975,-115.02 430.475,-111.87 426.975,-111.87 426.975,-111.87 426.975,-111.87 430.475,-111.87 426.975,-108.72 433.975,-111.87 433.975,-111.87\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"407.08\" y=\"-115.67\">b</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>5-&gt;5</title>\n",
-        "<path d=\"M442.449,-43.5341C440.886,-53.4951 443.23,-62.8701 449.48,-62.8701 454.168,-62.8701 456.658,-57.5966 456.951,-50.7576\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"456.511,-43.5341 460.081,-50.3299 456.724,-47.0277 456.937,-50.5212 456.937,-50.5212 456.937,-50.5212 456.724,-47.0277 453.792,-50.7125 456.511,-43.5341 456.511,-43.5341\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"444.98\" y=\"-66.6701\">1</text>\n",
+        "<path d=\"M445.049,-128.534C443.486,-138.495 445.83,-147.87 452.08,-147.87 456.768,-147.87 459.258,-142.597 459.551,-135.758\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"459.111,-128.534 462.681,-135.33 459.324,-132.028 459.537,-135.521 459.537,-135.521 459.537,-135.521 459.324,-132.028 456.392,-135.713 459.111,-128.534 459.111,-128.534\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"447.58\" y=\"-151.67\">1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
-        "<path d=\"M271.361,-138.907C270.059,-148.728 272.185,-157.87 277.74,-157.87 281.906,-157.87 284.144,-152.728 284.453,-146.013\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"284.119,-138.907 287.594,-145.752 284.284,-142.404 284.448,-145.9 284.448,-145.9 284.448,-145.9 284.284,-142.404 281.301,-146.047 284.119,-138.907 284.119,-138.907\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"274.24\" y=\"-161.67\">a</text>\n",
+        "<path d=\"M273.961,-43.9074C272.659,-53.728 274.785,-62.8701 280.34,-62.8701 284.506,-62.8701 286.744,-57.7276 287.053,-51.0134\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"286.719,-43.9074 290.194,-50.7519 286.884,-47.4035 287.048,-50.8997 287.048,-50.8997 287.048,-50.8997 286.884,-47.4035 283.901,-51.0474 286.719,-43.9074 286.719,-43.9074\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"276.84\" y=\"-66.6701\">a</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
@@ -278,7 +280,7 @@
         "<path fill=\"none\" stroke=\"black\" d=\"M177.786,-60.1238C175.905,-69.9444 178.977,-79.0864 187,-79.0864 193.018,-79.0864 196.25,-73.944 196.696,-67.2297\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"196.214,-60.1238 199.831,-66.8946 196.451,-63.6157 196.688,-67.1077 196.688,-67.1077 196.688,-67.1077 196.451,-63.6157 193.545,-67.3209 196.214,-60.1238 196.214,-60.1238\"/>\n",
         "<text text-anchor=\"start\" x=\"182.5\" y=\"-97.8864\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "<text text-anchor=\"start\" x=\"179\" y=\"-82.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "<text text-anchor=\"start\" x=\"179\" y=\"-82.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g id=\"node4\" class=\"node\"><title>2</title>\n",
@@ -303,7 +305,7 @@
         "<path fill=\"none\" stroke=\"black\" d=\"M212.976,-48.1914C223.813,-49.6298 236.606,-50.2786 248,-48.0864 253.898,-46.9517 259.994,-45.0925 265.774,-42.9703\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"272.382,-40.3859 267.01,-45.8692 269.122,-41.6607 265.863,-42.9356 265.863,-42.9356 265.863,-42.9356 269.122,-41.6607 264.715,-40.002 272.382,-40.3859 272.382,-40.3859\"/>\n",
         "<text text-anchor=\"start\" x=\"233.5\" y=\"-67.8864\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
-        "<text text-anchor=\"start\" x=\"232\" y=\"-52.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "<text text-anchor=\"start\" x=\"232\" y=\"-52.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g id=\"node6\" class=\"node\"><title>4</title>\n",
@@ -339,7 +341,7 @@
         "<path fill=\"none\" stroke=\"black\" d=\"M272.429,-17.7941C260.3,-13.3342 245.247,-10.1137 232,-14.0864 224.351,-16.3803 216.804,-20.481 210.177,-24.8899\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"204.374,-28.9825 208.279,-22.3739 207.234,-26.9653 210.094,-24.9481 210.094,-24.9481 210.094,-24.9481 207.234,-26.9653 211.91,-27.5224 204.374,-28.9825 204.374,-28.9825\"/>\n",
         "<text text-anchor=\"start\" x=\"235.5\" y=\"-32.8864\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "<text text-anchor=\"start\" x=\"232\" y=\"-17.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "<text text-anchor=\"start\" x=\"232\" y=\"-17.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
@@ -360,7 +362,7 @@
         "<path fill=\"none\" stroke=\"black\" d=\"M327.016,-30.9063C374.646,-33.8476 468.425,-39.6387 520.185,-42.8351\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"527.2,-43.2683 520.019,-45.9808 523.707,-43.0525 520.214,-42.8368 520.214,-42.8368 520.214,-42.8368 523.707,-43.0525 520.408,-39.6928 527.2,-43.2683 527.2,-43.2683\"/>\n",
         "<text text-anchor=\"start\" x=\"408.595\" y=\"-57.8864\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
-        "<text text-anchor=\"start\" x=\"419.095\" y=\"-42.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"419.095\" y=\"-42.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;2 -->\n",
         "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;2</title>\n",
@@ -375,13 +377,13 @@
         "<path fill=\"none\" stroke=\"black\" d=\"M546.04,-61.7505C543.462,-71.7114 547.329,-81.0864 557.642,-81.0864 565.376,-81.0864 569.485,-75.813 569.969,-68.974\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"569.243,-61.7505 573.077,-68.4009 569.593,-65.233 569.943,-68.7155 569.943,-68.7155 569.943,-68.7155 569.593,-65.233 566.808,-69.0302 569.243,-61.7505 569.243,-61.7505\"/>\n",
         "<text text-anchor=\"start\" x=\"539.142\" y=\"-99.8864\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
-        "<text text-anchor=\"start\" x=\"549.642\" y=\"-84.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"549.642\" y=\"-84.8864\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd1684339f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989a50> >"
        ]
       }
      ],
@@ -531,7 +533,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd16b5891e0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989b40> >"
        ]
       }
      ],
@@ -571,36 +573,36 @@
        "output_type": "pyout",
        "prompt_number": 5,
        "svg": [
-        "<svg height=\"166pt\" viewBox=\"0.00 0.00 385.48 166.25\" width=\"385pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 162.252)\">\n",
+        "<svg height=\"167pt\" viewBox=\"0.00 0.00 385.48 167.23\" width=\"385pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 163.23)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-162.252 381.48,-162.252 381.48,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"166.24\" y=\"-144.052\">Fin(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.24\" y=\"-144.052\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"207.24\" y=\"-144.052\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-163.23 381.48,-163.23 381.48,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"166.24\" y=\"-145.03\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.24\" y=\"-145.03\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"207.24\" y=\"-145.03\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"64.8701\" cy=\"-67\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-70.8\">0</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-55.8\">\u24ff</text>\n",
+        "<ellipse cx=\"64.8701\" cy=\"-68\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-71.8\">0</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-56.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.04557,-67C1.94668,-67 16.0699,-67 30.6965,-67\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.8616,-67 30.8617,-70.1501 34.3616,-67 30.8616,-67.0001 30.8616,-67.0001 30.8616,-67.0001 34.3616,-67 30.8616,-63.8501 37.8616,-67 37.8616,-67\" stroke=\"black\"/>\n",
+        "<path d=\"M1.04557,-68C1.94668,-68 16.0699,-68 30.6965,-68\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.8616,-68 30.8617,-71.1501 34.3616,-68 30.8616,-68.0001 30.8616,-68.0001 30.8616,-68.0001 34.3616,-68 30.8616,-64.8501 37.8616,-68 37.8616,-68\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"218.61\" cy=\"-62\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.11\" y=\"-65.8\">1</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.61\" y=\"-50.8\">\u24ff</text>\n",
+        "<ellipse cx=\"218.61\" cy=\"-63\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.11\" y=\"-66.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.61\" y=\"-51.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M89.4817,-55.3538C95.8999,-52.7356 102.955,-50.3378 109.74,-49 137.647,-43.4974 145.59,-44.9169 173.74,-49 177.769,-49.5844 181.943,-50.4558 186.043,-51.4759\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"192.833,-53.3086 185.254,-54.5257 189.454,-52.3966 186.075,-51.4845 186.075,-51.4845 186.075,-51.4845 189.454,-52.3966 186.896,-48.4433 192.833,-53.3086 192.833,-53.3086\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.24\" y=\"-52.8\">a</text>\n",
+        "<path d=\"M89.4817,-56.3538C95.8999,-53.7356 102.955,-51.3378 109.74,-50 137.647,-44.4974 145.59,-45.9169 173.74,-50 177.769,-50.5844 181.943,-51.4558 186.043,-52.4759\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"192.833,-54.3086 185.254,-55.5257 189.454,-53.3966 186.075,-52.4845 186.075,-52.4845 186.075,-52.4845 189.454,-53.3966 186.896,-49.4433 192.833,-54.3086 192.833,-54.3086\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.24\" y=\"-53.8\">a</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node4\"><title>2</title>\n",
@@ -609,36 +611,37 @@
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M88.0042,-53.2326C112.349,-39.0498 153.154,-18.0502 191.74,-11 241.874,-1.83985 301.833,-8.57241 334.447,-13.6824\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"341.745,-14.8711 334.329,-16.8547 338.29,-14.3084 334.836,-13.7456 334.836,-13.7456 334.836,-13.7456 338.29,-14.3084 335.342,-10.6366 341.745,-14.8711 341.745,-14.8711\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213.11\" y=\"-14.8\">!a</text>\n",
+        "<path d=\"M88.0042,-54.2326C112.349,-40.0498 153.154,-19.0502 191.74,-12 241.809,-2.85175 301.698,-9.08831 334.339,-13.9001\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"341.262,-14.9601 333.866,-17.0142 337.802,-14.4303 334.342,-13.9005 334.342,-13.9005 334.342,-13.9005 337.802,-14.4303 334.819,-10.7868 341.262,-14.9601 341.262,-14.9601\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213.11\" y=\"-15.8\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>1-&gt;0</title>\n",
-        "<path d=\"M191.632,-63.2607C185.75,-63.5249 179.531,-63.7875 173.74,-64 148.786,-64.9157 120.576,-65.6911 99.2648,-66.2241\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"92.031,-66.4023 98.9513,-63.0808 95.53,-66.3161 99.0289,-66.2298 99.0289,-66.2298 99.0289,-66.2298 95.53,-66.3161 99.1065,-69.3789 92.031,-66.4023 92.031,-66.4023\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.74\" y=\"-69.8\">!a &amp; b &amp; p</text>\n",
+        "<path d=\"M191.632,-64.2607C185.75,-64.5249 179.531,-64.7875 173.74,-65 148.786,-65.9157 120.576,-66.6911 99.2648,-67.2241\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"92.031,-67.4023 98.9513,-64.0808 95.53,-67.3161 99.0289,-67.2298 99.0289,-67.2298 99.0289,-67.2298 95.53,-67.3161 99.1065,-70.3789 92.031,-67.4023 92.031,-67.4023\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.74\" y=\"-70.8\">!a &amp; b &amp; p</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;1</title>\n",
-        "<path d=\"M205.074,-85.5464C203.403,-96.8722 207.915,-106.87 218.61,-106.87 226.966,-106.87 231.548,-100.768 232.355,-92.6976\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"232.146,-85.5464 235.5,-92.4513 232.249,-89.0449 232.351,-92.5434 232.351,-92.5434 232.351,-92.5434 232.249,-89.0449 229.202,-92.6355 232.146,-85.5464 232.146,-85.5464\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"199.11\" y=\"-110.67\">!b &amp; p</text>\n",
+        "<path d=\"M205.074,-86.5464C203.403,-97.8722 207.915,-107.87 218.61,-107.87 226.966,-107.87 231.548,-101.768 232.355,-93.6976\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"232.146,-86.5464 235.5,-93.4513 232.249,-90.0449 232.351,-93.5434 232.351,-93.5434 232.351,-93.5434 232.249,-90.0449 229.202,-93.6355 232.146,-86.5464 232.146,-86.5464\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"199.11\" y=\"-111.67\">!b &amp; p</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>1-&gt;2</title>\n",
-        "<path d=\"M243.487,-50.881C249.903,-48.1082 256.891,-45.2791 263.48,-43 287.348,-34.7443 315.39,-27.6746 334.791,-23.1811\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"341.777,-21.588 335.653,-26.2156 338.365,-22.3662 334.952,-23.1445 334.952,-23.1445 334.952,-23.1445 338.365,-22.3662 334.252,-20.0733 341.777,-21.588 341.777,-21.588\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272.98\" y=\"-46.8\">!a &amp; !b</text>\n",
+        "<path d=\"M243.502,-51.9247C249.918,-49.1516 256.903,-46.3114 263.48,-44 287.37,-35.6052 315.408,-28.2227 334.803,-23.4902\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"341.786,-21.8097 335.718,-26.5102 338.383,-22.6286 334.981,-23.4476 334.981,-23.4476 334.981,-23.4476 338.383,-22.6286 334.243,-20.385 341.786,-21.8097 341.786,-21.8097\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272.98\" y=\"-47.8\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g class=\"node\" id=\"node5\"><title>-1</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"359.98,-103.5 358.98,-103.5 358.98,-102.5 359.98,-102.5 359.98,-103.5\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"359.48\" cy=\"-104\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;-1</title>\n",
-        "<path d=\"M245.842,-60.9712C267.498,-61.0578 298.604,-63.3807 323.48,-74 341.479,-81.6835 357.452,-101.696 358.433,-102.939\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"263.48\" y=\"-77.8\">a &amp; b &amp; p</text>\n",
+        "<path d=\"M245.842,-61.9712C267.498,-62.0578 298.604,-64.3807 323.48,-75 335.419,-80.0965 346.466,-90.6175 352.838,-97.4873\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"351.282,-99.4292 357.738,-103.079 354.968,-96.1998 351.282,-99.4292\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"263.48\" y=\"-78.8\">a &amp; b &amp; p</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
@@ -648,13 +651,13 @@
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>-1-&gt;0</title>\n",
-        "<path d=\"M358.412,-103.033C355.558,-104.407 263.674,-148.238 191.74,-131 155.477,-122.31 117.869,-101.352 93.3175,-85.7725\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"87.3656,-81.9382 94.9562,-83.0811 90.3079,-83.8337 93.2502,-85.7292 93.2502,-85.7292 93.2502,-85.7292 90.3079,-83.8337 91.5443,-88.3773 87.3656,-81.9382 87.3656,-81.9382\" stroke=\"black\"/>\n",
+        "<path d=\"M357.41,-104.507C346.853,-109.443 260.248,-148.417 191.74,-132 155.477,-123.31 117.869,-102.352 93.3175,-86.7725\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"87.3656,-82.9382 94.9562,-84.0811 90.3079,-84.8337 93.2502,-86.7292 93.2502,-86.7292 93.2502,-86.7292 90.3079,-84.8337 91.5443,-89.3773 87.3656,-82.9382 87.3656,-82.9382\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>-1-&gt;1</title>\n",
-        "<path d=\"M358.322,-103.001C355.064,-103.022 302.332,-103.139 263.48,-89 257.923,-86.9777 252.31,-84.1987 247.04,-81.1889\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"241.036,-77.581 248.658,-78.4863 244.036,-79.3837 247.036,-81.1864 247.036,-81.1864 247.036,-81.1864 244.036,-79.3837 245.413,-83.8864 241.036,-77.581 241.036,-77.581\" stroke=\"black\"/>\n",
+        "<path d=\"M357.508,-104.003C349.993,-104 300.452,-103.454 263.48,-90 257.923,-87.9777 252.31,-85.1987 247.04,-82.1889\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"241.036,-78.581 248.658,-79.4863 244.036,-80.3837 247.036,-82.1864 247.036,-82.1864 247.036,-82.1864 244.036,-80.3837 245.413,-84.8864 241.036,-78.581 241.036,-78.581\" stroke=\"black\"/>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
@@ -794,7 +797,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd16843a2d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989a80> >"
        ]
       }
      ],
@@ -837,32 +840,33 @@
        "output_type": "pyout",
        "prompt_number": 7,
        "svg": [
-        "<svg height=\"180pt\" viewBox=\"0.00 0.00 510.48 180.25\" width=\"510pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 176.252)\">\n",
+        "<svg height=\"180pt\" viewBox=\"0.00 0.00 510.48 180.23\" width=\"510pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 176.23)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-176.252 506.48,-176.252 506.48,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228.74\" y=\"-158.052\">Fin(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.74\" y=\"-158.052\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269.74\" y=\"-158.052\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-176.23 506.48,-176.23 506.48,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228.74\" y=\"-158.03\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.74\" y=\"-158.03\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269.74\" y=\"-158.03\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node2\"><title>3</title>\n",
-        "<ellipse cx=\"56\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-30.3\">3</text>\n",
+        "<ellipse cx=\"56\" cy=\"-35\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-31.3\">3</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;3</title>\n",
-        "<path d=\"M1.15491,-34C2.79388,-34 17.1543,-34 30.6317,-34\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-34 30.9419,-37.1501 34.4419,-34 30.9419,-34.0001 30.9419,-34.0001 30.9419,-34.0001 34.4419,-34 30.9418,-30.8501 37.9419,-34 37.9419,-34\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-35C2.79388,-35 17.1543,-35 30.6317,-35\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-35 30.9419,-38.1501 34.4419,-35 30.9419,-35.0001 30.9419,-35.0001 30.9419,-35.0001 34.4419,-35 30.9418,-31.8501 37.9419,-35 37.9419,-35\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;4 -->\n",
         "<g class=\"node\" id=\"node7\"><title>-4</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"122,-52.5 121,-52.5 121,-51.5 122,-51.5 122,-52.5\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"121.5\" cy=\"-53\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;&#45;4 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>3-&gt;-4</title>\n",
-        "<path d=\"M73.6839,-38.7293C91.9099,-43.8957 118.759,-51.5064 120.419,-51.9771\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-49.8\">a</text>\n",
+        "<path d=\"M73.6839,-39.7293C86.1591,-43.2656 102.674,-47.9471 112.387,-50.7001\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"111.857,-53.0965 119.26,-52.6485 113.194,-48.3823 111.857,-53.0965\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-50.8\">a</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
@@ -884,13 +888,13 @@
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node5\"><title>2</title>\n",
-        "<ellipse cx=\"484.48\" cy=\"-32\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"484.48\" y=\"-28.3\">2</text>\n",
+        "<ellipse cx=\"484.48\" cy=\"-31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"484.48\" y=\"-27.3\">2</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M213.004,-67.2326C237.349,-53.0498 278.154,-32.0502 316.74,-25 366.874,-15.8398 426.833,-22.5724 459.447,-27.6824\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"466.745,-28.8711 459.329,-30.8547 463.29,-28.3084 459.836,-27.7456 459.836,-27.7456 459.836,-27.7456 463.29,-28.3084 460.342,-24.6366 466.745,-28.8711 466.745,-28.8711\" stroke=\"black\"/>\n",
+        "<path d=\"M213.004,-67.2326C237.349,-53.0498 278.154,-32.0502 316.74,-25 366.809,-15.8517 426.698,-22.0883 459.339,-26.9001\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"466.262,-27.9601 458.866,-30.0142 462.802,-27.4303 459.342,-26.9005 459.342,-26.9005 459.342,-26.9005 462.802,-27.4303 459.819,-23.7868 466.262,-27.9601 466.262,-27.9601\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338.11\" y=\"-28.8\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
@@ -907,39 +911,40 @@
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>1-&gt;2</title>\n",
-        "<path d=\"M368.487,-64.881C374.903,-62.1082 381.891,-59.2791 388.48,-57 412.348,-48.7443 440.39,-41.6746 459.791,-37.1811\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"466.777,-35.588 460.653,-40.2156 463.365,-36.3662 459.952,-37.1445 459.952,-37.1445 459.952,-37.1445 463.365,-36.3662 459.252,-34.0733 466.777,-35.588 466.777,-35.588\" stroke=\"black\"/>\n",
+        "<path d=\"M368.502,-64.9247C374.918,-62.1516 381.903,-59.3114 388.48,-57 412.37,-48.6052 440.408,-41.2227 459.803,-36.4902\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"466.786,-34.8097 460.718,-39.5102 463.383,-35.6286 459.981,-36.4476 459.981,-36.4476 459.981,-36.4476 463.383,-35.6286 459.243,-33.385 466.786,-34.8097 466.786,-34.8097\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"397.98\" y=\"-60.8\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g class=\"node\" id=\"node6\"><title>-1</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"484.98,-117.5 483.98,-117.5 483.98,-116.5 484.98,-116.5 484.98,-117.5\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"484.48\" cy=\"-117\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;-1</title>\n",
-        "<path d=\"M370.842,-74.9712C392.498,-75.0578 423.604,-77.3807 448.48,-88 466.479,-95.6835 482.452,-115.696 483.433,-116.939\" fill=\"none\" stroke=\"black\"/>\n",
+        "<path d=\"M370.842,-74.9712C392.498,-75.0578 423.604,-77.3807 448.48,-88 460.419,-93.0965 471.466,-103.617 477.838,-110.487\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"476.282,-112.429 482.738,-116.079 479.968,-109.2 476.282,-112.429\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.48\" y=\"-91.8\">a &amp; b &amp; p</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
-        "<path d=\"M473.568,-46.4167C469.757,-57.166 473.394,-68 484.48,-68 493.141,-68 497.256,-61.3875 496.825,-53.3688\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"495.393,-46.4167 499.89,-52.6375 496.099,-49.8447 496.805,-53.2728 496.805,-53.2728 496.805,-53.2728 496.099,-49.8447 493.72,-53.9082 495.393,-46.4167 495.393,-46.4167\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"484.48\" y=\"-71.8\">1</text>\n",
+        "<path d=\"M473.568,-45.4167C469.757,-56.166 473.394,-67 484.48,-67 493.141,-67 497.256,-60.3875 496.825,-52.3688\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"495.393,-45.4167 499.89,-51.6375 496.099,-48.8447 496.805,-52.2728 496.805,-52.2728 496.805,-52.2728 496.099,-48.8447 493.72,-52.9082 495.393,-45.4167 495.393,-45.4167\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"484.48\" y=\"-70.8\">1</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>-1-&gt;0</title>\n",
-        "<path d=\"M483.412,-117.033C480.558,-118.407 388.674,-162.238 316.74,-145 280.477,-136.31 242.869,-115.352 218.318,-99.7725\" fill=\"none\" stroke=\"black\"/>\n",
+        "<path d=\"M482.41,-117.507C471.853,-122.443 385.248,-161.417 316.74,-145 280.477,-136.31 242.869,-115.352 218.318,-99.7725\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"212.366,-95.9382 219.956,-97.0811 215.308,-97.8337 218.25,-99.7292 218.25,-99.7292 218.25,-99.7292 215.308,-97.8337 216.544,-102.377 212.366,-95.9382 212.366,-95.9382\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>-1-&gt;1</title>\n",
-        "<path d=\"M483.322,-117.001C480.064,-117.022 427.332,-117.139 388.48,-103 382.923,-100.978 377.31,-98.1987 372.04,-95.1889\" fill=\"none\" stroke=\"black\"/>\n",
+        "<path d=\"M482.508,-117.003C474.993,-117 425.452,-116.454 388.48,-103 382.923,-100.978 377.31,-98.1987 372.04,-95.1889\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"366.036,-91.581 373.658,-92.4863 369.036,-93.3837 372.036,-95.1864 372.036,-95.1864 372.036,-95.1864 369.036,-93.3837 370.413,-97.8864 366.036,-91.581 366.036,-91.581\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge13\"><title>-4-&gt;0</title>\n",
-        "<path d=\"M122.548,-52.021C123.588,-52.4753 141.298,-60.2135 158.154,-67.5786\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"164.78,-70.4739 157.104,-70.5576 161.573,-69.0725 158.365,-67.6712 158.365,-67.6712 158.365,-67.6712 161.573,-69.0725 159.627,-64.7847 164.78,-70.4739 164.78,-70.4739\" stroke=\"black\"/>\n",
+        "<g class=\"edge\" id=\"edge12\"><title>-4-&gt;0</title>\n",
+        "<path d=\"M123.652,-53.486C127.921,-55.2871 143.358,-61.7994 158.141,-68.036\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"164.844,-70.8641 157.17,-71.0455 161.62,-69.5037 158.395,-68.1432 158.395,-68.1432 158.395,-68.1432 161.62,-69.5037 159.619,-65.2409 164.844,-70.8641 164.844,-70.8641\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node8\"><title>4</title>\n",
@@ -947,14 +952,14 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"189.87\" y=\"-14.3\">4</text>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>-4-&gt;4</title>\n",
-        "<path d=\"M122.548,-51.9754C123.772,-51.3485 148.089,-38.8914 166.926,-29.2414\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"173.565,-25.8403 168.771,-31.8355 170.45,-27.4361 167.335,-29.0319 167.335,-29.0319 167.335,-29.0319 170.45,-27.4361 165.899,-26.2284 173.565,-25.8403 173.565,-25.8403\" stroke=\"black\"/>\n",
+        "<g class=\"edge\" id=\"edge13\"><title>-4-&gt;4</title>\n",
+        "<path d=\"M123.652,-52.3925C128.819,-49.6679 150.342,-38.3178 167.268,-29.3919\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"173.716,-25.9913 168.994,-32.0429 170.62,-27.624 167.524,-29.2566 167.524,-29.2566 167.524,-29.2566 170.62,-27.624 166.055,-26.4703 173.716,-25.9913 173.716,-25.9913\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>4-&gt;3</title>\n",
-        "<path d=\"M171.965,-20.0511C148.855,-22.855 107.273,-27.9003 80.9587,-31.0931\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"73.9697,-31.941 80.5393,-27.9707 77.4443,-31.5194 80.9188,-31.0978 80.9188,-31.0978 80.9188,-31.0978 77.4443,-31.5194 81.2982,-34.2249 73.9697,-31.941 73.9697,-31.941\" stroke=\"black\"/>\n",
+        "<path d=\"M171.73,-20.1074C157.166,-21.9074 135.707,-24.5816 117,-27 105.23,-28.5217 92.167,-30.2577 81.2432,-31.7228\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.0645,-32.6879 80.5823,-28.6333 77.5333,-32.2216 81.0021,-31.7552 81.0021,-31.7552 81.0021,-31.7552 77.5333,-32.2216 81.4218,-34.8771 74.0645,-32.6879 74.0645,-32.6879\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"121.5\" y=\"-30.8\">1</text>\n",
         "</g>\n",
         "</g>\n",
@@ -1140,7 +1145,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd168433c90> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989c90> >"
        ]
       }
      ],
@@ -1187,162 +1192,165 @@
        "output_type": "pyout",
        "prompt_number": 9,
        "svg": [
-        "<svg height=\"302pt\" viewBox=\"0.00 0.00 520.22 301.87\" width=\"520pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 297.87)\">\n",
+        "<svg height=\"304pt\" viewBox=\"0.00 0.00 522.82 303.87\" width=\"523pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 299.87)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-297.87 516.22,-297.87 516.22,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233.61\" y=\"-279.67\">Fin(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.61\" y=\"-279.67\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"274.61\" y=\"-279.67\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-299.87 518.82,-299.87 518.82,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.91\" y=\"-281.67\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.91\" y=\"-281.67\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275.91\" y=\"-281.67\">)</text>\n",
         "<!-- I -->\n",
         "<!-- &#45;7 -->\n",
         "<g class=\"node\" id=\"node2\"><title>-7</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"39,-99.3701 38,-99.3701 38,-98.3701 39,-98.3701 39,-99.3701\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"39.8\" cy=\"-99.8701\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- I&#45;&gt;&#45;7 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;-7</title>\n",
-        "<path d=\"M1.10614,-98.8701C3.20855,-98.8701 35.8616,-98.8701 37.9003,-98.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<path d=\"M1.10844,-99.8701C2.6468,-99.8701 20.196,-99.8701 30.7973,-99.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"30.9213,-102.32 37.9213,-99.8701 30.9212,-97.4202 30.9213,-102.32\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"102.87\" cy=\"-138.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98.3701\" y=\"-142.67\">0</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.8701\" y=\"-127.67\">\u24ff</text>\n",
+        "<ellipse cx=\"105.47\" cy=\"-139.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100.97\" y=\"-143.67\">0</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.4701\" y=\"-128.67\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;7&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>-7-&gt;0</title>\n",
-        "<path d=\"M39.0456,-98.899C40.0523,-99.5396 57.5624,-110.68 73.8402,-121.037\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"79.7486,-124.796 72.1517,-123.696 76.7956,-122.917 73.8426,-121.038 73.8426,-121.038 73.8426,-121.038 76.7956,-122.917 75.5336,-118.38 79.7486,-124.796 79.7486,-124.796\" stroke=\"black\"/>\n",
+        "<path d=\"M41.9051,-100.564C46.1242,-103.215 61.7127,-113.008 76.2726,-122.155\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"82.4135,-126.013 74.8104,-124.957 79.4498,-124.151 76.4862,-122.289 76.4862,-122.289 76.4862,-122.289 79.4498,-124.151 78.1619,-119.622 82.4135,-126.013 82.4135,-126.013\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node4\"><title>3</title>\n",
-        "<ellipse cx=\"102.87\" cy=\"-42.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102.87\" y=\"-39.1701\">3</text>\n",
+        "<ellipse cx=\"105.47\" cy=\"-43.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"105.47\" y=\"-40.1701\">3</text>\n",
         "</g>\n",
         "<!-- &#45;7&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>-7-&gt;3</title>\n",
-        "<path d=\"M39.0456,-98.8295C40.2587,-97.7489 65.4346,-75.3241 83.5422,-59.1952\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"88.9005,-54.4224 85.7686,-61.4305 86.287,-56.7503 83.6734,-59.0783 83.6734,-59.0783 83.6734,-59.0783 86.287,-56.7503 81.5782,-56.7261 88.9005,-54.4224 88.9005,-54.4224\" stroke=\"black\"/>\n",
+        "<path d=\"M41.515,-99.2412C45.8357,-95.441 68.8376,-75.21 85.7945,-60.2959\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"91.2776,-55.4733 88.1017,-62.4616 88.6495,-57.7848 86.0213,-60.0963 86.0213,-60.0963 86.0213,-60.0963 88.6495,-57.7848 83.941,-57.731 91.2776,-55.4733 91.2776,-55.4733\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node5\"><title>1</title>\n",
-        "<ellipse cx=\"256.61\" cy=\"-145.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"252.11\" y=\"-149.67\">1</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.61\" y=\"-134.67\">\u24ff</text>\n",
+        "<ellipse cx=\"259.21\" cy=\"-147.87\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.71\" y=\"-151.67\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"251.21\" y=\"-136.67\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>0-&gt;1</title>\n",
-        "<path d=\"M128.647,-147.561C134.808,-149.346 141.451,-150.958 147.74,-151.87 172.756,-155.498 201.327,-153.644 222.778,-151.074\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"229.764,-150.181 223.22,-154.193 226.293,-150.625 222.821,-151.068 222.821,-151.068 222.821,-151.068 226.293,-150.625 222.422,-147.944 229.764,-150.181 229.764,-150.181\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"176.24\" y=\"-158.67\">a</text>\n",
+        "<path d=\"M131.247,-148.561C137.408,-150.346 144.051,-151.958 150.34,-152.87 175.344,-156.497 203.916,-154.919 225.37,-152.612\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"232.358,-151.808 225.764,-155.738 228.881,-152.208 225.403,-152.608 225.403,-152.608 225.403,-152.608 228.881,-152.208 225.043,-149.479 232.358,-151.808 232.358,-151.808\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"178.84\" y=\"-159.67\">a</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node6\"><title>2</title>\n",
-        "<ellipse cx=\"406.35\" cy=\"-219.87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.35\" y=\"-216.17\">2</text>\n",
+        "<ellipse cx=\"408.95\" cy=\"-221.87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"408.95\" y=\"-218.17\">2</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>0-&gt;2</title>\n",
-        "<path d=\"M123.94,-156.275C147.427,-175.308 188.394,-204.486 229.74,-214.87 282.406,-228.097 346.753,-225.345 381.062,-222.442\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"388.313,-221.787 381.624,-225.554 384.827,-222.102 381.341,-222.417 381.341,-222.417 381.341,-222.417 384.827,-222.102 381.058,-219.279 388.313,-221.787 388.313,-221.787\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"251.11\" y=\"-226.67\">!a</text>\n",
+        "<path d=\"M126.086,-157.123C149.471,-176.363 190.651,-206.185 232.34,-216.87 284.941,-230.352 349.313,-227.5 383.644,-224.513\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"390.899,-223.84 384.22,-227.623 387.414,-224.163 383.929,-224.486 383.929,-224.486 383.929,-224.486 387.414,-224.163 383.638,-221.35 390.899,-223.84 390.899,-223.84\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.71\" y=\"-228.67\">!a</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>3-&gt;3</title>\n",
-        "<path d=\"M95.2021,-59.1603C93.3532,-69.2592 95.9091,-78.8701 102.87,-78.8701 108.091,-78.8701 110.834,-73.464 111.099,-66.5004\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"110.538,-59.1603 114.212,-65.9 110.805,-62.6502 111.071,-66.14 111.071,-66.14 111.071,-66.14 110.805,-62.6502 107.93,-66.38 110.538,-59.1603 110.538,-59.1603\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.3701\" y=\"-82.6701\">a</text>\n",
+        "<path d=\"M97.8021,-60.1603C95.9532,-70.2592 98.5091,-79.8701 105.47,-79.8701 110.691,-79.8701 113.434,-74.464 113.699,-67.5004\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"113.138,-60.1603 116.812,-66.9 113.405,-63.6502 113.671,-67.14 113.671,-67.14 113.671,-67.14 113.405,-63.6502 110.53,-67.38 113.138,-60.1603 113.138,-60.1603\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"101.97\" y=\"-83.6701\">a</text>\n",
         "</g>\n",
         "<!-- &#45;4 -->\n",
         "<g class=\"node\" id=\"node8\"><title>-4</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"257.11,-27.3701 256.11,-27.3701 256.11,-26.3701 257.11,-26.3701 257.11,-27.3701\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"259.21\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;&#45;4 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>3-&gt;-4</title>\n",
-        "<path d=\"M120.982,-41.0658C160.045,-36.9467 252.657,-27.1815 255.541,-26.8773\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.24\" y=\"-42.6701\">!a</text>\n",
+        "<path d=\"M123.582,-41.953C156.135,-38.3059 225.874,-30.4928 249.885,-27.8028\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"250.451,-30.2048 257.134,-26.9906 249.905,-25.3353 250.451,-30.2048\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"176.84\" y=\"-42.6701\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>1-&gt;0</title>\n",
-        "<path d=\"M230.833,-137.179C224.672,-135.394 218.029,-133.782 211.74,-132.87 186.725,-129.242 158.153,-131.096 136.702,-133.666\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"129.716,-134.559 136.26,-130.547 133.188,-134.115 136.66,-133.672 136.66,-133.672 136.66,-133.672 133.188,-134.115 137.059,-136.796 129.716,-134.559 129.716,-134.559\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"147.74\" y=\"-136.67\">!a &amp; b &amp; p</text>\n",
+        "<path d=\"M233.937,-138.657C227.647,-136.677 220.818,-134.879 214.34,-133.87 189.364,-129.981 160.79,-131.85 139.329,-134.491\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"132.338,-135.41 138.868,-131.375 135.809,-134.954 139.279,-134.498 139.279,-134.498 139.279,-134.498 135.809,-134.954 139.689,-137.621 132.338,-135.41 132.338,-135.41\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150.34\" y=\"-137.67\">!a &amp; b &amp; p</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>1-&gt;1</title>\n",
-        "<path d=\"M243.074,-169.416C241.403,-180.742 245.915,-190.74 256.61,-190.74 264.966,-190.74 269.548,-184.638 270.355,-176.568\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"270.146,-169.416 273.5,-176.321 270.249,-172.915 270.351,-176.413 270.351,-176.413 270.351,-176.413 270.249,-172.915 267.202,-176.506 270.146,-169.416 270.146,-169.416\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"237.11\" y=\"-194.54\">!b &amp; p</text>\n",
+        "<path d=\"M245.674,-171.416C244.003,-182.742 248.515,-192.74 259.21,-192.74 267.566,-192.74 272.148,-186.638 272.955,-178.568\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"272.746,-171.416 276.1,-178.321 272.849,-174.915 272.951,-178.413 272.951,-178.413 272.951,-178.413 272.849,-174.915 269.802,-178.506 272.746,-171.416 272.746,-171.416\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239.71\" y=\"-196.54\">!b &amp; p</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>1-&gt;2</title>\n",
-        "<path d=\"M281.02,-157.596C309.073,-171.647 355.724,-195.013 383.204,-208.778\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"389.755,-212.058 382.085,-211.74 386.625,-210.491 383.496,-208.924 383.496,-208.924 383.496,-208.924 386.625,-210.491 384.906,-206.107 389.755,-212.058 389.755,-212.058\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"310.98\" y=\"-201.67\">!a &amp; !b</text>\n",
+        "<path d=\"M283.62,-159.596C311.673,-173.647 358.324,-197.013 385.804,-210.778\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"392.355,-214.058 384.685,-213.74 389.225,-212.491 386.096,-210.924 386.096,-210.924 386.096,-210.924 389.225,-212.491 387.506,-208.107 392.355,-214.058 392.355,-214.058\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.58\" y=\"-203.67\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g class=\"node\" id=\"node7\"><title>-1</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"406.85,-116.37 405.85,-116.37 405.85,-115.37 406.85,-115.37 406.85,-116.37\" stroke=\"none\"/>\n",
+        "<ellipse cx=\"408.95\" cy=\"-117.87\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;&#45;1 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;-1</title>\n",
-        "<path d=\"M283.314,-141.645C304.39,-138.066 334.963,-132.613 361.48,-126.87 380.512,-122.748 403.841,-116.289 405.28,-115.89\" fill=\"none\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"301.48\" y=\"-142.67\">a &amp; b &amp; p</text>\n",
+        "<path d=\"M285.914,-143.645C306.99,-140.066 337.563,-134.613 364.08,-128.87 376.704,-126.136 391.219,-122.374 399.981,-120.033\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"none\" points=\"400.755,-122.362 406.871,-118.168 399.474,-117.633 400.755,-122.362\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"304.08\" y=\"-144.67\">a &amp; b &amp; p</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>2-&gt;2</title>\n",
-        "<path d=\"M397.985,-236.16C395.968,-246.259 398.757,-255.87 406.35,-255.87 412.046,-255.87 415.038,-250.464 415.327,-243.5\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"414.715,-236.16 418.436,-242.874 415.006,-239.648 415.297,-243.136 415.297,-243.136 415.297,-243.136 415.006,-239.648 412.158,-243.398 414.715,-236.16 414.715,-236.16\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.35\" y=\"-259.67\">1</text>\n",
+        "<path d=\"M400.585,-238.16C398.568,-248.259 401.357,-257.87 408.95,-257.87 414.646,-257.87 417.638,-252.464 417.927,-245.5\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"417.315,-238.16 421.036,-244.874 417.606,-241.648 417.897,-245.136 417.897,-245.136 417.897,-245.136 417.606,-241.648 414.758,-245.398 417.315,-238.16 417.315,-238.16\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"408.95\" y=\"-261.67\">1</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>-1-&gt;0</title>\n",
-        "<path d=\"M405.301,-115.867C403.239,-115.725 336.847,-111.183 283.48,-109.87 259.603,-109.283 253.5,-107.433 229.74,-109.87 192.715,-113.668 183.93,-118.178 147.74,-126.87 143.805,-127.815 139.688,-128.863 135.618,-129.934\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"128.856,-131.745 134.802,-126.891 132.237,-130.84 135.617,-129.934 135.617,-129.934 135.617,-129.934 132.237,-130.84 136.432,-132.977 128.856,-131.745 128.856,-131.745\" stroke=\"black\"/>\n",
+        "<path d=\"M406.975,-117.804C398.503,-117.23 336.482,-113.11 286.08,-111.87 262.203,-111.283 256.114,-109.572 232.34,-111.87 195.381,-115.442 186.495,-119.41 150.34,-127.87 146.4,-128.792 142.279,-129.826 138.208,-130.89\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"131.444,-132.694 137.395,-127.846 134.825,-131.792 138.207,-130.89 138.207,-130.89 138.207,-130.89 134.825,-131.792 139.019,-133.933 131.444,-132.694 131.444,-132.694\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>-1-&gt;1</title>\n",
-        "<path d=\"M405.308,-115.872C403.521,-115.961 346,-118.888 301.48,-129.87 297.245,-130.915 292.851,-132.227 288.554,-133.649\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"281.915,-135.95 287.498,-130.681 285.222,-134.804 288.529,-133.657 288.529,-133.657 288.529,-133.657 285.222,-134.804 289.561,-136.634 281.915,-135.95 281.915,-135.95\" stroke=\"black\"/>\n",
+        "<path d=\"M406.911,-117.925C398.869,-118.365 345.773,-121.585 304.08,-131.87 299.845,-132.915 295.451,-134.227 291.154,-135.649\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"284.515,-137.95 290.098,-132.681 287.822,-136.804 291.129,-135.657 291.129,-135.657 291.129,-135.657 287.822,-136.804 292.161,-138.634 284.515,-137.95 284.515,-137.95\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge15\"><title>-4-&gt;3</title>\n",
-        "<path d=\"M255.566,-26.8659C253.721,-26.6916 194.31,-21.1766 147.74,-28.8701 140.789,-30.0184 133.425,-32.0351 126.756,-34.1863\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"119.845,-36.5386 125.456,-31.3011 123.158,-35.4109 126.471,-34.2831 126.471,-34.2831 126.471,-34.2831 123.158,-35.4109 127.486,-37.2651 119.845,-36.5386 119.845,-36.5386\" stroke=\"black\"/>\n",
+        "<path d=\"M257.136,-26.7865C248.825,-26.1629 193.929,-22.4615 150.34,-29.8701 143.394,-31.0506 136.032,-33.0774 129.363,-35.2279\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"122.451,-37.5757 128.066,-32.3416 125.765,-36.45 129.079,-35.3242 129.079,-35.3242 129.079,-35.3242 125.765,-36.45 130.092,-38.3069 122.451,-37.5757 122.451,-37.5757\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node9\"><title>4</title>\n",
-        "<ellipse cx=\"406.35\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"401.85\" y=\"-30.6701\">4</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.35\" y=\"-15.6701\">\u24ff</text>\n",
+        "<ellipse cx=\"408.95\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.45\" y=\"-30.6701\">4</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"400.95\" y=\"-15.6701\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge16\"><title>-4-&gt;4</title>\n",
-        "<path d=\"M257.717,-26.8701C260.798,-26.8701 329.654,-26.8701 372.228,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"379.336,-26.8701 372.336,-30.0202 375.836,-26.8701 372.336,-26.8702 372.336,-26.8702 372.336,-26.8702 375.836,-26.8701 372.336,-23.7202 379.336,-26.8701 379.336,-26.8701\" stroke=\"black\"/>\n",
+        "<path d=\"M261.154,-26.8701C269.685,-26.8701 334.135,-26.8701 374.752,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"381.793,-26.8701 374.793,-30.0202 378.293,-26.8701 374.793,-26.8702 374.793,-26.8702 374.793,-26.8702 378.293,-26.8701 374.792,-23.7202 381.793,-26.8701 381.793,-26.8701\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge17\"><title>4-&gt;4</title>\n",
-        "<path d=\"M397.429,-52.2401C396.814,-62.7939 399.788,-71.7401 406.35,-71.7401 411.375,-71.7401 414.295,-66.496 415.112,-59.3013\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"415.271,-52.2401 418.263,-59.3092 415.192,-55.7392 415.114,-59.2383 415.114,-59.2383 415.114,-59.2383 415.192,-55.7392 411.964,-59.1674 415.271,-52.2401 415.271,-52.2401\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"400.85\" y=\"-75.5401\">!a</text>\n",
+        "<path d=\"M400.029,-52.2401C399.414,-62.7939 402.388,-71.7401 408.95,-71.7401 413.975,-71.7401 416.895,-66.496 417.712,-59.3013\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"417.871,-52.2401 420.863,-59.3092 417.792,-55.7392 417.714,-59.2383 417.714,-59.2383 417.714,-59.2383 417.792,-55.7392 414.564,-59.1674 417.871,-52.2401 417.871,-52.2401\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"403.45\" y=\"-75.5401\">!a</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g class=\"node\" id=\"node10\"><title>5</title>\n",
-        "<ellipse cx=\"494.22\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"494.22\" y=\"-23.1701\">5</text>\n",
+        "<ellipse cx=\"496.82\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"496.82\" y=\"-23.1701\">5</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge18\"><title>4-&gt;5</title>\n",
-        "<path d=\"M433.581,-26.8701C444.801,-26.8701 457.826,-26.8701 468.835,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"476.088,-26.8701 469.088,-30.0202 472.588,-26.8701 469.088,-26.8702 469.088,-26.8702 469.088,-26.8702 472.588,-26.8701 469.088,-23.7202 476.088,-26.8701 476.088,-26.8701\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"451.22\" y=\"-30.6701\">a</text>\n",
+        "<path d=\"M436.181,-26.8701C447.401,-26.8701 460.426,-26.8701 471.435,-26.8701\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"478.688,-26.8701 471.688,-30.0202 475.188,-26.8701 471.688,-26.8702 471.688,-26.8702 471.688,-26.8702 475.188,-26.8701 471.688,-23.7202 478.688,-26.8701 478.688,-26.8701\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"453.82\" y=\"-30.6701\">a</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge19\"><title>5-&gt;5</title>\n",
-        "<path d=\"M487.487,-43.9074C486.113,-53.728 488.357,-62.8701 494.22,-62.8701 498.618,-62.8701 500.98,-57.7276 501.306,-51.0134\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"500.954,-43.9074 504.447,-50.7428 501.127,-47.4031 501.301,-50.8988 501.301,-50.8988 501.301,-50.8988 501.127,-47.4031 498.154,-51.0547 500.954,-43.9074 500.954,-43.9074\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"494.22\" y=\"-66.6701\">1</text>\n",
+        "<path d=\"M490.087,-43.9074C488.713,-53.728 490.957,-62.8701 496.82,-62.8701 501.218,-62.8701 503.58,-57.7276 503.906,-51.0134\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"503.554,-43.9074 507.047,-50.7428 503.727,-47.4031 503.901,-50.8988 503.901,-50.8988 503.901,-50.8988 503.727,-47.4031 500.754,-51.0547 503.554,-43.9074 503.554,-43.9074\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"496.82\" y=\"-66.6701\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
@@ -1587,7 +1595,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd1684d6420> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989690> >"
        ]
       }
      ],
@@ -1632,14 +1640,14 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"346pt\" height=\"118pt\"\n",
-        " viewBox=\"0.00 0.00 346.15 117.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"349pt\" height=\"118pt\"\n",
+        " viewBox=\"0.00 0.00 348.75 117.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 113.74)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-113.74 342.149,-113.74 342.149,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"146.574\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"171.574\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"187.574\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-113.74 344.749,-113.74 344.749,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"147.874\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"172.874\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"188.874\" y=\"-95.5401\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
@@ -1653,57 +1661,58 @@
         "</g>\n",
         "<!-- &#45;1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>&#45;1</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"148.994,-27.3701 147.994,-27.3701 147.994,-26.3701 148.994,-26.3701 148.994,-27.3701\"/>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"149.794\" cy=\"-26.8701\" rx=\"1.8\" ry=\"1.8\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;&#45;1 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;&#45;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M103.053,-26.8701C123.467,-26.8701 146.505,-26.8701 147.925,-26.8701\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M103.383,-26.8701C116.92,-26.8701 131.598,-26.8701 140.496,-26.8701\"/>\n",
+        "<polygon fill=\"none\" stroke=\"black\" points=\"140.716,-29.3202 147.716,-26.8701 140.716,-24.4202 140.716,-29.3202\"/>\n",
         "<text text-anchor=\"start\" x=\"120.994\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;0 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M147.88,-26.8525C146.756,-26.68 137.529,-25.2874 129.994,-24.8701 123.512,-24.511 116.621,-24.4558 109.931,-24.575\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"102.777,-24.7668 109.69,-21.4303 106.276,-24.673 109.775,-24.5791 109.775,-24.5791 109.775,-24.5791 106.276,-24.673 109.859,-27.728 102.777,-24.7668 102.777,-24.7668\"/>\n",
+        "<g id=\"edge3\" class=\"edge\"><title>&#45;1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M147.778,-26.7236C144.962,-26.326 136.812,-25.2317 129.994,-24.8701 123.586,-24.5301 116.779,-24.4796 110.16,-24.5965\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"103.08,-24.7832 109.994,-21.4497 106.579,-24.6909 110.077,-24.5986 110.077,-24.5986 110.077,-24.5986 106.579,-24.6909 110.16,-27.7475 103.08,-24.7832 103.08,-24.7832\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node4\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"213.571\" cy=\"-26.8701\" rx=\"27.6545\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"start\" x=\"202.071\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">F(a)</text>\n",
-        "<text text-anchor=\"start\" x=\"205.571\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"216.171\" cy=\"-26.8701\" rx=\"27.6545\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"start\" x=\"204.671\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">F(a)</text>\n",
+        "<text text-anchor=\"start\" x=\"208.171\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "<!-- &#45;1&#45;&gt;1 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M149.04,-26.8701C149.945,-26.8701 164.032,-26.8701 178.71,-26.8701\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"185.908,-26.8701 178.908,-30.0202 182.408,-26.8701 178.908,-26.8702 178.908,-26.8702 178.908,-26.8702 182.408,-26.8701 178.908,-23.7202 185.908,-26.8701 185.908,-26.8701\"/>\n",
+        "<g id=\"edge4\" class=\"edge\"><title>&#45;1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M151.912,-26.8701C155.659,-26.8701 168.277,-26.8701 181.268,-26.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"188.47,-26.8701 181.47,-30.0202 184.97,-26.8701 181.47,-26.8702 181.47,-26.8702 181.47,-26.8702 184.97,-26.8701 181.47,-23.7202 188.47,-26.8701 188.47,-26.8701\"/>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M204.999,-52.6914C204.515,-63.0476 207.372,-71.7401 213.571,-71.7401 218.221,-71.7401 220.99,-66.8506 221.88,-60.0368\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"222.144,-52.6914 225.041,-59.7998 222.018,-56.1891 221.893,-59.6869 221.893,-59.6869 221.893,-59.6869 222.018,-56.1891 218.745,-59.574 222.144,-52.6914 222.144,-52.6914\"/>\n",
-        "<text text-anchor=\"start\" x=\"209.071\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M207.599,-52.6914C207.115,-63.0476 209.972,-71.7401 216.171,-71.7401 220.821,-71.7401 223.59,-66.8506 224.48,-60.0368\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"224.744,-52.6914 227.641,-59.7998 224.618,-56.1891 224.493,-59.6869 224.493,-59.6869 224.493,-59.6869 224.618,-56.1891 221.345,-59.574 224.744,-52.6914 224.744,-52.6914\"/>\n",
+        "<text text-anchor=\"start\" x=\"211.671\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g id=\"node5\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"311.149\" cy=\"-26.8701\" rx=\"27\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"311.149\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"313.749\" cy=\"-26.8701\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"313.749\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M241.195,-26.8701C252.264,-26.8701 265.233,-26.8701 276.917,-26.8701\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"283.998,-26.8701 276.998,-30.0202 280.498,-26.8701 276.998,-26.8702 276.998,-26.8702 276.998,-26.8702 280.498,-26.8701 276.998,-23.7202 283.998,-26.8701 283.998,-26.8701\"/>\n",
-        "<text text-anchor=\"start\" x=\"259.149\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.795,-26.8701C254.864,-26.8701 267.833,-26.8701 279.517,-26.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"286.598,-26.8701 279.598,-30.0202 283.098,-26.8701 279.598,-26.8702 279.598,-26.8702 279.598,-26.8702 283.098,-26.8701 279.598,-23.7202 286.598,-26.8701 286.598,-26.8701\"/>\n",
+        "<text text-anchor=\"start\" x=\"261.749\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M302.579,-44.28C300.98,-53.9579 303.836,-62.8701 311.149,-62.8701 316.519,-62.8701 319.486,-58.0637 320.049,-51.6773\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"319.718,-44.28 323.178,-51.1319 319.875,-47.7764 320.031,-51.2729 320.031,-51.2729 320.031,-51.2729 319.875,-47.7764 316.885,-51.414 319.718,-44.28 319.718,-44.28\"/>\n",
-        "<text text-anchor=\"start\" x=\"306.649\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M305.179,-44.28C303.58,-53.9579 306.436,-62.8701 313.749,-62.8701 319.119,-62.8701 322.086,-58.0637 322.649,-51.6773\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"322.318,-44.28 325.778,-51.1319 322.475,-47.7764 322.631,-51.2729 322.631,-51.2729 322.631,-51.2729 322.475,-47.7764 319.485,-51.414 322.318,-44.28 322.318,-44.28\"/>\n",
+        "<text text-anchor=\"start\" x=\"309.249\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd168433d50> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989e10> >"
        ]
       }
      ],
@@ -1777,20 +1786,11 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd168433d20> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dc4989ba0> >"
        ]
       }
      ],
      "prompt_number": 12
-    },
-    {
-     "cell_type": "code",
-     "collapsed": true,
-     "input": [],
-     "language": "python",
-     "metadata": {},
-     "outputs": [],
-     "prompt_number": null
     }
    ],
    "metadata": {}