diff --git a/NEWS b/NEWS
index f83b9d645..b87bdca74 100644
--- a/NEWS
+++ b/NEWS
@@ -112,6 +112,8 @@ New in spot 2.0.3a (not yet released)
 
   * Bindings for language_containment_checker were added.
 
+  * Bindings for randomize() were added.
+
   * Under IPython the spot.ltsmin modules now offers a
     %%pml magic to define promela models, compile them
     with spins, and dynamically load them.   This is
diff --git a/python/spot/impl.i b/python/spot/impl.i
index a544b4ff0..18044f8db 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -128,6 +128,7 @@
 #include <spot/twaalgos/magic.hh>
 #include <spot/twaalgos/minimize.hh>
 #include <spot/twaalgos/neverclaim.hh>
+#include <spot/twaalgos/randomize.hh>
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/strength.hh>
 #include <spot/twaalgos/sccfilter.hh>
@@ -435,6 +436,7 @@ namespace std {
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/minimize.hh>
 %include <spot/twaalgos/neverclaim.hh>
+%include <spot/twaalgos/randomize.hh>
 %include <spot/twaalgos/remfin.hh>
 %include <spot/twaalgos/strength.hh>
 %include <spot/twaalgos/sccfilter.hh>
diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb
index 4f79a6fca..2b73e6071 100644
--- a/tests/python/highlighting.ipynb
+++ b/tests/python/highlighting.ipynb
@@ -18,7 +18,7 @@
    "version": "3.4.3+"
   },
   "name": "",
-  "signature": "sha256:024df96495fac2f6862d63f78750ad9279a60f4e73ad02643779e5dc6a1f1982"
+  "signature": "sha256:30e1abf38b76bd072ff688d2b48f94eb5945807bfa9583a8f457ad3bc4966c4e"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -155,7 +155,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe2a411c588>"
+        "<IPython.core.display.SVG at 0x7fc0d01ef400>"
        ]
       }
      ],
@@ -255,7 +255,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a40ed8a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d01be8a0> >"
        ]
       }
      ],
@@ -357,7 +357,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fe2a4061f90> >"
+        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fc0d0132f90> >"
        ]
       }
      ],
@@ -572,7 +572,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf0f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b10f0> >"
        ]
       }
      ],
@@ -751,7 +751,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf0f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b10f0> >"
        ]
       }
      ],
@@ -831,7 +831,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf090> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1090> >"
        ]
       },
       {
@@ -877,7 +877,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf030> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1030> >"
        ]
       }
      ],
@@ -963,7 +963,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a4061fc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d0132fc0> >"
        ]
       }
      ],
@@ -1088,7 +1088,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a4061fc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d0132fc0> >"
        ]
       },
       {
@@ -1145,7 +1145,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf090> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1090> >"
        ]
       },
       {
@@ -1191,7 +1191,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf030> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1030> >"
        ]
       }
      ],
@@ -1398,7 +1398,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fe2a8edf150> >"
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fc0d57b1150> >"
        ]
       },
       {
@@ -1472,7 +1472,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf120> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1120> >"
        ]
       },
       {
@@ -1556,7 +1556,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf180> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1180> >"
        ]
       }
      ],
@@ -1702,12 +1702,157 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2a8edf270> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1270> >"
        ]
       }
      ],
      "prompt_number": 17
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Disappearing highlights\n",
+      "\n",
+      "As explained at the top of this notebook, named properties (such as highlights) are fragile, and you should not really on them being preserved across algorithms.  In-place algorithm are probably the worst, because they might modify the automaton and ignore the attached named properties.  \n",
+      "\n",
+      "`randomize()` is one such in-place algorithm: it reorder states or transitions of the automaton.   By doing so it renumber the states and edges, and that process would completely invalidate the highlights information.  Fortunately `randomize()` know about highlights: it will preserve highlighted states, but it will drop all highlighted edges."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "spot.randomize(b); b"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 18,
+       "svg": [
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"386pt\" height=\"318pt\"\n",
+        " viewBox=\"0.00 0.00 386.00 318.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 314)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-314 382,-314 382,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;4 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-153C2.79388,-153 17.1543,-153 30.6317,-153\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-153 30.9419,-156.15 34.4419,-153 30.9419,-153 30.9419,-153 30.9419,-153 34.4419,-153 30.9418,-149.85 37.9419,-153 37.9419,-153\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"#f15854\" stroke-width=\"2\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;1 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-153C85.1153,-153 99.5214,-153 111.67,-153\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-153 111.892,-156.15 115.392,-153 111.892,-153 111.892,-153 111.892,-153 115.392,-153 111.892,-149.85 118.892,-153 118.892,-153\"/>\n",
+        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"360\" cy=\"-211\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"360\" y=\"-207.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\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=\"M355.18,-228.41C354.28,-238.088 355.887,-247 360,-247 363.021,-247 364.69,-242.194 365.007,-235.807\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"364.82,-228.41 368.146,-235.328 364.908,-231.909 364.997,-235.408 364.997,-235.408 364.997,-235.408 364.908,-231.909 361.848,-235.487 364.82,-228.41 364.82,-228.41\"/>\n",
+        "<text text-anchor=\"start\" x=\"353.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "<text text-anchor=\"start\" x=\"352\" y=\"-250.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M352.733,-227.596C347.242,-248.863 349.664,-277 360,-277 369.246,-277 372.159,-254.485 368.741,-234.513\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"367.267,-227.596 371.807,-233.786 367.997,-231.019 368.726,-234.442 368.726,-234.442 368.726,-234.442 367.997,-231.019 365.645,-235.099 367.267,-227.596 367.267,-227.596\"/>\n",
+        "<text text-anchor=\"start\" x=\"355.5\" y=\"-280.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M150.726,-165.117C167.085,-179.773 197.086,-203.64 228,-213 264.017,-223.905 308.195,-219.88 334.942,-215.667\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"342.003,-214.486 335.618,-218.748 338.551,-215.064 335.099,-215.641 335.099,-215.641 335.099,-215.641 338.551,-215.064 334.579,-212.534 342.003,-214.486 342.003,-214.486\"/>\n",
+        "<text text-anchor=\"start\" x=\"228\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-169.664C128.406,-179.625 130.75,-189 137,-189 141.688,-189 144.178,-183.727 144.471,-176.888\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"144.031,-169.664 147.601,-176.46 144.244,-173.158 144.456,-176.651 144.456,-176.651 144.456,-176.651 144.244,-173.158 141.312,-176.842 144.031,-169.664 144.031,-169.664\"/>\n",
+        "<text text-anchor=\"start\" x=\"123.5\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M155.109,-153C173.324,-153 202.31,-153 222.956,-153\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"230.149,-153 223.149,-156.15 226.649,-153 223.149,-153 223.149,-153 223.149,-153 226.649,-153 223.149,-149.85 230.149,-153 230.149,-153\"/>\n",
+        "<text text-anchor=\"start\" x=\"173\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M149.102,-139.313C168.696,-115.156 209.453,-64.9068 231.876,-37.2621\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"236.369,-31.7237 234.405,-39.1445 234.164,-34.4419 231.959,-37.1602 231.959,-37.1602 231.959,-37.1602 234.164,-34.4419 229.513,-35.1759 236.369,-31.7237 236.369,-31.7237\"/>\n",
+        "<text text-anchor=\"start\" x=\"174.5\" y=\"-113.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M264.726,-161.065C283.578,-171.05 315.818,-188.127 337.267,-199.489\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"343.551,-202.817 335.891,-202.324 340.458,-201.179 337.365,-199.54 337.365,-199.54 337.365,-199.54 340.458,-201.179 338.839,-196.757 343.551,-202.817 343.551,-202.817\"/>\n",
+        "<text text-anchor=\"start\" x=\"287\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M238.925,-168.541C236.23,-178.909 239.422,-189 248.5,-189 255.45,-189 258.95,-183.085 258.999,-175.659\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"258.075,-168.541 262.1,-175.077 258.526,-172.012 258.977,-175.483 258.977,-175.483 258.977,-175.483 258.526,-172.012 255.853,-175.889 258.075,-168.541 258.075,-168.541\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.501,-35.4099C242.568,-45.0879 244.234,-54 248.5,-54 251.633,-54 253.363,-49.1936 253.692,-42.8073\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"253.499,-35.4099 256.831,-42.3252 253.59,-38.9087 253.682,-42.4075 253.682,-42.4075 253.682,-42.4075 253.59,-38.9087 250.533,-42.4899 253.499,-35.4099 253.499,-35.4099\"/>\n",
+        "<text text-anchor=\"start\" x=\"230\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"240.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M240.963,-34.5959C235.269,-55.8633 237.781,-84 248.5,-84 258.088,-84 261.11,-61.4854 257.564,-41.5132\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"256.037,-34.5959 260.622,-40.7517 256.792,-38.0135 257.546,-41.4311 257.546,-41.4311 257.546,-41.4311 256.792,-38.0135 254.471,-42.1106 256.037,-34.5959 256.037,-34.5959\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; 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 0x7fc0d57b1270> >"
+       ]
+      }
+     ],
+     "prompt_number": 18
+    },
     {
      "cell_type": "markdown",
      "metadata": {},
@@ -1721,7 +1866,8 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "display(b.show('.<4'), b.show('.<2'))"
+      "spot.highlight_nondet_edges(b, 4)  # let's get those highlighted edges back\n",
+      "display(b, b.show('.<4'), b.show('.<2'))"
      ],
      "language": "python",
      "metadata": {},
@@ -1730,15 +1876,136 @@
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"302pt\" viewBox=\"0.00 0.00 276.50 301.50\" width=\"277pt\" 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.5)\">\n",
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"386pt\" height=\"318pt\"\n",
+        " viewBox=\"0.00 0.00 386.00 318.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 314)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-297.5 272.5,-297.5 272.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-314 382,-314 382,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;4 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-153C2.79388,-153 17.1543,-153 30.6317,-153\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-153 30.9419,-156.15 34.4419,-153 30.9419,-153 30.9419,-153 30.9419,-153 34.4419,-153 30.9418,-149.85 37.9419,-153 37.9419,-153\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"#f15854\" stroke-width=\"2\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;1 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-153C85.1153,-153 99.5214,-153 111.67,-153\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-153 111.892,-156.15 115.392,-153 111.892,-153 111.892,-153 111.892,-153 115.392,-153 111.892,-149.85 118.892,-153 118.892,-153\"/>\n",
+        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"360\" cy=\"-211\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"360\" y=\"-207.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\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=\"M355.18,-228.41C354.28,-238.088 355.887,-247 360,-247 363.021,-247 364.69,-242.194 365.007,-235.807\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"364.82,-228.41 368.146,-235.328 364.908,-231.909 364.997,-235.408 364.997,-235.408 364.997,-235.408 364.908,-231.909 361.848,-235.487 364.82,-228.41 364.82,-228.41\"/>\n",
+        "<text text-anchor=\"start\" x=\"353.5\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "<text text-anchor=\"start\" x=\"352\" y=\"-250.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M352.733,-227.596C347.242,-248.863 349.664,-277 360,-277 369.246,-277 372.159,-254.485 368.741,-234.513\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"367.267,-227.596 371.807,-233.786 367.997,-231.019 368.726,-234.442 368.726,-234.442 368.726,-234.442 367.997,-231.019 365.645,-235.099 367.267,-227.596 367.267,-227.596\"/>\n",
+        "<text text-anchor=\"start\" x=\"355.5\" y=\"-280.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M150.726,-165.117C167.085,-179.773 197.086,-203.64 228,-213 264.017,-223.905 308.195,-219.88 334.942,-215.667\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"342.003,-214.486 335.618,-218.748 338.551,-215.064 335.099,-215.641 335.099,-215.641 335.099,-215.641 338.551,-215.064 334.579,-212.534 342.003,-214.486 342.003,-214.486\"/>\n",
+        "<text text-anchor=\"start\" x=\"228\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M129.969,-169.664C128.406,-179.625 130.75,-189 137,-189 141.688,-189 144.178,-183.727 144.471,-176.888\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"144.031,-169.664 147.601,-176.46 144.743,-173.127 144.955,-176.621 144.456,-176.651 143.957,-176.682 143.745,-173.188 141.312,-176.842 144.031,-169.664 144.031,-169.664\"/>\n",
+        "<text text-anchor=\"start\" x=\"123.5\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M155.109,-153C173.324,-153 202.31,-153 222.956,-153\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"230.149,-153 223.149,-156.15 226.649,-153.5 223.149,-153.5 223.149,-153 223.149,-152.5 226.649,-152.5 223.149,-149.85 230.149,-153 230.149,-153\"/>\n",
+        "<text text-anchor=\"start\" x=\"173\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M149.102,-139.313C168.696,-115.156 209.453,-64.9068 231.876,-37.2621\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"236.369,-31.7237 234.405,-39.1445 234.552,-34.7569 232.347,-37.4752 231.959,-37.1602 231.571,-36.8452 233.775,-34.127 229.513,-35.1759 236.369,-31.7237 236.369,-31.7237\"/>\n",
+        "<text text-anchor=\"start\" x=\"174.5\" y=\"-113.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M264.726,-161.065C283.578,-171.05 315.818,-188.127 337.267,-199.489\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"343.551,-202.817 335.891,-202.324 340.458,-201.179 337.365,-199.54 337.365,-199.54 337.365,-199.54 340.458,-201.179 338.839,-196.757 343.551,-202.817 343.551,-202.817\"/>\n",
+        "<text text-anchor=\"start\" x=\"287\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M238.925,-168.541C236.23,-178.909 239.422,-189 248.5,-189 255.45,-189 258.95,-183.085 258.999,-175.659\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"258.075,-168.541 262.1,-175.077 258.526,-172.012 258.977,-175.483 258.977,-175.483 258.977,-175.483 258.526,-172.012 255.853,-175.889 258.075,-168.541 258.075,-168.541\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.501,-35.4099C242.568,-45.0879 244.234,-54 248.5,-54 251.633,-54 253.363,-49.1936 253.692,-42.8073\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"253.499,-35.4099 256.831,-42.3252 253.59,-38.9087 253.682,-42.4075 253.682,-42.4075 253.682,-42.4075 253.59,-38.9087 250.533,-42.4899 253.499,-35.4099 253.499,-35.4099\"/>\n",
+        "<text text-anchor=\"start\" x=\"230\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"240.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M240.963,-34.5959C235.269,-55.8633 237.781,-84 248.5,-84 258.088,-84 261.11,-61.4854 257.564,-41.5132\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"256.037,-34.5959 260.622,-40.7517 256.792,-38.0135 257.546,-41.4311 257.546,-41.4311 257.546,-41.4311 256.792,-38.0135 254.471,-42.1106 256.037,-34.5959 256.037,-34.5959\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; 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 0x7fc0d57b1270> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"254pt\" viewBox=\"0.00 0.00 335.00 253.50\" width=\"335pt\" 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 249.5)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-249.5 331,-249.5 331,4 -4,4\" stroke=\"none\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
         "<ellipse cx=\"56\" cy=\"-153\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-149.3\">0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-149.3\">4</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
@@ -1764,67 +2031,70 @@
         "</g>\n",
         "<!-- u1 -->\n",
         "<g class=\"node\" id=\"node4\"><title>u1</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"263,-293.5 237,-293.5 237,-270.5 263,-270.5 263,-293.5\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250\" y=\"-278.3\">...</text>\n",
+        "<polygon fill=\"#ffffaa\" points=\"259,-245.5 233,-245.5 233,-222.5 259,-222.5 259,-245.5\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"246\" y=\"-230.3\">...</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;u1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>1-&gt;u1</title>\n",
-        "<path d=\"M149.461,-166.319C169.751,-189.899 211.956,-238.949 234.334,-264.956\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"239.053,-270.44 232.1,-267.189 236.77,-267.787 234.488,-265.134 234.488,-265.134 234.488,-265.134 236.77,-267.787 236.875,-263.08 239.053,-270.44 239.053,-270.44\" stroke=\"black\"/>\n",
+        "<path d=\"M151.988,-163.589C171.271,-178.187 206.026,-204.497 227.157,-220.493\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"232.989,-224.907 225.506,-223.194 230.198,-222.795 227.408,-220.682 227.408,-220.682 227.408,-220.682 230.198,-222.795 229.309,-218.171 232.989,-224.907 232.989,-224.907\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node5\"><title>2</title>\n",
-        "<ellipse cx=\"250\" cy=\"-153\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250\" y=\"-149.3\">2</text>\n",
+        "<ellipse cx=\"246\" cy=\"-153\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"246\" y=\"-149.3\">3</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
-        "<path d=\"M155.344,-153C173.998,-153 203.797,-153 224.763,-153\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"231.778,-153 224.778,-156.15 228.278,-153 224.778,-153 224.778,-153 224.778,-153 228.278,-153 224.778,-149.85 231.778,-153 231.778,-153\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-156.8\">!a &amp; !b</text>\n",
+        "<path d=\"M155.191,-153C172.897,-153 200.648,-153 220.616,-153\" fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
+        "<polygon fill=\"#60bd68\" points=\"227.851,-153 220.851,-156.15 224.351,-153.5 220.851,-153.5 220.851,-153 220.851,-152.5 224.351,-152.5 220.851,-149.85 227.851,-153 227.851,-153\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-156.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node6\"><title>3</title>\n",
-        "<ellipse cx=\"250\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"250\" y=\"-14.3\">3</text>\n",
+        "<ellipse cx=\"246\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"246\" y=\"-14.3\">2</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;3</title>\n",
-        "<path d=\"M149.049,-139.562C168.81,-115.528 210.269,-65.1054 233.092,-37.3471\" fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
-        "<polygon fill=\"#60bd68\" points=\"237.665,-31.7854 235.653,-39.193 235.829,-34.8065 233.606,-37.51 233.22,-37.1924 232.833,-36.8749 235.056,-34.1714 230.786,-35.1919 237.665,-31.7854 237.665,-31.7854\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"176.5\" y=\"-112.8\">a &amp; b</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;2</title>\n",
-        "<path d=\"M245.001,-170.41C244.068,-180.088 245.734,-189 250,-189 253.133,-189 254.863,-184.194 255.192,-177.807\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"254.999,-170.41 258.331,-177.325 255.09,-173.909 255.182,-177.408 255.182,-177.408 255.182,-177.408 255.09,-173.909 252.033,-177.49 254.999,-170.41 254.999,-170.41\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"245.5\" y=\"-192.8\">b</text>\n",
+        "<path d=\"M148.849,-139.313C167.995,-115.156 207.822,-64.9068 229.733,-37.2621\" fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
+        "<polygon fill=\"#60bd68\" points=\"234.123,-31.7237 232.243,-39.1662 232.341,-34.7772 230.166,-37.5201 229.775,-37.2095 229.383,-36.899 231.557,-34.156 227.306,-35.2529 234.123,-31.7237 234.123,-31.7237\" stroke=\"#60bd68\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.5\" y=\"-109.8\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>2-&gt;2</title>\n",
-        "<path d=\"M242.044,-169.308C236.903,-186.96 239.555,-207 250,-207 259.058,-207 262.256,-191.93 259.592,-176.415\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"257.956,-169.308 262.596,-175.423 258.742,-172.719 259.527,-176.13 259.527,-176.13 259.527,-176.13 258.742,-172.719 256.457,-176.837 257.956,-169.308 257.956,-169.308\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243.5\" y=\"-225.8\">!b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-210.8\">\u24ff</text>\n",
+        "<path d=\"M239.621,-170.037C238.319,-179.858 240.445,-189 246,-189 250.166,-189 252.404,-183.858 252.713,-177.143\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"252.379,-170.037 255.854,-176.882 252.543,-173.533 252.708,-177.03 252.708,-177.03 252.708,-177.03 252.543,-173.533 249.561,-177.177 252.379,-170.037 252.379,-170.037\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"229\" y=\"-192.8\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- u2 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>u2</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"327,-164.5 301,-164.5 301,-141.5 327,-141.5 327,-164.5\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"314\" y=\"-149.3\">...</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;u2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;u2</title>\n",
+        "<path d=\"M264.341,-153C273.382,-153 284.464,-153 293.767,-153\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"300.774,-153 293.774,-156.15 297.274,-153 293.774,-153 293.774,-153 293.774,-153 297.274,-153 293.774,-149.85 300.774,-153 300.774,-153\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>3-&gt;3</title>\n",
-        "<path d=\"M245.001,-35.4099C244.068,-45.0879 245.734,-54 250,-54 253.133,-54 254.863,-49.1936 255.192,-42.8073\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"254.999,-35.4099 258.331,-42.3252 255.09,-38.9087 255.182,-42.4075 255.182,-42.4075 255.182,-42.4075 255.09,-38.9087 252.033,-42.4899 254.999,-35.4099 254.999,-35.4099\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233\" y=\"-57.8\">a &amp; b</text>\n",
+        "<path d=\"M242.764,-35.7817C242.214,-45.3149 243.293,-54 246,-54 247.988,-54 249.098,-49.3161 249.329,-43.0521\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"249.236,-35.7817 252.476,-42.7406 249.281,-39.2814 249.326,-42.7812 249.326,-42.7812 249.326,-42.7812 249.281,-39.2814 246.176,-42.8217 249.236,-35.7817 249.236,-35.7817\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"227.5\" y=\"-72.8\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-57.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>3-&gt;3</title>\n",
-        "<path d=\"M242.044,-34.3083C236.903,-51.9604 239.555,-72 250,-72 259.058,-72 262.256,-56.9299 259.592,-41.4154\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"257.956,-34.3083 262.596,-40.4232 258.742,-37.7191 259.527,-41.1299 259.527,-41.1299 259.527,-41.1299 258.742,-37.7191 256.457,-41.8366 257.956,-34.3083 257.956,-34.3083\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.5\" y=\"-90.8\">a &amp; !b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-75.8\">\u24ff</text>\n",
+        "<path d=\"M240.991,-35.5771C237.545,-56.718 239.215,-84 246,-84 252.043,-84 254.028,-62.3596 251.956,-42.6907\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"251.009,-35.5771 255.056,-42.1002 251.471,-39.0465 251.933,-42.5159 251.933,-42.5159 251.933,-42.5159 251.471,-39.0465 248.811,-42.9316 251.009,-35.5771 251.009,-35.5771\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"229\" y=\"-87.8\">a &amp; b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe2a4013240>"
+        "<IPython.core.display.SVG at 0x7fc0d00e1518>"
        ]
       },
       {
@@ -1839,7 +2109,7 @@
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
         "<ellipse cx=\"56\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.3\">0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.3\">4</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
@@ -1877,11 +2147,11 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe2a402f860>"
+        "<IPython.core.display.SVG at 0x7fc0d00feb38>"
        ]
       }
      ],
-     "prompt_number": 18
+     "prompt_number": 19
     }
    ],
    "metadata": {}