diff --git a/NEWS b/NEWS
index 23204222e..fb8177c7a 100644
--- a/NEWS
+++ b/NEWS
@@ -126,6 +126,11 @@ New in spot 2.11.6.dev  (not yet released)
     drop_false_edges=False argument to disable the historical behavior
     of ignoring edges labeled by False.
 
+  - Calling aut.highlight_state(s, None) or aut.highlight_edge(e,
+    None) may now be used to remove the highlighting color of some
+    given state or edge.  Use aut.remove_highlight_states() or
+    aut.remove_highlight_edges() to remove all colors. (Issue #554.)
+
   Bugs fixed:
 
   - tgba_determinize()'s use_simulation option would cause it to
diff --git a/python/spot/impl.i b/python/spot/impl.i
index e8160c362..e1dd7f296 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -407,6 +407,16 @@ namespace swig
     $result = SWIG_FromCharPtr($1->c_str());
 }
 
+%typemap(typecheck, precedence=2000) std::nullptr_t {
+     $1 = $input == Py_None;
+}
+
+%typemap(in) std::nullptr_t {
+    if ($input != Py_None)
+      %argument_fail(SWIG_TypeError, "std::nullptr_t", $symname, $argnum);
+    $1 = nullptr;
+}
+
 // For some reason, Swig can convert [aut1,aut2,...]  into
 // std::vector<spot::twa_graph_ptr>, but not into
 // std::vector<spot::const_twa_graph_ptr>.  Let's fix that by using
@@ -1037,6 +1047,21 @@ static void* ptr_for_bdddict(PyObject* obj)
     return self;
   }
 
+  twa* highlight_state(unsigned state, std::nullptr_t color) // color=None
+  {
+    (void) color;
+    if (std::map<unsigned, unsigned>* hs =
+        self->get_named_prop<std::map<unsigned, unsigned>>("highlight-states"))
+      hs->erase(state);
+    return self;
+  }
+
+  twa* remove_highlight_states()
+  {
+    self->set_named_prop("highlight-states", nullptr);
+    return self;
+  }
+
   twa* highlight_edge(unsigned edge, unsigned color)
   {
     auto ht =
@@ -1049,6 +1074,21 @@ static void* ptr_for_bdddict(PyObject* obj)
     (*ht)[edge] = color;
     return self;
   }
+
+  twa* highlight_edge(unsigned edge, std::nullptr_t color) // color=None
+  {
+    (void) color;
+    if (std::map<unsigned, unsigned>* hs =
+        self->get_named_prop<std::map<unsigned, unsigned>>("highlight-edges"))
+      hs->erase(edge);
+    return self;
+  }
+
+  twa* remove_highlight_edges()
+  {
+    self->set_named_prop("highlight-edges", nullptr);
+    return self;
+  }
 }
 
 %extend spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb
index a35f88334..6fe0856a1 100644
--- a/tests/python/highlighting.ipynb
+++ b/tests/python/highlighting.ipynb
@@ -247,7 +247,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bb720> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e410bd0> >"
       ]
      },
      "execution_count": 4,
@@ -359,7 +359,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fb7ec3bbb40> >"
+       "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fe86e4110e0> >"
       ]
      },
      "execution_count": 5,
@@ -469,7 +469,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bb720> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e410bd0> >"
       ]
      },
      "execution_count": 6,
@@ -549,6 +549,235 @@
     "print(a.to_str('HOA', '1.1'))"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Removing highlights"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Use `None` as the color to remove some specific highlights."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"305pt\" height=\"148pt\"\n",
+       " viewBox=\"0.00 0.00 305.00 148.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 144)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-144 301,-144 301,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"127\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"56\" cy=\"-62\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-58.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;2 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-62C2.79,-62 17.15,-62 30.63,-62\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-62 30.94,-65.15 34.44,-62 30.94,-62 30.94,-62 30.94,-62 34.44,-62 30.94,-58.85 37.94,-62 37.94,-62\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"#ff7f00\" stroke-width=\"2\" d=\"M49.62,-79.04C48.32,-88.86 50.45,-98 56,-98 60.17,-98 62.4,-92.86 62.71,-86.14\"/>\n",
+       "<polygon fill=\"#ff7f00\" stroke=\"#ff7f00\" stroke-width=\"2\" points=\"62.38,-79.04 65.85,-85.88 63.04,-82.51 63.21,-86.01 62.71,-86.03 62.21,-86.05 62.04,-82.56 59.56,-86.18 62.38,-79.04 62.38,-79.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"38.5\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"275\" cy=\"-62\" rx=\"18\" ry=\"18\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"275\" cy=\"-62\" rx=\"22\" ry=\"22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"275\" y=\"-58.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.55,-66.19C101.64,-72.75 160.43,-84.1 210,-78 222.33,-76.48 235.7,-73.38 247.02,-70.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"253.78,-68.41 247.89,-73.33 250.41,-69.35 247.04,-70.3 247.04,-70.3 247.04,-70.3 250.41,-69.35 246.18,-67.27 253.78,-68.41 253.78,-68.41\"/>\n",
+       "<text text-anchor=\"start\" x=\"188.5\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"192\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"start\" x=\"187.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;1 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"#ff4da0\" stroke-width=\"2\" d=\"M73.43,-56.6C97.04,-48.85 140.68,-34.52 167.63,-25.67\"/>\n",
+       "<polygon fill=\"#ff4da0\" stroke=\"#ff4da0\" stroke-width=\"2\" points=\"174.43,-23.44 168.77,-28.62 171.27,-25.01 167.94,-26.1 167.78,-25.62 167.63,-25.15 170.95,-24.06 166.8,-22.63 174.43,-23.44 174.43,-23.44\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-53.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b &amp; !c</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M267.32,-82.99C266.37,-93.09 268.93,-102 275,-102 279.55,-102 282.13,-96.99 282.74,-90.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"282.68,-82.99 285.88,-89.97 282.71,-86.49 282.73,-89.99 282.73,-89.99 282.73,-89.99 282.71,-86.49 279.58,-90.01 282.68,-82.99 282.68,-82.99\"/>\n",
+       "<text text-anchor=\"start\" x=\"270.5\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M208.24,-26.28C219.74,-32.52 235.76,-41.23 249.11,-48.48\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"255.42,-51.91 247.77,-51.33 252.34,-50.24 249.27,-48.57 249.27,-48.57 249.27,-48.57 252.34,-50.24 250.77,-45.8 255.42,-51.91 255.42,-51.91\"/>\n",
+       "<text text-anchor=\"start\" x=\"228\" y=\"-43.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M185.27,-35.04C183.89,-44.86 186.14,-54 192,-54 196.4,-54 198.76,-48.86 199.09,-42.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"198.73,-35.04 202.23,-41.87 198.91,-38.53 199.08,-42.03 199.08,-42.03 199.08,-42.03 198.91,-38.53 195.93,-42.18 198.73,-35.04 198.73,-35.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"174\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">b &amp; !c</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fe86e411e30> >"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a.highlight_state(0, None).highlight_edges([4, 2], None)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Or use `remove_highlight_states()` or `remove_highlight_edges()` to remove all highlights."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {
+    "scrolled": true
+   },
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"305pt\" height=\"148pt\"\n",
+       " viewBox=\"0.00 0.00 305.00 148.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 144)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-144 301,-144 301,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"127\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-62\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-58.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;2 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-62C2.79,-62 17.15,-62 30.63,-62\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-62 30.94,-65.15 34.44,-62 30.94,-62 30.94,-62 30.94,-62 34.44,-62 30.94,-58.85 37.94,-62 37.94,-62\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.62,-79.04C48.32,-88.86 50.45,-98 56,-98 60.17,-98 62.4,-92.86 62.71,-86.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-79.04 65.85,-85.88 62.54,-82.53 62.71,-86.03 62.71,-86.03 62.71,-86.03 62.54,-82.53 59.56,-86.18 62.38,-79.04 62.38,-79.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"38.5\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"275\" cy=\"-62\" rx=\"18\" ry=\"18\"/>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"275\" cy=\"-62\" rx=\"22\" ry=\"22\"/>\n",
+       "<text text-anchor=\"middle\" x=\"275\" y=\"-58.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.55,-66.19C101.64,-72.75 160.43,-84.1 210,-78 222.33,-76.48 235.7,-73.38 247.02,-70.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"253.78,-68.41 247.89,-73.33 250.41,-69.35 247.04,-70.3 247.04,-70.3 247.04,-70.3 250.41,-69.35 246.18,-67.27 253.78,-68.41 253.78,-68.41\"/>\n",
+       "<text text-anchor=\"start\" x=\"188.5\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"192\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"start\" x=\"187.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;1 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M73.43,-56.6C97.04,-48.85 140.68,-34.52 167.63,-25.67\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"174.43,-23.44 168.77,-28.62 171.11,-24.53 167.78,-25.62 167.78,-25.62 167.78,-25.62 171.11,-24.53 166.8,-22.63 174.43,-23.44 174.43,-23.44\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-53.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b &amp; !c</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M267.32,-82.99C266.37,-93.09 268.93,-102 275,-102 279.55,-102 282.13,-96.99 282.74,-90.22\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"282.68,-82.99 285.88,-89.97 282.71,-86.49 282.73,-89.99 282.73,-89.99 282.73,-89.99 282.71,-86.49 279.58,-90.01 282.68,-82.99 282.68,-82.99\"/>\n",
+       "<text text-anchor=\"start\" x=\"270.5\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;0 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M208.24,-26.28C219.74,-32.52 235.76,-41.23 249.11,-48.48\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"255.42,-51.91 247.77,-51.33 252.34,-50.24 249.27,-48.57 249.27,-48.57 249.27,-48.57 252.34,-50.24 250.77,-45.8 255.42,-51.91 255.42,-51.91\"/>\n",
+       "<text text-anchor=\"start\" x=\"228\" y=\"-43.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M185.27,-35.04C183.89,-44.86 186.14,-54 192,-54 196.4,-54 198.76,-48.86 199.09,-42.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"198.73,-35.04 202.23,-41.87 198.91,-38.53 199.08,-42.03 199.08,-42.03 199.08,-42.03 198.91,-38.53 195.93,-42.18 198.73,-35.04 198.73,-35.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"174\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">b &amp; !c</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fe86e411c50> >"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a.remove_highlight_states().remove_highlight_edges()"
+   ]
+  },
   {
    "cell_type": "markdown",
    "metadata": {},
@@ -562,7 +791,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
@@ -702,10 +931,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bba50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e4123a0> >"
       ]
      },
-     "execution_count": 8,
+     "execution_count": 10,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -716,7 +945,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [
     {
@@ -741,7 +970,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 12,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -757,7 +986,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 13,
    "metadata": {},
    "outputs": [
     {
@@ -897,10 +1126,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bba50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e4123a0> >"
       ]
      },
-     "execution_count": 11,
+     "execution_count": 13,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -920,7 +1149,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 14,
    "metadata": {},
    "outputs": [
     {
@@ -1235,7 +1464,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3dc8d0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e4121f0> >"
       ]
      },
      "metadata": {},
@@ -1496,7 +1725,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60adc0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e410f90> >"
       ]
      },
      "metadata": {},
@@ -1679,7 +1908,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60a7f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e410ff0> >"
       ]
      },
      "metadata": {},
@@ -1734,7 +1963,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 15,
    "metadata": {},
    "outputs": [
     {
@@ -1796,7 +2025,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bbdb0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e413030> >"
       ]
      },
      "metadata": {},
@@ -1851,7 +2080,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60b810> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412280> >"
       ]
      },
      "metadata": {},
@@ -1866,7 +2095,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 16,
    "metadata": {},
    "outputs": [
     {
@@ -1945,10 +2174,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bbc60> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412310> >"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 16,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1959,7 +2188,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 17,
    "metadata": {},
    "outputs": [
     {
@@ -1982,7 +2211,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 18,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -1995,7 +2224,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 19,
    "metadata": {},
    "outputs": [
     {
@@ -2074,7 +2303,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bbc60> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412310> >"
       ]
      },
      "metadata": {},
@@ -2139,7 +2368,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3bbdb0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e413030> >"
       ]
      },
      "metadata": {},
@@ -2194,7 +2423,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60b810> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412280> >"
       ]
      },
      "metadata": {},
@@ -2214,7 +2443,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 20,
    "metadata": {},
    "outputs": [
     {
@@ -2420,7 +2649,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fb7ef60a7f0> >"
+       "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fe86e413c00> >"
       ]
      },
      "metadata": {},
@@ -2505,7 +2734,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60af10> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e4109c0> >"
       ]
      },
      "metadata": {},
@@ -2602,7 +2831,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ef60b840> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e413bd0> >"
       ]
      },
      "metadata": {},
@@ -2631,7 +2860,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 21,
    "metadata": {},
    "outputs": [
     {
@@ -2771,10 +3000,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3dd860> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412b50> >"
       ]
      },
-     "execution_count": 19,
+     "execution_count": 21,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2799,7 +3028,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 22,
    "metadata": {},
    "outputs": [
     {
@@ -2939,10 +3168,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3dd860> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412b50> >"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 22,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2962,7 +3191,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 23,
    "metadata": {},
    "outputs": [
     {
@@ -3102,7 +3331,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb7ec3dd860> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe86e412b50> >"
       ]
      },
      "metadata": {},
@@ -3336,7 +3565,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 24,
    "metadata": {},
    "outputs": [
     {
@@ -3582,7 +3811,7 @@
        "<spot.jupyter.SVG object>"
       ]
      },
-     "execution_count": 22,
+     "execution_count": 24,
      "metadata": {},
      "output_type": "execute_result"
     }