From 091251b5b725ddca47e533c0b822f9fb95d1e992 Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Sat, 13 Feb 2016 18:50:15 +0100
Subject: [PATCH] Provide support for %dve and %require

* NEWS, python/spot/ltsmin.i,
tests/python/ltsmin.ipynb: Here.
---
 NEWS                      |    3 +
 python/spot/ltsmin.i      |   76 ++
 tests/python/ltsmin.ipynb | 1955 +++++++++++++++++++------------------
 3 files changed, 1106 insertions(+), 928 deletions(-)

diff --git a/NEWS b/NEWS
index 52e43df6e..6a77bc885 100644
--- a/NEWS
+++ b/NEWS
@@ -87,6 +87,9 @@ New in spot 1.99.7a (not yet released)
   * The ltsmin interface has been binded in Python.  See
     https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example.
 
+  * The ltsmin interface support two extra 'magic commands' when ipython
+    is used: %dve and %%require.
+
   * spot.setup() sets de maximum number of states to display in
     automata to 50 by default, as more states is likely to be
     unreadable (and slow to process by GraphViz).  This can be
diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i
index 5b33b525b..31c858ecf 100644
--- a/python/spot/ltsmin.i
+++ b/python/spot/ltsmin.i
@@ -106,4 +106,80 @@ class model:
         res += type
       res += '\n';
     return res
+
+# Load IPython specific support if we can.
+try:
+    # Load only if we are running IPython.
+    __IPYTHON__
+
+    from IPython.core.magic import (Magics, magics_class, line_cell_magic)
+    from IPython.core.magic_arguments \
+        import (argument, magic_arguments, parse_argstring)
+    import os
+    import tempfile
+    import sys
+    import shutil
+    try:
+        import ipywidgets as widgets
+    except ImportError:
+        pass
+
+    # This class provides support for %%dve model description
+    @magics_class
+    class EditDVE(Magics):
+
+        @line_cell_magic
+        def dve(self, line, cell=None):
+            try:
+                # DiViNe prefers when files are in the current directory
+                # so write cell into local file
+                t = tempfile.NamedTemporaryFile(dir=os.getcwd())
+                filename = t.name + '.dve'
+                f = open(filename,"w")
+                f.write(cell)
+                f.close()
+
+                # Then compile and unlink temporary files
+                import subprocess
+                out=""
+                self.shell.user_ns[line] = None
+                out = subprocess.check_call(['divine', 'compile',
+                                       '--ltsmin', filename])
+                os.unlink(filename)
+                os.unlink(filename + '.cpp')
+                self.shell.user_ns[line] = load(filename + '2C')
+                os.unlink(filename + '2C')
+            except Exception as error:
+                try:
+                    os.unlink(filename)
+                    os.unlink(filename + '.cpp')
+                finally:
+                    if out != "":
+                        raise RuntimeError(out) from error
+                    raise error
+
+        @line_cell_magic
+        def require(self, line, cell=None):
+            if line != "divine":
+                print ("Unknown" + line, file=sys.stderr)
+                sys.exit(77)
+            if cell != None:
+                print ("No support for Cell magic command")
+                sys.exit(77)
+            if shutil.which("divine") == None:
+                print ("divine not available", file=sys.stderr)
+                sys.exit(77)
+            import subprocess
+            out = subprocess.check_output(['divine', 'compile',
+                                           '--help'], stderr=subprocess.STDOUT)
+            if b'LTSmin' not in out:
+                print ("divine available but no support for LTSmin",
+		       file=sys.stderr)
+                sys.exit(77)
+
+    ip = get_ipython()
+    ip.register_magics(EditDVE)
+
+except (ImportError, NameError):
+    pass
 %}
diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb
index a149b8134..59e73cc9a 100644
--- a/tests/python/ltsmin.ipynb
+++ b/tests/python/ltsmin.ipynb
@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.5.1"
   },
   "name": ""
  },
@@ -71,6 +71,27 @@
      "outputs": [],
      "prompt_number": 2
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The check of DiVinE and the setup of Spot can also be done with only:"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": true,
+     "input": [
+      "import spot\n",
+      "import spot.ltsmin\n",
+      "%require divine\n",
+      "spot.setup(max_states=10)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": 3
+    },
     {
      "cell_type": "markdown",
      "metadata": {},
@@ -87,7 +108,7 @@
      "language": "python",
      "metadata": {},
      "outputs": [],
-     "prompt_number": 3
+     "prompt_number": 4
     },
     {
      "cell_type": "code",
@@ -126,7 +147,7 @@
        ]
       }
      ],
-     "prompt_number": 4
+     "prompt_number": 5
     },
     {
      "cell_type": "markdown",
@@ -150,7 +171,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 5,
+       "prompt_number": 6,
        "text": [
         "ltsmin model with the following variables:\n",
         "  a: int\n",
@@ -160,7 +181,69 @@
        ]
       }
      ],
-     "prompt_number": 5
+     "prompt_number": 6
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "You can also directly load the model into variable m1 by using %dve command"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": true,
+     "input": [
+      "%%dve m1\n",
+      "int a = 0, b = 0;\n",
+      "\n",
+      "process P {\n",
+      " state x;\n",
+      " init x;\n",
+      "\n",
+      " trans\n",
+      "   x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
+      "   x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
+      "}\n",
+      "\n",
+      "process Q {\n",
+      "  state wait, work;\n",
+      "  init wait;\n",
+      "  trans\n",
+      "    wait -> work { guard b > 1; },\n",
+      "    work -> wait { guard a > 1; };\n",
+      "}\n",
+      "\n",
+      "system async;"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": 7
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "m1"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 8,
+       "text": [
+        "ltsmin model with the following variables:\n",
+        "  a: int\n",
+        "  b: int\n",
+        "  P: ['x']\n",
+        "  Q: ['wait', 'work']"
+       ]
+      }
+     ],
+     "prompt_number": 8
     },
     {
      "cell_type": "code",
@@ -174,7 +257,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 6,
+       "prompt_number": 9,
        "text": [
         "[('state_size', 4),\n",
         " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
@@ -182,855 +265,14 @@
        ]
       }
      ],
-     "prompt_number": 6
-    },
-    {
-     "cell_type": "code",
-     "collapsed": false,
-     "input": [
-      "k = m.kripke([\"a<1\", \"b>2\"])\n",
-      "k"
-     ],
-     "language": "python",
-     "metadata": {},
-     "outputs": [
-      {
-       "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 7,
-       "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=\"734pt\" height=\"218pt\"\n",
-        " viewBox=\"0.00 0.00 734.00 217.81\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.648748 0.648748) rotate(0) translate(4 331.74)\">\n",
-        "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-331.74 1127.41,-331.74 1127.41,4 -4,4\"/>\n",
-        "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"150.137\" cy=\"-154.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"150.137\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"150.137\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</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.10737,-154.87C2.31861,-154.87 13.6687,-154.87 29.5939,-154.87\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"36.6828,-154.87 29.6829,-158.02 33.1828,-154.87 29.6828,-154.87 29.6828,-154.87 29.6828,-154.87 33.1828,-154.87 29.6828,-151.72 36.6828,-154.87 36.6828,-154.87\"/>\n",
-        "</g>\n",
-        "<!-- 1 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"415.24\" cy=\"-190.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-194.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-179.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M248.733,-168.224C268.01,-170.862 288.33,-173.642 307.88,-176.317\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"315.044,-177.297 307.682,-179.469 311.577,-176.823 308.109,-176.348 308.109,-176.348 308.109,-176.348 311.577,-176.823 308.536,-173.227 315.044,-177.297 315.044,-177.297\"/>\n",
-        "</g>\n",
-        "<!-- 2 -->\n",
-        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"415.24\" cy=\"-118.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-122.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-107.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M248.733,-141.516C268.617,-138.795 289.613,-135.923 309.727,-133.17\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"316.802,-132.202 310.293,-136.272 313.334,-132.677 309.866,-133.151 309.866,-133.151 309.866,-133.151 313.334,-132.677 309.439,-130.031 316.802,-132.202 316.802,-132.202\"/>\n",
-        "</g>\n",
-        "<!-- 3 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-226.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-230.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-215.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;3 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M515.641,-204.326C535.172,-206.97 555.737,-209.754 575.495,-212.429\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"582.447,-213.37 575.088,-215.553 578.979,-212.901 575.511,-212.431 575.511,-212.431 575.511,-212.431 578.979,-212.901 575.933,-209.31 582.447,-213.37 582.447,-213.37\"/>\n",
-        "</g>\n",
-        "<!-- 4 -->\n",
-        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-154.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;4 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M515.641,-177.414C535.172,-174.77 555.737,-171.986 575.495,-169.311\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"582.447,-168.37 575.933,-172.431 578.979,-168.84 575.511,-169.309 575.511,-169.309 575.511,-169.309 578.979,-168.84 575.088,-166.188 582.447,-168.37 582.447,-168.37\"/>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;4 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M514.13,-132.122C534.134,-134.83 555.279,-137.692 575.57,-140.439\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"582.708,-141.405 575.349,-143.588 579.24,-140.936 575.772,-140.466 575.772,-140.466 575.772,-140.466 579.24,-140.936 576.194,-137.345 582.708,-141.405 582.708,-141.405\"/>\n",
-        "</g>\n",
-        "<!-- 5 -->\n",
-        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-82.8701\" rx=\"113.274\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;5 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M514.13,-105.618C534.753,-102.826 556.589,-99.8704 577.453,-97.0461\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"584.488,-96.0937 577.974,-100.154 581.019,-96.5633 577.551,-97.0329 577.551,-97.0329 577.551,-97.0329 581.019,-96.5633 577.128,-93.9113 584.488,-96.0937 584.488,-96.0937\"/>\n",
-        "</g>\n",
-        "<!-- 6 -->\n",
-        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-282.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-286.67\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-271.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;6 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M769.229,-244.974C797.049,-250.896 828.052,-257.494 856.29,-263.505\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"863.407,-265.019 855.904,-266.643 859.983,-264.291 856.56,-263.562 856.56,-263.562 856.56,-263.562 859.983,-264.291 857.216,-260.481 863.407,-265.019 863.407,-265.019\"/>\n",
-        "</g>\n",
-        "<!-- 7 -->\n",
-        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-210.87\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-214.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;7 -->\n",
-        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M795.75,-220.085C819.635,-218.632 844.42,-217.125 866.855,-215.76\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"874.053,-215.323 867.257,-218.892 870.559,-215.535 867.066,-215.748 867.066,-215.748 867.066,-215.748 870.559,-215.535 866.874,-212.604 874.053,-215.323 874.053,-215.323\"/>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;7 -->\n",
-        "<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M769.229,-172.974C803.85,-180.343 843.401,-188.761 876.419,-195.789\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"883.361,-197.267 875.859,-198.89 879.938,-196.538 876.515,-195.809 876.515,-195.809 876.515,-195.809 879.938,-196.538 877.17,-192.728 883.361,-197.267 883.361,-197.267\"/>\n",
-        "</g>\n",
-        "<!-- 8 -->\n",
-        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-138.87\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-142.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-127.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;8 -->\n",
-        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M795.75,-148.085C819.635,-146.632 844.42,-145.125 866.855,-143.76\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"874.053,-143.323 867.257,-146.892 870.559,-143.535 867.066,-143.748 867.066,-143.748 867.066,-143.748 870.559,-143.535 866.874,-140.604 874.053,-143.323 874.053,-143.323\"/>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;8 -->\n",
-        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M768.141,-100.743C802.961,-108.154 842.92,-116.659 876.251,-123.753\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"883.258,-125.245 875.756,-126.868 879.835,-124.516 876.411,-123.787 876.411,-123.787 876.411,-123.787 879.835,-124.516 877.067,-120.706 883.258,-125.245 883.258,-125.245\"/>\n",
-        "</g>\n",
-        "<!-- u5 -->\n",
-        "<g id=\"node11\" class=\"node\"><title>u5</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"961.273,-94.3701 935.273,-94.3701 935.273,-71.3701 961.273,-71.3701 961.273,-94.3701\"/>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;u5 -->\n",
-        "<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;u5</title>\n",
-        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M796.513,-82.8701C846.303,-82.8701 899.844,-82.8701 927.777,-82.8701\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"934.951,-82.8701 927.951,-86.0202 931.451,-82.8701 927.951,-82.8702 927.951,-82.8702 927.951,-82.8702 931.451,-82.8701 927.951,-79.7202 934.951,-82.8701 934.951,-82.8701\"/>\n",
-        "</g>\n",
-        "<!-- 9 -->\n",
-        "<g id=\"node12\" class=\"node\"><title>9</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-26.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n",
-        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;9 -->\n",
-        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M768.141,-64.9973C802.961,-57.5862 842.92,-49.081 876.251,-41.9869\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"883.258,-40.4954 877.067,-45.0337 879.835,-41.224 876.411,-41.9527 876.411,-41.9527 876.411,-41.9527 879.835,-41.224 875.756,-38.8717 883.258,-40.4954 883.258,-40.4954\"/>\n",
-        "</g>\n",
-        "<!-- 6&#45;&gt;6 -->\n",
-        "<g id=\"edge15\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M918.017,-309.141C916.672,-319.298 926.758,-327.74 948.273,-327.74 964.41,-327.74 974.117,-322.991 977.395,-316.332\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"978.53,-309.141 980.55,-316.546 977.984,-312.598 977.439,-316.055 977.439,-316.055 977.439,-316.055 977.984,-312.598 974.327,-315.564 978.53,-309.141 978.53,-309.141\"/>\n",
-        "</g>\n",
-        "<!-- u7 -->\n",
-        "<g id=\"node13\" class=\"node\"><title>u7</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-222.37 1097.41,-222.37 1097.41,-199.37 1123.41,-199.37 1123.41,-222.37\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-207.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;u7 -->\n",
-        "<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-210.87C1047.98,-210.87 1073.49,-210.87 1090.27,-210.87\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-210.87 1090.33,-214.02 1093.83,-210.87 1090.33,-210.87 1090.33,-210.87 1090.33,-210.87 1093.83,-210.87 1090.33,-207.72 1097.33,-210.87 1097.33,-210.87\"/>\n",
-        "</g>\n",
-        "<!-- u8 -->\n",
-        "<g id=\"node14\" class=\"node\"><title>u8</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-150.37 1097.41,-150.37 1097.41,-127.37 1123.41,-127.37 1123.41,-150.37\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-135.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;u8 -->\n",
-        "<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;u8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-138.87C1047.98,-138.87 1073.49,-138.87 1090.27,-138.87\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-138.87 1090.33,-142.02 1093.83,-138.87 1090.33,-138.87 1090.33,-138.87 1090.33,-138.87 1093.83,-138.87 1090.33,-135.72 1097.33,-138.87 1097.33,-138.87\"/>\n",
-        "</g>\n",
-        "<!-- u9 -->\n",
-        "<g id=\"node15\" class=\"node\"><title>u9</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-38.3701 1097.41,-38.3701 1097.41,-15.3701 1123.41,-15.3701 1123.41,-38.3701\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
-        "</g>\n",
-        "<!-- 9&#45;&gt;u9 -->\n",
-        "<g id=\"edge18\" class=\"edge\"><title>9&#45;&gt;u9</title>\n",
-        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-26.8701C1047.98,-26.8701 1073.49,-26.8701 1090.27,-26.8701\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-26.8701 1090.33,-30.0202 1093.83,-26.8701 1090.33,-26.8702 1090.33,-26.8702 1090.33,-26.8702 1093.83,-26.8701 1090.33,-23.7202 1097.33,-26.8701 1097.33,-26.8701\"/>\n",
-        "</g>\n",
-        "</g>\n",
-        "</svg>\n"
-       ],
-       "text": [
-        "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f426c309690> >"
-       ]
-      }
-     ],
-     "prompt_number": 7
-    },
-    {
-     "cell_type": "code",
-     "collapsed": false,
-     "input": [
-      "k.show('.<15')"
-     ],
-     "language": "python",
-     "metadata": {},
-     "outputs": [
-      {
-       "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 8,
-       "svg": [
-        "<svg height=\"200pt\" viewBox=\"0.00 0.00 734.00 199.71\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.524532 0.524532) rotate(0) translate(4 376.74)\">\n",
-        "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-376.74 1395.34,-376.74 1395.34,4 -4,4\" stroke=\"none\"/>\n",
-        "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"150.137\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-187.67\">a=0, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-172.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.10737,-183.87C2.31861,-183.87 13.6687,-183.87 29.5939,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"36.6828,-183.87 29.6829,-187.02 33.1828,-183.87 29.6828,-183.87 29.6828,-183.87 29.6828,-183.87 33.1828,-183.87 29.6828,-180.72 36.6828,-183.87 36.6828,-183.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 1 -->\n",
-        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-219.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-223.67\">a=1, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-208.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M248.733,-197.224C268.01,-199.862 288.33,-202.642 307.88,-205.317\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"315.044,-206.297 307.682,-208.469 311.577,-205.823 308.109,-205.348 308.109,-205.348 308.109,-205.348 311.577,-205.823 308.536,-202.227 315.044,-206.297 315.044,-206.297\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 2 -->\n",
-        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-147.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-151.67\">a=0, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-136.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M248.733,-170.516C268.617,-167.795 289.613,-164.923 309.727,-162.17\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"316.802,-161.202 310.293,-165.272 313.334,-161.677 309.866,-162.151 309.866,-162.151 309.866,-162.151 313.334,-161.677 309.439,-159.031 316.802,-161.202 316.802,-161.202\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 3 -->\n",
-        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-259.67\">a=2, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-244.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
-        "<path d=\"M515.641,-233.326C535.172,-235.97 555.737,-238.754 575.495,-241.429\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-242.37 575.088,-244.553 578.979,-241.901 575.511,-241.431 575.511,-241.431 575.511,-241.431 578.979,-241.901 575.933,-238.31 582.447,-242.37 582.447,-242.37\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 4 -->\n",
-        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-187.67\">a=1, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-172.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
-        "<path d=\"M515.641,-206.414C535.172,-203.77 555.737,-200.986 575.495,-198.311\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-197.37 575.933,-201.431 578.979,-197.84 575.511,-198.309 575.511,-198.309 575.511,-198.309 578.979,-197.84 575.088,-195.188 582.447,-197.37 582.447,-197.37\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
-        "<path d=\"M514.13,-161.122C534.134,-163.83 555.279,-166.692 575.57,-169.439\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.708,-170.405 575.349,-172.588 579.24,-169.936 575.772,-169.466 575.772,-169.466 575.772,-169.466 579.24,-169.936 576.194,-166.345 582.708,-170.405 582.708,-170.405\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 5 -->\n",
-        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-115.67\">a=0, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-100.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
-        "<path d=\"M514.13,-134.618C534.753,-131.826 556.589,-128.87 577.453,-126.046\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"584.488,-125.094 577.974,-129.154 581.019,-125.563 577.551,-126.033 577.551,-126.033 577.551,-126.033 581.019,-125.563 577.128,-122.911 584.488,-125.094 584.488,-125.094\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 6 -->\n",
-        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-331.67\">a=3, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-316.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
-        "<path d=\"M759.31,-276.214C793.436,-285.453 833.873,-296.402 868.718,-305.836\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"875.609,-307.701 868.029,-308.912 872.23,-306.787 868.852,-305.872 868.852,-305.872 868.852,-305.872 872.23,-306.787 869.675,-302.831 875.609,-307.701 875.609,-307.701\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 7 -->\n",
-        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-259.67\">a=2, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-244.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
-        "<path d=\"M799.265,-255.87C808.661,-255.87 818.179,-255.87 827.625,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"834.832,-255.87 827.832,-259.02 831.332,-255.87 827.832,-255.87 827.832,-255.87 827.832,-255.87 831.332,-255.87 827.832,-252.72 834.832,-255.87 834.832,-255.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
-        "<path d=\"M759.31,-204.214C793.148,-213.375 833.191,-224.217 867.834,-233.596\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.688,-235.452 867.108,-236.663 871.309,-234.537 867.931,-233.622 867.931,-233.622 867.931,-233.622 871.309,-234.537 868.754,-230.582 874.688,-235.452 874.688,-235.452\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 8 -->\n",
-        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-187.67\">a=1, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-172.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
-        "<path d=\"M799.265,-183.87C808.661,-183.87 818.179,-183.87 827.625,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"834.832,-183.87 827.832,-187.02 831.332,-183.87 827.832,-183.87 827.832,-183.87 827.832,-183.87 831.332,-183.87 827.832,-180.72 834.832,-183.87 834.832,-183.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
-        "<path d=\"M758.601,-132.022C792.597,-141.226 832.972,-152.158 867.864,-161.605\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.766,-163.473 867.186,-164.684 871.388,-162.558 868.009,-161.644 868.009,-161.644 868.009,-161.644 871.388,-162.558 868.833,-158.603 874.766,-163.473 874.766,-163.473\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 9 -->\n",
-        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-15.6701\">...</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;9 -->\n",
-        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
-        "<path d=\"M751.62,-90.3111C793.454,-76.9397 846.823,-59.8814 887.681,-46.8216\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"894.385,-44.6789 888.676,-49.8107 891.051,-45.7446 887.717,-46.8102 887.717,-46.8102 887.717,-46.8102 891.051,-45.7446 886.758,-43.8097 894.385,-44.6789 894.385,-44.6789\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 10 -->\n",
-        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-115.67\">a=0, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-100.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;10 -->\n",
-        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
-        "<path d=\"M796.564,-111.87C807.833,-111.87 819.305,-111.87 830.644,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"837.684,-111.87 830.684,-115.02 834.184,-111.87 830.684,-111.87 830.684,-111.87 830.684,-111.87 834.184,-111.87 830.684,-108.72 837.684,-111.87 837.684,-111.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 6&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
-        "<path d=\"M902.375,-352.332C897.735,-363.275 913.977,-372.74 951.102,-372.74 979.526,-372.74 995.708,-367.192 999.65,-359.68\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"999.828,-352.332 1002.81,-359.406 999.743,-355.831 999.658,-359.33 999.658,-359.33 999.658,-359.33 999.743,-355.831 996.509,-359.253 999.828,-352.332 999.828,-352.332\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 11 -->\n",
-        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
-        "<ellipse cx=\"1216.2\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-331.67\">a=3, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-316.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;11 -->\n",
-        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
-        "<path d=\"M1026.79,-276.31C1060.41,-285.508 1100.15,-296.385 1134.45,-305.772\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1141.24,-307.628 1133.65,-308.819 1137.86,-306.705 1134.49,-305.781 1134.49,-305.781 1134.49,-305.781 1137.86,-306.705 1135.32,-302.742 1141.24,-307.628 1141.24,-307.628\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 12 -->\n",
-        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
-        "<ellipse cx=\"1216.2\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-259.67\">a=2, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-244.67\">...</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;12 -->\n",
-        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
-        "<path d=\"M1067.12,-255.87C1089.61,-255.87 1112.75,-255.87 1133.86,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1140.94,-255.87 1133.94,-259.02 1137.44,-255.87 1133.94,-255.87 1133.94,-255.87 1133.94,-255.87 1137.44,-255.87 1133.94,-252.72 1140.94,-255.87 1140.94,-255.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;12 -->\n",
-        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
-        "<path d=\"M1026.79,-204.31C1065.41,-214.877 1112.12,-227.66 1149.37,-237.854\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1156.21,-239.726 1148.63,-240.916 1152.83,-238.802 1149.46,-237.878 1149.46,-237.878 1149.46,-237.878 1152.83,-238.802 1150.29,-234.84 1156.21,-239.726 1156.21,-239.726\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 13 -->\n",
-        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
-        "<ellipse cx=\"1216.2\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-187.67\">a=1, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-172.67\">...</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;13 -->\n",
-        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
-        "<path d=\"M1067.12,-183.87C1089.61,-183.87 1112.75,-183.87 1133.86,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1140.94,-183.87 1133.94,-187.02 1137.44,-183.87 1133.94,-183.87 1133.94,-183.87 1133.94,-183.87 1137.44,-183.87 1133.94,-180.72 1140.94,-183.87 1140.94,-183.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 14 -->\n",
-        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
-        "<ellipse cx=\"1216.2\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-115.67\">a=1, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-100.67\">...</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;14 -->\n",
-        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
-        "<path d=\"M1026.79,-163.43C1065.41,-152.863 1112.12,-140.08 1149.37,-129.886\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1156.21,-128.014 1150.29,-132.9 1152.83,-128.938 1149.46,-129.862 1149.46,-129.862 1149.46,-129.862 1152.83,-128.938 1148.63,-126.824 1156.21,-128.014 1156.21,-128.014\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- u9 -->\n",
-        "<g class=\"node\" id=\"node17\"><title>u9</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1229.2,-26.3701 1203.2,-26.3701 1203.2,-3.37006 1229.2,-3.37006 1229.2,-26.3701\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-11.1701\">...</text>\n",
-        "</g>\n",
-        "<!-- 9&#45;&gt;u9 -->\n",
-        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;u9</title>\n",
-        "<path d=\"M1025.74,-23.5114C1083.69,-20.8685 1160.36,-17.3713 1195.76,-15.7567\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1203.06,-15.4238 1196.21,-18.8896 1199.57,-15.5833 1196.07,-15.7428 1196.07,-15.7428 1196.07,-15.7428 1199.57,-15.5833 1195.93,-12.5961 1203.06,-15.4238 1203.06,-15.4238\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 10&#45;&gt;14 -->\n",
-        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;14</title>\n",
-        "<path d=\"M1064.44,-111.87C1087.76,-111.87 1111.9,-111.87 1133.84,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1140.89,-111.87 1133.89,-115.02 1137.39,-111.87 1133.89,-111.87 1133.89,-111.87 1133.89,-111.87 1137.39,-111.87 1133.89,-108.72 1140.89,-111.87 1140.89,-111.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- u10 -->\n",
-        "<g class=\"node\" id=\"node18\"><title>u10</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1229.2,-67.3701 1203.2,-67.3701 1203.2,-44.3701 1229.2,-44.3701 1229.2,-67.3701\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2\" y=\"-52.1701\">...</text>\n",
-        "</g>\n",
-        "<!-- 10&#45;&gt;u10 -->\n",
-        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;u10</title>\n",
-        "<path d=\"M1029.87,-92.4189C1053.33,-86.7964 1079.19,-80.841 1103.07,-75.8701 1135.59,-69.0971 1173.73,-62.6 1196.1,-58.9338\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1203.05,-57.8027 1196.64,-62.0361 1199.59,-58.3648 1196.14,-58.927 1196.14,-58.927 1196.14,-58.927 1199.59,-58.3648 1195.63,-55.8179 1203.05,-57.8027 1203.05,-57.8027\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 11&#45;&gt;11 -->\n",
-        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
-        "<path d=\"M1185.95,-354.141C1184.6,-364.298 1194.69,-372.74 1216.2,-372.74 1232.34,-372.74 1242.05,-367.991 1245.33,-361.332\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1246.46,-354.141 1248.48,-361.546 1245.92,-357.598 1245.37,-361.055 1245.37,-361.055 1245.37,-361.055 1245.92,-357.598 1242.26,-360.564 1246.46,-354.141 1246.46,-354.141\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- u12 -->\n",
-        "<g class=\"node\" id=\"node19\"><title>u12</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1391.34,-267.37 1365.34,-267.37 1365.34,-244.37 1391.34,-244.37 1391.34,-267.37\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.34\" y=\"-252.17\">...</text>\n",
-        "</g>\n",
-        "<!-- 12&#45;&gt;u12 -->\n",
-        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;u12</title>\n",
-        "<path d=\"M1291.18,-255.87C1315.91,-255.87 1341.42,-255.87 1358.2,-255.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1365.26,-255.87 1358.26,-259.02 1361.76,-255.87 1358.26,-255.87 1358.26,-255.87 1358.26,-255.87 1361.76,-255.87 1358.26,-252.72 1365.26,-255.87 1365.26,-255.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- u13 -->\n",
-        "<g class=\"node\" id=\"node20\"><title>u13</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1391.34,-195.37 1365.34,-195.37 1365.34,-172.37 1391.34,-172.37 1391.34,-195.37\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.34\" y=\"-180.17\">...</text>\n",
-        "</g>\n",
-        "<!-- 13&#45;&gt;u13 -->\n",
-        "<g class=\"edge\" id=\"edge26\"><title>13-&gt;u13</title>\n",
-        "<path d=\"M1291.18,-183.87C1315.91,-183.87 1341.42,-183.87 1358.2,-183.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1365.26,-183.87 1358.26,-187.02 1361.76,-183.87 1358.26,-183.87 1358.26,-183.87 1358.26,-183.87 1361.76,-183.87 1358.26,-180.72 1365.26,-183.87 1365.26,-183.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- u14 -->\n",
-        "<g class=\"node\" id=\"node21\"><title>u14</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1391.34,-123.37 1365.34,-123.37 1365.34,-100.37 1391.34,-100.37 1391.34,-123.37\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.34\" y=\"-108.17\">...</text>\n",
-        "</g>\n",
-        "<!-- 14&#45;&gt;u14 -->\n",
-        "<g class=\"edge\" id=\"edge27\"><title>14-&gt;u14</title>\n",
-        "<path d=\"M1291.18,-111.87C1315.91,-111.87 1341.42,-111.87 1358.2,-111.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1365.26,-111.87 1358.26,-115.02 1361.76,-111.87 1358.26,-111.87 1358.26,-111.87 1358.26,-111.87 1361.76,-111.87 1358.26,-108.72 1365.26,-111.87 1365.26,-111.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "</g>\n",
-        "</svg>"
-       ],
-       "text": [
-        "<IPython.core.display.SVG object>"
-       ]
-      }
-     ],
-     "prompt_number": 8
-    },
-    {
-     "cell_type": "code",
-     "collapsed": false,
-     "input": [
-      "k.show('.<0')  # unlimited output"
-     ],
-     "language": "python",
-     "metadata": {},
-     "outputs": [
-      {
-       "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 9,
-       "svg": [
-        "<svg height=\"151pt\" viewBox=\"0.00 0.00 734.00 150.69\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.390662 0.390662) rotate(0) translate(4 381.74)\">\n",
-        "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-381.74 1874.86,-381.74 1874.86,4 -4,4\" stroke=\"none\"/>\n",
-        "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"150.137\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-192.67\">a=0, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-177.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.10737,-188.87C2.31861,-188.87 13.6687,-188.87 29.5939,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"36.6828,-188.87 29.6829,-192.02 33.1828,-188.87 29.6828,-188.87 29.6828,-188.87 29.6828,-188.87 33.1828,-188.87 29.6828,-185.72 36.6828,-188.87 36.6828,-188.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 1 -->\n",
-        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-224.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-228.67\">a=1, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-213.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M248.733,-202.224C268.01,-204.862 288.33,-207.642 307.88,-210.317\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"315.044,-211.297 307.682,-213.469 311.577,-210.823 308.109,-210.348 308.109,-210.348 308.109,-210.348 311.577,-210.823 308.536,-207.227 315.044,-211.297 315.044,-211.297\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 2 -->\n",
-        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-152.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-156.67\">a=0, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-141.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M248.733,-175.516C268.617,-172.795 289.613,-169.923 309.727,-167.17\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"316.802,-166.202 310.293,-170.272 313.334,-166.677 309.866,-167.151 309.866,-167.151 309.866,-167.151 313.334,-166.677 309.439,-164.031 316.802,-166.202 316.802,-166.202\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 3 -->\n",
-        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-264.67\">a=2, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
-        "<path d=\"M515.641,-238.326C535.172,-240.97 555.737,-243.754 575.495,-246.429\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-247.37 575.088,-249.553 578.979,-246.901 575.511,-246.431 575.511,-246.431 575.511,-246.431 578.979,-246.901 575.933,-243.31 582.447,-247.37 582.447,-247.37\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 4 -->\n",
-        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-192.67\">a=1, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
-        "<path d=\"M515.641,-211.414C535.172,-208.77 555.737,-205.986 575.495,-203.311\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-202.37 575.933,-206.431 578.979,-202.84 575.511,-203.309 575.511,-203.309 575.511,-203.309 578.979,-202.84 575.088,-200.188 582.447,-202.37 582.447,-202.37\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
-        "<path d=\"M514.13,-166.122C534.134,-168.83 555.279,-171.692 575.57,-174.439\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.708,-175.405 575.349,-177.588 579.24,-174.936 575.772,-174.466 575.772,-174.466 575.772,-174.466 579.24,-174.936 576.194,-171.345 582.708,-175.405 582.708,-175.405\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 5 -->\n",
-        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-120.67\">a=0, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-105.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
-        "<path d=\"M514.13,-139.618C534.753,-136.826 556.589,-133.87 577.453,-131.046\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"584.488,-130.094 577.974,-134.154 581.019,-130.563 577.551,-131.033 577.551,-131.033 577.551,-131.033 581.019,-130.563 577.128,-127.911 584.488,-130.094 584.488,-130.094\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 6 -->\n",
-        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-336.67\">a=3, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
-        "<path d=\"M759.31,-281.214C793.436,-290.453 833.873,-301.402 868.718,-310.836\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"875.609,-312.701 868.029,-313.912 872.23,-311.787 868.852,-310.872 868.852,-310.872 868.852,-310.872 872.23,-311.787 869.675,-307.831 875.609,-312.701 875.609,-312.701\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 7 -->\n",
-        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-264.67\">a=2, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
-        "<path d=\"M799.265,-260.87C808.661,-260.87 818.179,-260.87 827.625,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"834.832,-260.87 827.832,-264.02 831.332,-260.87 827.832,-260.87 827.832,-260.87 827.832,-260.87 831.332,-260.87 827.832,-257.72 834.832,-260.87 834.832,-260.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
-        "<path d=\"M759.31,-209.214C793.148,-218.375 833.191,-229.217 867.834,-238.596\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.688,-240.452 867.108,-241.663 871.309,-239.537 867.931,-238.622 867.931,-238.622 867.931,-238.622 871.309,-239.537 868.754,-235.582 874.688,-240.452 874.688,-240.452\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 8 -->\n",
-        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-192.67\">a=1, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
-        "<path d=\"M799.265,-188.87C808.661,-188.87 818.179,-188.87 827.625,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"834.832,-188.87 827.832,-192.02 831.332,-188.87 827.832,-188.87 827.832,-188.87 827.832,-188.87 831.332,-188.87 827.832,-185.72 834.832,-188.87 834.832,-188.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
-        "<path d=\"M758.601,-137.022C792.597,-146.226 832.972,-157.158 867.864,-166.605\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.766,-168.473 867.186,-169.684 871.388,-167.558 868.009,-166.644 868.009,-166.644 868.009,-166.644 871.388,-167.558 868.833,-163.603 874.766,-168.473 874.766,-168.473\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 9 -->\n",
-        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-35.8701\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-39.6701\">a=0, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-24.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;9 -->\n",
-        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
-        "<path d=\"M753.694,-95.6941C790.782,-84.3974 836.471,-70.4808 874.448,-58.9136\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"881.445,-56.7822 875.667,-61.8352 878.097,-57.8021 874.749,-58.8219 874.749,-58.8219 874.749,-58.8219 878.097,-57.8021 873.831,-55.8086 881.445,-56.7822 881.445,-56.7822\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 10 -->\n",
-        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
-        "<ellipse cx=\"951.102\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-120.67\">a=0, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"951.102\" y=\"-105.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;10 -->\n",
-        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
-        "<path d=\"M796.564,-116.87C807.833,-116.87 819.305,-116.87 830.644,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"837.684,-116.87 830.684,-120.02 834.184,-116.87 830.684,-116.87 830.684,-116.87 830.684,-116.87 834.184,-116.87 830.684,-113.72 837.684,-116.87 837.684,-116.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 6&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
-        "<path d=\"M902.006,-357.332C897.33,-368.275 913.695,-377.74 951.102,-377.74 979.741,-377.74 996.046,-372.192 1000.02,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1000.2,-357.332 1003.18,-364.407 1000.11,-360.831 1000.03,-364.33 1000.03,-364.33 1000.03,-364.33 1000.11,-360.831 996.877,-364.253 1000.2,-357.332 1000.2,-357.332\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 11 -->\n",
-        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
-        "<ellipse cx=\"1219.03\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-336.67\">a=3, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;11 -->\n",
-        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
-        "<path d=\"M1027.24,-281.214C1061.37,-290.453 1101.8,-301.402 1136.65,-310.836\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1143.54,-312.701 1135.96,-313.912 1140.16,-311.787 1136.78,-310.872 1136.78,-310.872 1136.78,-310.872 1140.16,-311.787 1137.61,-307.831 1143.54,-312.701 1143.54,-312.701\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 12 -->\n",
-        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
-        "<ellipse cx=\"1219.03\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-264.67\">a=2, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;12 -->\n",
-        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
-        "<path d=\"M1067.2,-260.87C1076.59,-260.87 1086.11,-260.87 1095.56,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1102.76,-260.87 1095.76,-264.02 1099.26,-260.87 1095.76,-260.87 1095.76,-260.87 1095.76,-260.87 1099.26,-260.87 1095.76,-257.72 1102.76,-260.87 1102.76,-260.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;12 -->\n",
-        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
-        "<path d=\"M1027.24,-209.214C1061.08,-218.375 1101.12,-229.217 1135.77,-238.596\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1142.62,-240.452 1135.04,-241.663 1139.24,-239.537 1135.86,-238.622 1135.86,-238.622 1135.86,-238.622 1139.24,-239.537 1136.69,-235.582 1142.62,-240.452 1142.62,-240.452\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 13 -->\n",
-        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
-        "<ellipse cx=\"1219.03\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-192.67\">a=1, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;13 -->\n",
-        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
-        "<path d=\"M1067.2,-188.87C1077.58,-188.87 1088.1,-188.87 1098.52,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1105.71,-188.87 1098.71,-192.02 1102.21,-188.87 1098.71,-188.87 1098.71,-188.87 1098.71,-188.87 1102.21,-188.87 1098.71,-185.72 1105.71,-188.87 1105.71,-188.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 14 -->\n",
-        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
-        "<ellipse cx=\"1219.03\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-120.67\">a=1, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-105.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;14 -->\n",
-        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
-        "<path d=\"M1027.24,-168.526C1061.08,-159.365 1101.12,-148.523 1135.77,-139.144\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1142.62,-137.288 1136.69,-142.158 1139.24,-138.203 1135.86,-139.118 1135.86,-139.118 1135.86,-139.118 1139.24,-138.203 1135.04,-136.077 1142.62,-137.288 1142.62,-137.288\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 15 -->\n",
-        "<g class=\"node\" id=\"node17\"><title>15</title>\n",
-        "<ellipse cx=\"1219.03\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"107.46\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-30.6701\">a=0, b=3, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1219.03\" y=\"-15.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 9&#45;&gt;15 -->\n",
-        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;15</title>\n",
-        "<path d=\"M1060.65,-32.1964C1075.34,-31.6994 1090.44,-31.1884 1105.2,-30.6888\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1112.41,-30.4446 1105.52,-33.8297 1108.91,-30.5631 1105.42,-30.6815 1105.42,-30.6815 1105.42,-30.6815 1108.91,-30.5631 1105.31,-27.5333 1112.41,-30.4446 1112.41,-30.4446\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 10&#45;&gt;14 -->\n",
-        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;14</title>\n",
-        "<path d=\"M1064.49,-116.87C1074.86,-116.87 1085.4,-116.87 1095.85,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1103.06,-116.87 1096.06,-120.02 1099.56,-116.87 1096.06,-116.87 1096.06,-116.87 1096.06,-116.87 1099.56,-116.87 1096.06,-113.72 1103.06,-116.87 1103.06,-116.87\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 10&#45;&gt;15 -->\n",
-        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;15</title>\n",
-        "<path d=\"M1016.82,-94.9687C1056.43,-81.5624 1107.13,-64.4034 1147.73,-50.6639\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1154.41,-48.4023 1148.79,-53.6301 1151.09,-49.5243 1147.78,-50.6463 1147.78,-50.6463 1147.78,-50.6463 1151.09,-49.5243 1146.77,-47.6626 1154.41,-48.4023 1154.41,-48.4023\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 11&#45;&gt;11 -->\n",
-        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
-        "<path d=\"M1169.94,-357.332C1165.26,-368.275 1181.63,-377.74 1219.03,-377.74 1247.67,-377.74 1263.98,-372.192 1267.95,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1268.13,-357.332 1271.11,-364.407 1268.04,-360.831 1267.96,-364.33 1267.96,-364.33 1267.96,-364.33 1268.04,-360.831 1264.81,-364.253 1268.13,-357.332 1268.13,-357.332\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 16 -->\n",
-        "<g class=\"node\" id=\"node18\"><title>16</title>\n",
-        "<ellipse cx=\"1486.96\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-336.67\">a=3, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 12&#45;&gt;16 -->\n",
-        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;16</title>\n",
-        "<path d=\"M1295.17,-281.214C1329.01,-290.375 1369.05,-301.217 1403.7,-310.596\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1410.55,-312.452 1402.97,-313.663 1407.17,-311.537 1403.79,-310.622 1403.79,-310.622 1403.79,-310.622 1407.17,-311.537 1404.62,-307.582 1410.55,-312.452 1410.55,-312.452\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 17 -->\n",
-        "<g class=\"node\" id=\"node19\"><title>17</title>\n",
-        "<ellipse cx=\"1486.96\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-192.67\">a=2, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 12&#45;&gt;17 -->\n",
-        "<g class=\"edge\" id=\"edge26\"><title>12-&gt;17</title>\n",
-        "<path d=\"M1295.17,-240.526C1329.3,-231.287 1369.74,-220.339 1404.58,-210.905\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1411.47,-209.039 1405.54,-213.909 1408.09,-209.954 1404.71,-210.868 1404.71,-210.868 1404.71,-210.868 1408.09,-209.954 1403.89,-207.828 1411.47,-209.039 1411.47,-209.039\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 18 -->\n",
-        "<g class=\"node\" id=\"node20\"><title>18</title>\n",
-        "<ellipse cx=\"1486.96\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-264.67\">a=2, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 12&#45;&gt;18 -->\n",
-        "<g class=\"edge\" id=\"edge27\"><title>12-&gt;18</title>\n",
-        "<path d=\"M1331.66,-254.198C1343.54,-254.111 1355.65,-254.097 1367.61,-254.156\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1374.63,-254.2 1367.61,-257.306 1371.13,-254.178 1367.63,-254.156 1367.63,-254.156 1367.63,-254.156 1371.13,-254.178 1367.65,-251.006 1374.63,-254.2 1374.63,-254.2\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 19 -->\n",
-        "<g class=\"node\" id=\"node21\"><title>19</title>\n",
-        "<ellipse cx=\"1486.96\" cy=\"-98.8701\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-102.67\">a=1, b=3, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1486.96\" y=\"-87.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 13&#45;&gt;19 -->\n",
-        "<g class=\"edge\" id=\"edge28\"><title>13-&gt;19</title>\n",
-        "<path d=\"M1289.18,-167.711C1304.31,-162.942 1320.22,-157.823 1335,-152.87 1362.37,-143.692 1392.35,-133.085 1418.33,-123.715\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1425.19,-121.235 1419.68,-126.577 1421.9,-122.425 1418.61,-123.614 1418.61,-123.614 1418.61,-123.614 1421.9,-122.425 1417.54,-120.652 1425.19,-121.235 1425.19,-121.235\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 14&#45;&gt;18 -->\n",
-        "<g class=\"edge\" id=\"edge29\"><title>14-&gt;18</title>\n",
-        "<path d=\"M1305.45,-134.936C1316.12,-139.606 1326.32,-145.481 1335,-152.87 1362.24,-176.063 1343.76,-201.677 1371,-224.87 1377.91,-230.758 1385.79,-235.685 1394.11,-239.807\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1400.54,-242.804 1392.87,-242.704 1397.37,-241.326 1394.2,-239.848 1394.2,-239.848 1394.2,-239.848 1397.37,-241.326 1395.53,-236.993 1400.54,-242.804 1400.54,-242.804\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 14&#45;&gt;19 -->\n",
-        "<g class=\"edge\" id=\"edge30\"><title>14-&gt;19</title>\n",
-        "<path d=\"M1330.5,-109.393C1344.6,-108.439 1359.04,-107.461 1373.17,-106.504\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1380.53,-106.006 1373.76,-109.622 1377.04,-106.243 1373.55,-106.479 1373.55,-106.479 1373.55,-106.479 1377.04,-106.243 1373.34,-103.336 1380.53,-106.006 1380.53,-106.006\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 15&#45;&gt;15 -->\n",
-        "<g class=\"edge\" id=\"edge31\"><title>15-&gt;15</title>\n",
-        "<path d=\"M1170.14,-50.8749C1164.81,-62.0106 1181.11,-71.7401 1219.03,-71.7401 1248.66,-71.7401 1265.09,-65.8017 1268.32,-57.8937\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1267.92,-50.8749 1271.46,-57.6868 1268.12,-54.3693 1268.31,-57.8638 1268.31,-57.8638 1268.31,-57.8638 1268.12,-54.3693 1265.17,-58.0408 1267.92,-50.8749 1267.92,-50.8749\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 20 -->\n",
-        "<g class=\"node\" id=\"node22\"><title>20</title>\n",
-        "<ellipse cx=\"1754.89\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1754.89\" y=\"-336.67\">a=3, b=2, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1754.89\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 16&#45;&gt;20 -->\n",
-        "<g class=\"edge\" id=\"edge32\"><title>16-&gt;20</title>\n",
-        "<path d=\"M1599.59,-326.198C1611.47,-326.111 1623.58,-326.097 1635.54,-326.156\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1642.56,-326.2 1635.54,-329.306 1639.06,-326.178 1635.56,-326.156 1635.56,-326.156 1635.56,-326.156 1639.06,-326.178 1635.58,-323.006 1642.56,-326.2 1642.56,-326.2\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 21 -->\n",
-        "<g class=\"node\" id=\"node23\"><title>21</title>\n",
-        "<ellipse cx=\"1754.89\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1754.89\" y=\"-192.67\">a=2, b=3, Q=1</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1754.89\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 17&#45;&gt;21 -->\n",
-        "<g class=\"edge\" id=\"edge33\"><title>17-&gt;21</title>\n",
-        "<path d=\"M1596.9,-182.219C1610.45,-182.106 1624.36,-182.09 1638.02,-182.17\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1645.13,-182.22 1638.11,-185.32 1641.63,-182.196 1638.13,-182.171 1638.13,-182.171 1638.13,-182.171 1641.63,-182.196 1638.16,-179.021 1645.13,-182.22 1645.13,-182.22\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 18&#45;&gt;12 -->\n",
-        "<g class=\"edge\" id=\"edge36\"><title>18-&gt;12</title>\n",
-        "<path d=\"M1374.63,-267.54C1362.75,-267.629 1350.63,-267.644 1338.68,-267.585\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1331.66,-267.542 1338.67,-264.435 1335.16,-267.564 1338.66,-267.585 1338.66,-267.585 1338.66,-267.585 1335.16,-267.564 1338.64,-270.735 1331.66,-267.542 1331.66,-267.542\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 18&#45;&gt;20 -->\n",
-        "<g class=\"edge\" id=\"edge34\"><title>18-&gt;20</title>\n",
-        "<path d=\"M1563.1,-281.214C1596.94,-290.375 1636.98,-301.217 1671.63,-310.596\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1678.48,-312.452 1670.9,-313.663 1675.1,-311.537 1671.72,-310.622 1671.72,-310.622 1671.72,-310.622 1675.1,-311.537 1672.55,-307.582 1678.48,-312.452 1678.48,-312.452\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 18&#45;&gt;21 -->\n",
-        "<g class=\"edge\" id=\"edge35\"><title>18-&gt;21</title>\n",
-        "<path d=\"M1563.1,-240.526C1597.23,-231.287 1637.67,-220.339 1672.51,-210.905\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1679.4,-209.039 1673.47,-213.909 1676.02,-209.954 1672.64,-210.868 1672.64,-210.868 1672.64,-210.868 1676.02,-209.954 1671.82,-207.828 1679.4,-209.039 1679.4,-209.039\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 19&#45;&gt;19 -->\n",
-        "<g class=\"edge\" id=\"edge37\"><title>19-&gt;19</title>\n",
-        "<path d=\"M1437.87,-123.332C1433.19,-134.275 1449.56,-143.74 1486.96,-143.74 1515.6,-143.74 1531.91,-138.192 1535.88,-130.68\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1536.06,-123.332 1539.04,-130.407 1535.97,-126.831 1535.89,-130.33 1535.89,-130.33 1535.89,-130.33 1535.97,-126.831 1532.74,-130.253 1536.06,-123.332 1536.06,-123.332\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 20&#45;&gt;16 -->\n",
-        "<g class=\"edge\" id=\"edge38\"><title>20-&gt;16</title>\n",
-        "<path d=\"M1642.56,-339.54C1630.68,-339.629 1618.56,-339.644 1606.61,-339.585\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1599.59,-339.542 1606.61,-336.435 1603.09,-339.564 1606.59,-339.585 1606.59,-339.585 1606.59,-339.585 1603.09,-339.564 1606.57,-342.735 1599.59,-339.542 1599.59,-339.542\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "<!-- 21&#45;&gt;17 -->\n",
-        "<g class=\"edge\" id=\"edge39\"><title>21-&gt;17</title>\n",
-        "<path d=\"M1645.13,-195.52C1631.58,-195.633 1617.67,-195.65 1604.01,-195.571\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"1596.9,-195.521 1603.92,-192.421 1600.4,-195.546 1603.9,-195.571 1603.9,-195.571 1603.9,-195.571 1600.4,-195.546 1603.87,-198.72 1596.9,-195.521 1596.9,-195.521\" stroke=\"black\"/>\n",
-        "</g>\n",
-        "</g>\n",
-        "</svg>"
-       ],
-       "text": [
-        "<IPython.core.display.SVG object>"
-       ]
-      }
-     ],
      "prompt_number": 9
     },
     {
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "a = spot.translate('\"a<1\" U \"b>2\"'); a"
+      "k = m.kripke([\"a<1\", \"b>2\"])\n",
+      "k"
      ],
      "language": "python",
      "metadata": {},
@@ -1046,11 +288,852 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"198pt\" height=\"85pt\"\n",
-        " viewBox=\"0.00 0.00 198.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"734pt\" height=\"222pt\"\n",
+        " viewBox=\"0.00 0.00 734.00 222.26\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.661987 0.661987) rotate(0) translate(4 331.74)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-331.74 1104.78,-331.74 1104.78,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"147.309\" cy=\"-154.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"147.309\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"147.309\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</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.10532,-154.87C2.30847,-154.87 13.7102,-154.87 29.6433,-154.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"36.7326,-154.87 29.7326,-158.02 33.2326,-154.87 29.7326,-154.87 29.7326,-154.87 29.7326,-154.87 33.2326,-154.87 29.7326,-151.72 36.7326,-154.87 36.7326,-154.87\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"406.754\" cy=\"-190.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"406.754\" y=\"-194.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"406.754\" y=\"-179.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.441,-168.173C262.448,-170.831 282.507,-173.636 301.795,-176.333\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"308.862,-177.321 301.493,-179.471 305.396,-176.836 301.93,-176.352 301.93,-176.352 301.93,-176.352 305.396,-176.836 302.366,-173.232 308.862,-177.321 308.862,-177.321\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"406.754\" cy=\"-118.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"406.754\" y=\"-122.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"406.754\" y=\"-107.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.441,-141.567C263.044,-138.826 283.766,-135.928 303.606,-133.154\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"310.584,-132.178 304.088,-136.267 307.118,-132.663 303.651,-133.148 303.651,-133.148 303.651,-133.148 307.118,-132.663 303.215,-130.028 310.584,-132.178 310.584,-132.178\"/>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-226.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-230.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-215.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M505.041,-204.326C524.202,-206.977 544.379,-209.767 563.759,-212.448\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"570.86,-213.43 563.494,-215.591 567.393,-212.951 563.926,-212.471 563.926,-212.471 563.926,-212.471 567.393,-212.951 564.357,-209.351 570.86,-213.43 570.86,-213.43\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-154.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M505.041,-177.414C524.202,-174.764 544.379,-171.973 563.759,-169.292\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"570.86,-168.31 564.357,-172.389 567.393,-168.79 563.926,-169.269 563.926,-169.269 563.926,-169.269 567.393,-168.79 563.494,-166.149 570.86,-168.31 570.86,-168.31\"/>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M503.193,-132.071C522.92,-134.799 543.794,-137.686 563.815,-140.456\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"570.858,-141.43 563.492,-143.591 567.391,-140.95 563.924,-140.471 563.924,-140.471 563.924,-140.471 567.391,-140.95 564.355,-137.35 570.858,-141.43 570.858,-141.43\"/>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-82.8701\" rx=\"110.118\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"669.029\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M503.193,-105.669C523.527,-102.857 545.081,-99.8757 565.662,-97.0289\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"572.602,-96.0691 566.099,-100.149 569.135,-96.5487 565.668,-97.0283 565.668,-97.0283 565.668,-97.0283 569.135,-96.5487 565.236,-93.908 572.602,-96.0691 572.602,-96.0691\"/>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-282.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-286.67\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-271.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M753.258,-244.974C780.48,-250.896 810.816,-257.494 838.448,-263.505\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"845.411,-265.019 837.901,-266.61 841.991,-264.275 838.571,-263.532 838.571,-263.532 838.571,-263.532 841.991,-264.275 839.24,-260.454 845.411,-265.019 845.411,-265.019\"/>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-210.87\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-214.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M778.836,-220.108C802.116,-218.661 826.286,-217.159 848.202,-215.797\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"855.234,-215.36 848.443,-218.938 851.741,-215.577 848.248,-215.794 848.248,-215.794 848.248,-215.794 851.741,-215.577 848.052,-212.65 855.234,-215.36 855.234,-215.36\"/>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M753.258,-172.974C786.856,-180.283 825.2,-188.623 857.346,-195.616\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"864.528,-197.178 857.019,-198.768 861.108,-196.434 857.688,-195.69 857.688,-195.69 857.688,-195.69 861.108,-196.434 858.358,-192.612 864.528,-197.178 864.528,-197.178\"/>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-138.87\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-142.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-127.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M778.836,-148.108C802.116,-146.661 826.286,-145.159 848.202,-143.797\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"855.234,-143.36 848.443,-146.938 851.741,-143.577 848.248,-143.794 848.248,-143.794 848.248,-143.794 851.741,-143.577 848.052,-140.65 855.234,-143.36 855.234,-143.36\"/>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M751.84,-100.666C785.792,-108.051 824.788,-116.533 857.397,-123.627\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"864.255,-125.118 856.745,-126.708 860.835,-124.374 857.414,-123.63 857.414,-123.63 857.414,-123.63 860.835,-124.374 858.084,-120.552 864.255,-125.118 864.255,-125.118\"/>\n",
+        "</g>\n",
+        "<!-- u5 -->\n",
+        "<g id=\"node11\" class=\"node\"><title>u5</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"941.474,-94.3701 915.474,-94.3701 915.474,-71.3701 941.474,-71.3701 941.474,-94.3701\"/>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;u5 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;u5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M779.582,-82.8701C828.369,-82.8701 880.914,-82.8701 908.333,-82.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"915.376,-82.8701 908.376,-86.0202 911.876,-82.8701 908.376,-82.8702 908.376,-82.8702 908.376,-82.8702 911.876,-82.8701 908.376,-79.7202 915.376,-82.8701 915.376,-82.8701\"/>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g id=\"node12\" class=\"node\"><title>9</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-26.8701\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"928.474\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M751.84,-65.0744C785.792,-57.6891 824.788,-49.2066 857.397,-42.1134\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"864.255,-40.6217 858.084,-45.1877 860.835,-41.3657 857.414,-42.1097 857.414,-42.1097 857.414,-42.1097 860.835,-41.3657 856.745,-39.0316 864.255,-40.6217 864.255,-40.6217\"/>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g id=\"edge15\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M898.965,-309.141C897.654,-319.298 907.49,-327.74 928.474,-327.74 944.213,-327.74 953.68,-322.991 956.877,-316.332\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"957.984,-309.141 960.032,-316.538 957.451,-312.6 956.919,-316.059 956.919,-316.059 956.919,-316.059 957.451,-312.6 953.806,-315.58 957.984,-309.141 957.984,-309.141\"/>\n",
+        "</g>\n",
+        "<!-- u7 -->\n",
+        "<g id=\"node13\" class=\"node\"><title>u7</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-222.37 1074.78,-222.37 1074.78,-199.37 1100.78,-199.37 1100.78,-222.37\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1087.78\" y=\"-207.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;u7 -->\n",
+        "<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-210.87C1026.7,-210.87 1050.95,-210.87 1067.23,-210.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-210.87 1067.54,-214.02 1071.04,-210.87 1067.54,-210.87 1067.54,-210.87 1067.54,-210.87 1071.04,-210.87 1067.54,-207.72 1074.54,-210.87 1074.54,-210.87\"/>\n",
+        "</g>\n",
+        "<!-- u8 -->\n",
+        "<g id=\"node14\" class=\"node\"><title>u8</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-150.37 1074.78,-150.37 1074.78,-127.37 1100.78,-127.37 1100.78,-150.37\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1087.78\" y=\"-135.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;u8 -->\n",
+        "<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;u8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-138.87C1026.7,-138.87 1050.95,-138.87 1067.23,-138.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-138.87 1067.54,-142.02 1071.04,-138.87 1067.54,-138.87 1067.54,-138.87 1067.54,-138.87 1071.04,-138.87 1067.54,-135.72 1074.54,-138.87 1074.54,-138.87\"/>\n",
+        "</g>\n",
+        "<!-- u9 -->\n",
+        "<g id=\"node15\" class=\"node\"><title>u9</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-38.3701 1074.78,-38.3701 1074.78,-15.3701 1100.78,-15.3701 1100.78,-38.3701\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1087.78\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;u9 -->\n",
+        "<g id=\"edge18\" class=\"edge\"><title>9&#45;&gt;u9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-26.8701C1026.7,-26.8701 1050.95,-26.8701 1067.23,-26.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-26.8701 1067.54,-30.0202 1071.04,-26.8701 1067.54,-26.8702 1067.54,-26.8702 1067.54,-26.8702 1071.04,-26.8701 1067.54,-23.7202 1074.54,-26.8701 1074.54,-26.8701\"/>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x109e19ed0> >"
+       ]
+      }
+     ],
+     "prompt_number": 10
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "k.show('.<15')"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 11,
+       "svg": [
+        "<svg height=\"204pt\" viewBox=\"0.00 0.00 734.00 203.83\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.535353 0.535353) rotate(0) translate(4 376.74)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-376.74 1367.06,-376.74 1367.06,4 -4,4\" stroke=\"none\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"147.309\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-187.67\">a=0, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-172.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.10532,-183.87C2.30847,-183.87 13.7102,-183.87 29.6433,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"36.7326,-183.87 29.7326,-187.02 33.2326,-183.87 29.7326,-183.87 29.7326,-183.87 29.7326,-183.87 33.2326,-183.87 29.7326,-180.72 36.7326,-183.87 36.7326,-183.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"406.754\" cy=\"-219.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-223.67\">a=1, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-208.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M243.441,-197.173C262.448,-199.831 282.507,-202.636 301.795,-205.333\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.862,-206.321 301.493,-208.471 305.396,-205.836 301.93,-205.352 301.93,-205.352 301.93,-205.352 305.396,-205.836 302.366,-202.232 308.862,-206.321 308.862,-206.321\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"406.754\" cy=\"-147.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-151.67\">a=0, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-136.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M243.441,-170.567C263.044,-167.826 283.766,-164.928 303.606,-162.154\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"310.584,-161.178 304.088,-165.267 307.118,-161.663 303.651,-162.148 303.651,-162.148 303.651,-162.148 307.118,-161.663 303.215,-159.028 310.584,-161.178 310.584,-161.178\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-259.67\">a=2, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-244.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M505.041,-233.326C524.202,-235.977 544.379,-238.767 563.759,-241.448\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.86,-242.43 563.494,-244.591 567.393,-241.951 563.926,-241.471 563.926,-241.471 563.926,-241.471 567.393,-241.951 564.357,-238.351 570.86,-242.43 570.86,-242.43\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-187.67\">a=1, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-172.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
+        "<path d=\"M505.041,-206.414C524.202,-203.764 544.379,-200.973 563.759,-198.292\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.86,-197.31 564.357,-201.389 567.393,-197.79 563.926,-198.269 563.926,-198.269 563.926,-198.269 567.393,-197.79 563.494,-195.149 570.86,-197.31 570.86,-197.31\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M503.193,-161.071C522.92,-163.799 543.794,-166.686 563.815,-169.456\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.858,-170.43 563.492,-172.591 567.391,-169.95 563.924,-169.471 563.924,-169.471 563.924,-169.471 567.391,-169.95 564.355,-166.35 570.858,-170.43 570.858,-170.43\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-115.67\">a=0, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-100.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
+        "<path d=\"M503.193,-134.669C523.527,-131.857 545.081,-128.876 565.662,-126.029\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"572.602,-125.069 566.099,-129.149 569.135,-125.549 565.668,-126.028 565.668,-126.028 565.668,-126.028 569.135,-125.549 565.236,-122.908 572.602,-125.069 572.602,-125.069\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-331.67\">a=3, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-316.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
+        "<path d=\"M743.569,-276.214C776.83,-285.415 816.217,-296.31 850.223,-305.718\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"857.394,-307.701 849.808,-308.871 854.021,-306.768 850.648,-305.835 850.648,-305.835 850.648,-305.835 854.021,-306.768 851.487,-302.799 857.394,-307.701 857.394,-307.701\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-259.67\">a=2, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-244.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
+        "<path d=\"M782.297,-255.87C791.726,-255.87 801.282,-255.87 810.763,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"817.995,-255.87 810.995,-259.02 814.495,-255.87 810.995,-255.87 810.995,-255.87 810.995,-255.87 814.495,-255.87 810.995,-252.72 817.995,-255.87 817.995,-255.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
+        "<path d=\"M743.569,-204.214C776.69,-213.376 815.885,-224.218 849.793,-233.598\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"856.944,-235.577 849.357,-236.746 853.571,-234.644 850.197,-233.71 850.197,-233.71 850.197,-233.71 853.571,-234.644 851.037,-230.674 856.944,-235.577 856.944,-235.577\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-187.67\">a=1, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-172.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
+        "<path d=\"M782.297,-183.87C791.726,-183.87 801.282,-183.87 810.763,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"817.995,-183.87 810.995,-187.02 814.495,-183.87 810.995,-183.87 810.995,-183.87 810.995,-183.87 814.495,-183.87 810.995,-180.72 817.995,-183.87 817.995,-183.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
+        "<path d=\"M742.529,-131.926C775.95,-141.171 815.726,-152.175 850.047,-161.669\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"856.835,-163.547 849.249,-164.716 853.462,-162.614 850.089,-161.68 850.089,-161.68 850.089,-161.68 853.462,-162.614 850.929,-158.644 856.835,-163.547 856.835,-163.547\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-15.6701\">...</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
+        "<path d=\"M735.707,-90.421C776.564,-77.078 828.761,-60.0315 868.808,-46.953\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"875.632,-44.7245 869.955,-49.892 872.305,-45.811 868.978,-46.8976 868.978,-46.8976 868.978,-46.8976 872.305,-45.811 868,-43.9033 875.632,-44.7245 875.632,-44.7245\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10 -->\n",
+        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-115.67\">a=0, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-100.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;10 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
+        "<path d=\"M779.654,-111.87C790.929,-111.87 802.414,-111.87 813.761,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"820.804,-111.87 813.804,-115.02 817.304,-111.87 813.804,-111.87 813.804,-111.87 813.804,-111.87 817.304,-111.87 813.804,-108.72 820.804,-111.87 820.804,-111.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
+        "<path d=\"M883.684,-352.332C879.148,-363.275 895.021,-372.74 931.303,-372.74 959.081,-372.74 974.895,-367.192 978.747,-359.68\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"978.922,-352.332 981.905,-359.404 978.839,-355.831 978.756,-359.33 978.756,-359.33 978.756,-359.33 978.839,-355.831 975.607,-359.255 978.922,-352.332 978.922,-352.332\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 11 -->\n",
+        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
+        "<ellipse cx=\"1190.75\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-331.67\">a=3, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-316.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
+        "<path d=\"M1005.39,-276.31C1038.14,-285.47 1076.85,-296.294 1110.31,-305.654\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1117.37,-307.628 1109.78,-308.777 1114,-306.686 1110.63,-305.743 1110.63,-305.743 1110.63,-305.743 1114,-306.686 1111.48,-302.709 1117.37,-307.628 1117.37,-307.628\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 12 -->\n",
+        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
+        "<ellipse cx=\"1190.75\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-259.67\">a=2, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-244.67\">...</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
+        "<path d=\"M1044.47,-255.87C1066.29,-255.87 1088.75,-255.87 1109.3,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1116.48,-255.87 1109.48,-259.02 1112.98,-255.87 1109.48,-255.87 1109.48,-255.87 1109.48,-255.87 1112.98,-255.87 1109.48,-252.72 1116.48,-255.87 1116.48,-255.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
+        "<path d=\"M1005.39,-204.31C1042.88,-214.794 1088.16,-227.46 1124.47,-237.614\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1131.61,-239.609 1124.02,-240.758 1128.24,-238.667 1124.87,-237.724 1124.87,-237.724 1124.87,-237.724 1128.24,-238.667 1125.71,-234.69 1131.61,-239.609 1131.61,-239.609\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 13 -->\n",
+        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
+        "<ellipse cx=\"1190.75\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-187.67\">a=1, b=3, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-172.67\">...</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;13 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
+        "<path d=\"M1044.47,-183.87C1066.29,-183.87 1088.75,-183.87 1109.3,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1116.48,-183.87 1109.48,-187.02 1112.98,-183.87 1109.48,-183.87 1109.48,-183.87 1109.48,-183.87 1112.98,-183.87 1109.48,-180.72 1116.48,-183.87 1116.48,-183.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 14 -->\n",
+        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
+        "<ellipse cx=\"1190.75\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-115.67\">a=1, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-100.67\">...</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
+        "<path d=\"M1005.39,-163.43C1042.88,-152.946 1088.16,-140.281 1124.47,-130.127\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1131.61,-128.131 1125.71,-133.05 1128.24,-129.073 1124.87,-130.016 1124.87,-130.016 1124.87,-130.016 1128.24,-129.073 1124.02,-126.982 1131.61,-128.131 1131.61,-128.131\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u9 -->\n",
+        "<g class=\"node\" id=\"node17\"><title>u9</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1203.75,-26.3701 1177.75,-26.3701 1177.75,-3.37006 1203.75,-3.37006 1203.75,-26.3701\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-11.1701\">...</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;u9 -->\n",
+        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;u9</title>\n",
+        "<path d=\"M1005.04,-23.4795C1061.44,-20.8505 1135.65,-17.3916 1170.33,-15.7753\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1177.49,-15.4414 1170.65,-18.914 1173.99,-15.6044 1170.5,-15.7674 1170.5,-15.7674 1170.5,-15.7674 1173.99,-15.6044 1170.35,-12.6208 1177.49,-15.4414 1177.49,-15.4414\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;14</title>\n",
+        "<path d=\"M1041.86,-111.87C1064.48,-111.87 1087.91,-111.87 1109.27,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1116.43,-111.87 1109.43,-115.02 1112.93,-111.87 1109.43,-111.87 1109.43,-111.87 1109.43,-111.87 1112.93,-111.87 1109.43,-108.72 1116.43,-111.87 1116.43,-111.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u10 -->\n",
+        "<g class=\"node\" id=\"node18\"><title>u10</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1203.75,-67.3701 1177.75,-67.3701 1177.75,-44.3701 1203.75,-44.3701 1203.75,-67.3701\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-52.1701\">...</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;u10 -->\n",
+        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;u10</title>\n",
+        "<path d=\"M1008.23,-92.5305C1031.35,-86.8813 1056.88,-80.8833 1080.44,-75.8701 1111.84,-69.1887 1148.59,-62.744 1170.48,-59.0506\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1177.57,-57.863 1171.19,-62.1263 1174.12,-58.4413 1170.67,-59.0196 1170.67,-59.0196 1170.67,-59.0196 1174.12,-58.4413 1170.15,-55.9129 1177.57,-57.863 1177.57,-57.863\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
+        "<path d=\"M1161.24,-354.141C1159.93,-364.298 1169.76,-372.74 1190.75,-372.74 1206.49,-372.74 1215.95,-367.991 1219.15,-361.332\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1220.26,-354.141 1222.31,-361.538 1219.73,-357.6 1219.19,-361.059 1219.19,-361.059 1219.19,-361.059 1219.73,-357.6 1216.08,-360.58 1220.26,-354.141 1220.26,-354.141\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u12 -->\n",
+        "<g class=\"node\" id=\"node19\"><title>u12</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1363.06,-267.37 1337.06,-267.37 1337.06,-244.37 1363.06,-244.37 1363.06,-267.37\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-252.17\">...</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;u12 -->\n",
+        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;u12</title>\n",
+        "<path d=\"M1265.34,-255.87C1288.98,-255.87 1313.23,-255.87 1329.5,-255.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1336.82,-255.87 1329.82,-259.02 1333.32,-255.87 1329.82,-255.87 1329.82,-255.87 1329.82,-255.87 1333.32,-255.87 1329.82,-252.72 1336.82,-255.87 1336.82,-255.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u13 -->\n",
+        "<g class=\"node\" id=\"node20\"><title>u13</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1363.06,-195.37 1337.06,-195.37 1337.06,-172.37 1363.06,-172.37 1363.06,-195.37\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-180.17\">...</text>\n",
+        "</g>\n",
+        "<!-- 13&#45;&gt;u13 -->\n",
+        "<g class=\"edge\" id=\"edge26\"><title>13-&gt;u13</title>\n",
+        "<path d=\"M1265.34,-183.87C1288.98,-183.87 1313.23,-183.87 1329.5,-183.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1336.82,-183.87 1329.82,-187.02 1333.32,-183.87 1329.82,-183.87 1329.82,-183.87 1329.82,-183.87 1333.32,-183.87 1329.82,-180.72 1336.82,-183.87 1336.82,-183.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u14 -->\n",
+        "<g class=\"node\" id=\"node21\"><title>u14</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1363.06,-123.37 1337.06,-123.37 1337.06,-100.37 1363.06,-100.37 1363.06,-123.37\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-108.17\">...</text>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;u14 -->\n",
+        "<g class=\"edge\" id=\"edge27\"><title>14-&gt;u14</title>\n",
+        "<path d=\"M1265.34,-111.87C1288.98,-111.87 1313.23,-111.87 1329.5,-111.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1336.82,-111.87 1329.82,-115.02 1333.32,-111.87 1329.82,-111.87 1329.82,-111.87 1329.82,-111.87 1333.32,-111.87 1329.82,-108.72 1336.82,-111.87 1336.82,-111.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 11
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "k.show('.<0')  # unlimited output"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 12,
+       "svg": [
+        "<svg height=\"154pt\" viewBox=\"0.00 0.00 734.00 153.94\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.399073 0.399073) rotate(0) translate(4 381.74)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-381.74 1835.26,-381.74 1835.26,4 -4,4\" stroke=\"none\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"147.309\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-192.67\">a=0, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-177.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.10532,-188.87C2.30847,-188.87 13.7102,-188.87 29.6433,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"36.7326,-188.87 29.7326,-192.02 33.2326,-188.87 29.7326,-188.87 29.7326,-188.87 29.7326,-188.87 33.2326,-188.87 29.7326,-185.72 36.7326,-188.87 36.7326,-188.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"406.754\" cy=\"-224.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-228.67\">a=1, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-213.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M243.441,-202.173C262.448,-204.831 282.507,-207.636 301.795,-210.333\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.862,-211.321 301.493,-213.471 305.396,-210.836 301.93,-210.352 301.93,-210.352 301.93,-210.352 305.396,-210.836 302.366,-207.232 308.862,-211.321 308.862,-211.321\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"406.754\" cy=\"-152.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-156.67\">a=0, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-141.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M243.441,-175.567C263.044,-172.826 283.766,-169.928 303.606,-167.154\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"310.584,-166.178 304.088,-170.267 307.118,-166.663 303.651,-167.148 303.651,-167.148 303.651,-167.148 307.118,-166.663 303.215,-164.028 310.584,-166.178 310.584,-166.178\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-264.67\">a=2, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M505.041,-238.326C524.202,-240.977 544.379,-243.767 563.759,-246.448\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.86,-247.43 563.494,-249.591 567.393,-246.951 563.926,-246.471 563.926,-246.471 563.926,-246.471 567.393,-246.951 564.357,-243.351 570.86,-247.43 570.86,-247.43\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-192.67\">a=1, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
+        "<path d=\"M505.041,-211.414C524.202,-208.764 544.379,-205.973 563.759,-203.292\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.86,-202.31 564.357,-206.389 567.393,-202.79 563.926,-203.269 563.926,-203.269 563.926,-203.269 567.393,-202.79 563.494,-200.149 570.86,-202.31 570.86,-202.31\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M503.193,-166.071C522.92,-168.799 543.794,-171.686 563.815,-174.456\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"570.858,-175.43 563.492,-177.591 567.391,-174.95 563.924,-174.471 563.924,-174.471 563.924,-174.471 567.391,-174.95 564.355,-171.35 570.858,-175.43 570.858,-175.43\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
+        "<ellipse cx=\"669.029\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-120.67\">a=0, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-105.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
+        "<path d=\"M503.193,-139.669C523.527,-136.857 545.081,-133.876 565.662,-131.029\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"572.602,-130.069 566.099,-134.149 569.135,-130.549 565.668,-131.028 565.668,-131.028 565.668,-131.028 569.135,-130.549 565.236,-127.908 572.602,-130.069 572.602,-130.069\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-336.67\">a=3, b=0, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
+        "<path d=\"M743.569,-281.214C776.83,-290.415 816.217,-301.31 850.223,-310.718\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"857.394,-312.701 849.808,-313.871 854.021,-311.768 850.648,-310.835 850.648,-310.835 850.648,-310.835 854.021,-311.768 851.487,-307.799 857.394,-312.701 857.394,-312.701\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-264.67\">a=2, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
+        "<path d=\"M782.297,-260.87C791.726,-260.87 801.282,-260.87 810.763,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"817.995,-260.87 810.995,-264.02 814.495,-260.87 810.995,-260.87 810.995,-260.87 810.995,-260.87 814.495,-260.87 810.995,-257.72 817.995,-260.87 817.995,-260.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
+        "<path d=\"M743.569,-209.214C776.69,-218.376 815.885,-229.218 849.793,-238.598\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"856.944,-240.577 849.357,-241.746 853.571,-239.644 850.197,-238.71 850.197,-238.71 850.197,-238.71 853.571,-239.644 851.037,-235.674 856.944,-240.577 856.944,-240.577\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-192.67\">a=1, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
+        "<path d=\"M782.297,-188.87C791.726,-188.87 801.282,-188.87 810.763,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"817.995,-188.87 810.995,-192.02 814.495,-188.87 810.995,-188.87 810.995,-188.87 810.995,-188.87 814.495,-188.87 810.995,-185.72 817.995,-188.87 817.995,-188.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
+        "<path d=\"M742.529,-136.926C775.95,-146.171 815.726,-157.175 850.047,-166.669\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"856.835,-168.547 849.249,-169.716 853.462,-167.614 850.089,-166.68 850.089,-166.68 850.089,-166.68 853.462,-167.614 850.929,-163.644 856.835,-168.547 856.835,-168.547\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-35.8701\" fill=\"#ffffaa\" rx=\"108.375\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-39.6701\">a=0, b=3, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-24.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
+        "<path d=\"M737.733,-95.7997C774.033,-84.5029 818.826,-70.5628 856.074,-58.9709\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"862.937,-56.8349 857.189,-61.9228 859.595,-57.875 856.253,-58.915 856.253,-58.915 856.253,-58.915 859.595,-57.875 855.317,-55.9073 862.937,-56.8349 862.937,-56.8349\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10 -->\n",
+        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
+        "<ellipse cx=\"931.303\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-120.67\">a=0, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-105.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;10 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
+        "<path d=\"M779.654,-116.87C790.929,-116.87 802.414,-116.87 813.761,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"820.804,-116.87 813.804,-120.02 817.304,-116.87 813.804,-116.87 813.804,-116.87 813.804,-116.87 817.304,-116.87 813.804,-113.72 820.804,-116.87 820.804,-116.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
+        "<path d=\"M882.945,-357.332C878.34,-368.275 894.459,-377.74 931.303,-377.74 959.511,-377.74 975.571,-372.192 979.483,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"979.66,-357.332 982.641,-364.406 979.576,-360.831 979.491,-364.33 979.491,-364.33 979.491,-364.33 979.576,-360.831 976.342,-364.254 979.66,-357.332 979.66,-357.332\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 11 -->\n",
+        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
+        "<ellipse cx=\"1193.58\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-336.67\">a=3, b=1, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
+        "<path d=\"M1005.84,-281.214C1039.1,-290.415 1078.49,-301.31 1112.5,-310.718\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1119.67,-312.701 1112.08,-313.871 1116.3,-311.768 1112.92,-310.835 1112.92,-310.835 1112.92,-310.835 1116.3,-311.768 1113.76,-307.799 1119.67,-312.701 1119.67,-312.701\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 12 -->\n",
+        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
+        "<ellipse cx=\"1193.58\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-264.67\">a=2, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
+        "<path d=\"M1044.57,-260.87C1054,-260.87 1063.56,-260.87 1073.04,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1080.27,-260.87 1073.27,-264.02 1076.77,-260.87 1073.27,-260.87 1073.27,-260.87 1073.27,-260.87 1076.77,-260.87 1073.27,-257.72 1080.27,-260.87 1080.27,-260.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
+        "<path d=\"M1005.84,-209.214C1038.96,-218.376 1078.16,-229.218 1112.07,-238.598\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1119.22,-240.577 1111.63,-241.746 1115.84,-239.644 1112.47,-238.71 1112.47,-238.71 1112.47,-238.71 1115.84,-239.644 1113.31,-235.674 1119.22,-240.577 1119.22,-240.577\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 13 -->\n",
+        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
+        "<ellipse cx=\"1193.58\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-192.67\">a=1, b=3, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;13 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
+        "<path d=\"M1044.57,-188.87C1054.97,-188.87 1065.52,-188.87 1075.95,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1083.15,-188.87 1076.15,-192.02 1079.65,-188.87 1076.15,-188.87 1076.15,-188.87 1076.15,-188.87 1079.65,-188.87 1076.15,-185.72 1083.15,-188.87 1083.15,-188.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 14 -->\n",
+        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
+        "<ellipse cx=\"1193.58\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-120.67\">a=1, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-105.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
+        "<path d=\"M1005.84,-168.526C1038.96,-159.364 1078.16,-148.522 1112.07,-139.142\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1119.22,-137.163 1113.31,-142.066 1115.84,-138.097 1112.47,-139.03 1112.47,-139.03 1112.47,-139.03 1115.84,-138.097 1111.63,-135.994 1119.22,-137.163 1119.22,-137.163\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 15 -->\n",
+        "<g class=\"node\" id=\"node17\"><title>15</title>\n",
+        "<ellipse cx=\"1193.58\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"105.218\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-30.6701\">a=0, b=3, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-15.6701\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;15</title>\n",
+        "<path d=\"M1038.54,-32.1964C1052.8,-31.7035 1067.45,-31.197 1081.78,-30.7014\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1088.78,-30.4592 1081.9,-33.8493 1085.28,-30.5802 1081.79,-30.7012 1081.79,-30.7012 1081.79,-30.7012 1085.28,-30.5802 1081.68,-27.5531 1088.78,-30.4592 1088.78,-30.4592\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;14</title>\n",
+        "<path d=\"M1041.93,-116.87C1052.2,-116.87 1062.65,-116.87 1073,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1080.16,-116.87 1073.16,-120.02 1076.66,-116.87 1073.16,-116.87 1073.16,-116.87 1073.16,-116.87 1076.66,-116.87 1073.16,-113.72 1080.16,-116.87 1080.16,-116.87\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;15</title>\n",
+        "<path d=\"M995.64,-94.9687C1034.33,-81.59 1083.83,-64.4742 1123.52,-50.7489\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1130.31,-48.4023 1124.72,-53.667 1127,-49.5461 1123.69,-50.69 1123.69,-50.69 1123.69,-50.69 1127,-49.5461 1122.66,-47.7129 1130.31,-48.4023 1130.31,-48.4023\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
+        "<path d=\"M1145.22,-357.332C1140.61,-368.275 1156.73,-377.74 1193.58,-377.74 1221.79,-377.74 1237.85,-372.192 1241.76,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1241.93,-357.332 1244.91,-364.406 1241.85,-360.831 1241.77,-364.33 1241.77,-364.33 1241.77,-364.33 1241.85,-360.831 1238.62,-364.254 1241.93,-357.332 1241.93,-357.332\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 16 -->\n",
+        "<g class=\"node\" id=\"node18\"><title>16</title>\n",
+        "<ellipse cx=\"1455.85\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-336.67\">a=3, b=2, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;16 -->\n",
+        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;16</title>\n",
+        "<path d=\"M1268.12,-281.214C1301.24,-290.376 1340.43,-301.218 1374.34,-310.598\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1381.49,-312.577 1373.91,-313.746 1378.12,-311.644 1374.75,-310.71 1374.75,-310.71 1374.75,-310.71 1378.12,-311.644 1375.59,-307.674 1381.49,-312.577 1381.49,-312.577\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 17 -->\n",
+        "<g class=\"node\" id=\"node19\"><title>17</title>\n",
+        "<ellipse cx=\"1455.85\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-192.67\">a=2, b=3, Q=0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;17 -->\n",
+        "<g class=\"edge\" id=\"edge26\"><title>12-&gt;17</title>\n",
+        "<path d=\"M1268.12,-240.526C1301.38,-231.325 1340.77,-220.43 1374.77,-211.023\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1381.94,-209.039 1376.04,-213.941 1378.57,-209.972 1375.2,-210.905 1375.2,-210.905 1375.2,-210.905 1378.57,-209.972 1374.36,-207.869 1381.94,-209.039 1381.94,-209.039\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 18 -->\n",
+        "<g class=\"node\" id=\"node20\"><title>18</title>\n",
+        "<ellipse cx=\"1455.85\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-264.67\">a=2, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-249.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;18 -->\n",
+        "<g class=\"edge\" id=\"edge27\"><title>12-&gt;18</title>\n",
+        "<path d=\"M1303.45,-254.201C1315.1,-254.112 1326.98,-254.096 1338.72,-254.155\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1346,-254.201 1338.98,-257.307 1342.5,-254.179 1339,-254.157 1339,-254.157 1339,-254.157 1342.5,-254.179 1339.02,-251.007 1346,-254.201 1346,-254.201\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 19 -->\n",
+        "<g class=\"node\" id=\"node21\"><title>19</title>\n",
+        "<ellipse cx=\"1455.85\" cy=\"-98.8701\" fill=\"#ffffaa\" rx=\"108.375\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-102.67\">a=1, b=3, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-87.6701\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 13&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge28\"><title>13-&gt;19</title>\n",
+        "<path d=\"M1262.02,-167.688C1276.78,-162.92 1292.3,-157.808 1306.71,-152.87 1333.58,-143.666 1362.99,-133.055 1388.48,-123.688\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1395.21,-121.209 1389.73,-126.584 1391.93,-122.418 1388.65,-123.628 1388.65,-123.628 1388.65,-123.628 1391.93,-122.418 1387.56,-120.671 1395.21,-121.209 1395.21,-121.209\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;18 -->\n",
+        "<g class=\"edge\" id=\"edge29\"><title>14-&gt;18</title>\n",
+        "<path d=\"M1277.62,-135.06C1288.13,-139.712 1298.18,-145.549 1306.71,-152.87 1333.87,-176.161 1315.56,-201.579 1342.71,-224.87 1349.52,-230.704 1357.28,-235.595 1365.47,-239.696\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1371.81,-242.681 1364.13,-242.549 1368.64,-241.19 1365.47,-239.699 1365.47,-239.699 1365.47,-239.699 1368.64,-241.19 1366.81,-236.849 1371.81,-242.681 1371.81,-242.681\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge30\"><title>14-&gt;19</title>\n",
+        "<path d=\"M1302.32,-109.419C1316.13,-108.463 1330.3,-107.484 1344.16,-106.525\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1351.37,-106.026 1344.61,-109.652 1347.88,-106.268 1344.39,-106.509 1344.39,-106.509 1344.39,-106.509 1347.88,-106.268 1344.17,-103.367 1351.37,-106.026 1351.37,-106.026\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 15&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge31\"><title>15-&gt;15</title>\n",
+        "<path d=\"M1145.42,-50.8749C1140.17,-62.0106 1156.22,-71.7401 1193.58,-71.7401 1222.76,-71.7401 1238.94,-65.8017 1242.12,-57.8937\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1241.73,-50.8749 1245.26,-57.6898 1241.92,-54.3695 1242.12,-57.8641 1242.12,-57.8641 1242.12,-57.8641 1241.92,-54.3695 1238.97,-58.0385 1241.73,-50.8749 1241.73,-50.8749\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 20 -->\n",
+        "<g class=\"node\" id=\"node22\"><title>20</title>\n",
+        "<ellipse cx=\"1718.13\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-336.67\">a=3, b=2, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-321.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 16&#45;&gt;20 -->\n",
+        "<g class=\"edge\" id=\"edge32\"><title>16-&gt;20</title>\n",
+        "<path d=\"M1565.72,-326.201C1577.37,-326.112 1589.26,-326.096 1600.99,-326.155\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1608.27,-326.201 1601.25,-329.307 1604.77,-326.179 1601.27,-326.157 1601.27,-326.157 1601.27,-326.157 1604.77,-326.179 1601.29,-323.007 1608.27,-326.201 1608.27,-326.201\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 21 -->\n",
+        "<g class=\"node\" id=\"node23\"><title>21</title>\n",
+        "<ellipse cx=\"1718.13\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-192.67\">a=2, b=3, Q=1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-177.67\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 17&#45;&gt;21 -->\n",
+        "<g class=\"edge\" id=\"edge33\"><title>17-&gt;21</title>\n",
+        "<path d=\"M1563.09,-182.222C1576.62,-182.105 1590.5,-182.089 1604.13,-182.172\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1611.23,-182.225 1604.2,-185.323 1607.73,-182.199 1604.23,-182.173 1604.23,-182.173 1604.23,-182.173 1607.73,-182.199 1604.25,-179.023 1611.23,-182.225 1611.23,-182.225\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge36\"><title>18-&gt;12</title>\n",
+        "<path d=\"M1346,-267.539C1334.35,-267.628 1322.46,-267.644 1310.73,-267.585\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1303.45,-267.539 1310.47,-264.434 1306.95,-267.561 1310.45,-267.584 1310.45,-267.584 1310.45,-267.584 1306.95,-267.561 1310.43,-270.734 1303.45,-267.539 1303.45,-267.539\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;20 -->\n",
+        "<g class=\"edge\" id=\"edge34\"><title>18-&gt;20</title>\n",
+        "<path d=\"M1530.39,-281.214C1563.51,-290.376 1602.71,-301.218 1636.62,-310.598\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1643.77,-312.577 1636.18,-313.746 1640.39,-311.644 1637.02,-310.71 1637.02,-310.71 1637.02,-310.71 1640.39,-311.644 1637.86,-307.674 1643.77,-312.577 1643.77,-312.577\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;21 -->\n",
+        "<g class=\"edge\" id=\"edge35\"><title>18-&gt;21</title>\n",
+        "<path d=\"M1530.39,-240.526C1563.65,-231.325 1603.04,-220.43 1637.05,-211.023\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1644.22,-209.039 1638.31,-213.941 1640.84,-209.972 1637.47,-210.905 1637.47,-210.905 1637.47,-210.905 1640.84,-209.972 1636.63,-207.869 1644.22,-209.039 1644.22,-209.039\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 19&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge37\"><title>19-&gt;19</title>\n",
+        "<path d=\"M1407.49,-123.332C1402.89,-134.275 1419.01,-143.74 1455.85,-143.74 1484.06,-143.74 1500.12,-138.192 1504.03,-130.68\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1504.21,-123.332 1507.19,-130.406 1504.12,-126.831 1504.04,-130.33 1504.04,-130.33 1504.04,-130.33 1504.12,-126.831 1500.89,-130.254 1504.21,-123.332 1504.21,-123.332\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 20&#45;&gt;16 -->\n",
+        "<g class=\"edge\" id=\"edge38\"><title>20-&gt;16</title>\n",
+        "<path d=\"M1608.27,-339.539C1596.62,-339.628 1584.74,-339.644 1573,-339.585\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1565.72,-339.539 1572.74,-336.434 1569.22,-339.561 1572.72,-339.584 1572.72,-339.584 1572.72,-339.584 1569.22,-339.561 1572.7,-342.734 1565.72,-339.539 1565.72,-339.539\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 21&#45;&gt;17 -->\n",
+        "<g class=\"edge\" id=\"edge39\"><title>21-&gt;17</title>\n",
+        "<path d=\"M1611.23,-195.515C1597.71,-195.633 1583.82,-195.652 1570.19,-195.57\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1563.09,-195.518 1570.11,-192.419 1566.59,-195.544 1570.09,-195.569 1570.09,-195.569 1570.09,-195.569 1566.59,-195.544 1570.07,-198.719 1563.09,-195.518 1563.09,-195.518\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 12
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "a = spot.translate('\"a<1\" U \"b>2\"'); a"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 13,
+       "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=\"197pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 197.00 85.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 81)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 194,-81 194,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 193,-81 193,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 1 -->\n",
         "<g id=\"node2\" class=\"node\"><title>1</title>\n",
@@ -1066,35 +1149,35 @@
         "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
-        "<text text-anchor=\"start\" x=\"10.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot;</text>\n",
+        "<text text-anchor=\"start\" x=\"11.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot;</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"168\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<ellipse fill=\"none\" stroke=\"black\" cx=\"168\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
-        "<text text-anchor=\"middle\" x=\"168\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"167\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.1875,-22C91.4086,-22 118.216,-22 138.601,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"145.791,-22 138.791,-25.1501 142.291,-22 138.791,-22.0001 138.791,-22.0001 138.791,-22.0001 142.291,-22 138.791,-18.8501 145.791,-22 145.791,-22\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.0312,-22C91.0958,-22 117.659,-22 137.859,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"144.984,-22 137.984,-25.1501 141.484,-22 137.984,-22.0001 137.984,-22.0001 137.984,-22.0001 141.484,-22 137.984,-18.8501 144.984,-22 144.984,-22\"/>\n",
         "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;b&gt;2&quot;</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=\"M157.574,-41.7575C155.802,-52.3499 159.277,-62 168,-62 174.678,-62 178.281,-56.3433 178.807,-48.9379\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"178.426,-41.7575 181.943,-48.5807 178.612,-45.2526 178.797,-48.7476 178.797,-48.7476 178.797,-48.7476 178.612,-45.2526 175.652,-48.9146 178.426,-41.7575 178.426,-41.7575\"/>\n",
-        "<text text-anchor=\"middle\" x=\"168\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M156.933,-41.7575C155.223,-52.3499 158.578,-62 167,-62 173.448,-62 176.926,-56.3433 177.435,-48.9379\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"177.067,-41.7575 180.571,-48.5871 177.246,-45.2529 177.425,-48.7483 177.425,-48.7483 177.425,-48.7483 177.246,-45.2529 174.279,-48.9095 177.067,-41.7575 177.067,-41.7575\"/>\n",
+        "<text text-anchor=\"middle\" x=\"167\" y=\"-65.8\" 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 0x7f426c05f960> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x109eaaab0> >"
        ]
       }
      ],
-     "prompt_number": 10
+     "prompt_number": 13
     },
     {
      "cell_type": "code",
@@ -1108,7 +1191,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 11,
+       "prompt_number": 14,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -1116,147 +1199,147 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"734pt\" height=\"105pt\"\n",
-        " viewBox=\"0.00 0.00 734.00 104.73\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.459345 0.459345) rotate(0) translate(4 224)\">\n",
+        "<svg width=\"734pt\" height=\"107pt\"\n",
+        " viewBox=\"0.00 0.00 734.00 106.67\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.467836 0.467836) rotate(0) translate(4 224)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-224 1593.93,-224 1593.93,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-224 1564.93,-224 1564.93,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"121.193\" cy=\"-179\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"121.193\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"119.893\" cy=\"-179\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"119.893\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0 * 1</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.08639,-179C2.22134,-179 14.4198,-179 30.6117,-179\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.775,-179 30.775,-182.15 34.275,-179 30.775,-179 30.775,-179 30.775,-179 34.275,-179 30.7749,-175.85 37.775,-179 37.775,-179\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.08545,-179C2.21412,-179 14.4049,-179 30.5502,-179\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.691,-179 30.6911,-182.15 34.191,-179 30.691,-179 30.691,-179 30.691,-179 34.191,-179 30.691,-175.85 37.691,-179 37.691,-179\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"467.578\" cy=\"-202\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"467.578\" y=\"-198.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"459.678\" cy=\"-202\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"459.678\" y=\"-198.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M201.202,-184.277C254.796,-187.856 325.624,-192.586 380.627,-196.26\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"387.937,-196.748 380.742,-199.424 384.444,-196.515 380.952,-196.281 380.952,-196.281 380.952,-196.281 384.444,-196.515 381.162,-193.138 387.937,-196.748 387.937,-196.748\"/>\n",
-        "<text text-anchor=\"start\" x=\"222.385\" y=\"-198.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M198.388,-184.277C250.861,-187.85 320.179,-192.57 374.087,-196.24\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"381.252,-196.728 374.054,-199.395 377.76,-196.49 374.268,-196.252 374.268,-196.252 374.268,-196.252 377.76,-196.49 374.482,-193.11 381.252,-196.728 381.252,-196.728\"/>\n",
+        "<text text-anchor=\"start\" x=\"219.785\" y=\"-198.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"467.578\" cy=\"-148\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"467.578\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"459.678\" cy=\"-148\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"459.678\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M191.935,-169.446C202.138,-168.195 212.526,-167.002 222.385,-166 274.68,-160.684 333.428,-156.304 380.194,-153.196\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"387.299,-152.727 380.521,-156.331 383.806,-152.958 380.314,-153.188 380.314,-153.188 380.314,-153.188 383.806,-152.958 380.107,-150.045 387.299,-152.727 387.299,-152.727\"/>\n",
-        "<text text-anchor=\"start\" x=\"222.385\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M189.462,-169.485C199.619,-168.222 209.967,-167.014 219.785,-166 270.641,-160.746 327.738,-156.387 373.357,-153.275\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"380.577,-152.787 373.806,-156.402 377.085,-153.023 373.593,-153.26 373.593,-153.26 373.593,-153.26 377.085,-153.023 373.381,-150.117 380.577,-152.787 380.577,-152.787\"/>\n",
+        "<text text-anchor=\"start\" x=\"219.785\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"813.963\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"813.963\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"799.464\" cy=\"-171\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"799.464\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M547.587,-153.277C601.181,-156.856 672.009,-161.586 727.012,-165.26\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"734.322,-165.748 727.127,-168.424 730.83,-165.515 727.337,-165.281 727.337,-165.281 727.337,-165.281 730.83,-165.515 727.547,-162.138 734.322,-165.748 734.322,-165.748\"/>\n",
-        "<text text-anchor=\"start\" x=\"568.77\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M538.173,-153.277C590.647,-156.85 659.965,-161.57 713.873,-165.24\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"721.038,-165.728 713.84,-168.395 717.546,-165.49 714.054,-165.252 714.054,-165.252 714.054,-165.252 717.546,-165.49 714.268,-162.11 721.038,-165.728 721.038,-165.728\"/>\n",
+        "<text text-anchor=\"start\" x=\"559.571\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g id=\"node6\" class=\"node\"><title>4</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"813.963\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"813.963\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"799.464\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"799.464\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;4 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M538.32,-138.446C548.523,-137.195 558.911,-136.002 568.77,-135 621.065,-129.684 679.813,-125.304 726.579,-122.196\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"733.684,-121.727 726.907,-125.331 730.192,-121.958 726.699,-122.188 726.699,-122.188 726.699,-122.188 730.192,-121.958 726.492,-119.045 733.684,-121.727 733.684,-121.727\"/>\n",
-        "<text text-anchor=\"start\" x=\"568.77\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M529.248,-138.485C539.404,-137.222 549.753,-136.014 559.571,-135 610.427,-129.746 667.524,-125.387 713.143,-122.275\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"720.363,-121.787 713.592,-125.402 716.871,-122.023 713.379,-122.26 713.379,-122.26 713.379,-122.26 716.871,-122.023 713.166,-119.117 720.363,-121.787 720.363,-121.787\"/>\n",
+        "<text text-anchor=\"start\" x=\"559.571\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g id=\"node7\" class=\"node\"><title>5</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-171\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1139.25\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;5 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>4&#45;&gt;5</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M876.083,-129.044C888.968,-131.456 902.494,-133.893 915.156,-136 970.724,-145.246 1033.65,-154.231 1081.71,-160.781\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1088.69,-161.73 1081.33,-163.908 1085.22,-161.259 1081.76,-160.787 1081.76,-160.787 1081.76,-160.787 1085.22,-161.259 1082.18,-157.666 1088.69,-161.73 1088.69,-161.73\"/>\n",
-        "<text text-anchor=\"start\" x=\"915.156\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M860.791,-129.032C873.509,-131.444 886.859,-133.885 899.356,-136 953.606,-145.181 1015.03,-154.149 1062.01,-160.708\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1069.13,-161.699 1061.76,-163.853 1065.66,-161.216 1062.19,-160.734 1062.19,-160.734 1062.19,-160.734 1065.66,-161.216 1062.63,-157.614 1069.13,-161.699 1069.13,-161.699\"/>\n",
+        "<text text-anchor=\"start\" x=\"899.356\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 6 -->\n",
         "<g id=\"node8\" class=\"node\"><title>6</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1139.25\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;6 -->\n",
         "<g id=\"edge7\" class=\"edge\"><title>4&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M897.452,-117C949.442,-117 1016.57,-117 1069.85,-117\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1076.94,-117 1069.94,-120.15 1073.44,-117 1069.94,-117 1069.94,-117 1069.94,-117 1073.44,-117 1069.94,-113.85 1076.94,-117 1076.94,-117\"/>\n",
-        "<text text-anchor=\"start\" x=\"915.156\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M881.372,-117C932.168,-117 997.697,-117 1049.86,-117\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1057.12,-117 1050.12,-120.15 1053.62,-117 1050.12,-117 1050.12,-117 1050.12,-117 1053.62,-117 1050.12,-113.85 1057.12,-117 1057.12,-117\"/>\n",
+        "<text text-anchor=\"start\" x=\"899.356\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 7 -->\n",
         "<g id=\"node9\" class=\"node\"><title>7</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-63\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-63\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1139.25\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1 * 1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;7 -->\n",
         "<g id=\"edge8\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M876.083,-104.956C888.968,-102.544 902.494,-100.107 915.156,-98 970.724,-88.7538 1033.65,-79.7694 1081.71,-73.2187\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1088.69,-72.2701 1082.18,-76.3341 1085.22,-72.7414 1081.76,-73.2128 1081.76,-73.2128 1081.76,-73.2128 1085.22,-72.7414 1081.33,-70.0915 1088.69,-72.2701 1088.69,-72.2701\"/>\n",
-        "<text text-anchor=\"start\" x=\"915.156\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M860.791,-104.968C873.509,-102.556 886.859,-100.115 899.356,-98 953.606,-88.8191 1015.03,-79.8515 1062.01,-73.292\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1069.13,-72.3012 1062.63,-76.3864 1065.66,-72.7838 1062.19,-73.2664 1062.19,-73.2664 1062.19,-73.2664 1065.66,-72.7838 1061.76,-70.1465 1069.13,-72.3012 1069.13,-72.3012\"/>\n",
+        "<text text-anchor=\"start\" x=\"899.356\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 8 -->\n",
         "<g id=\"node10\" class=\"node\"><title>8</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1506.73\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1 * 0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1479.03\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1479.03\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1 * 0</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;8 -->\n",
         "<g id=\"edge9\" class=\"edge\"><title>6&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1243.84,-117C1295.83,-117 1362.95,-117 1416.23,-117\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1423.32,-117 1416.32,-120.15 1419.82,-117 1416.32,-117 1416.32,-117 1416.32,-117 1419.82,-117 1416.32,-113.85 1423.32,-117 1423.32,-117\"/>\n",
-        "<text text-anchor=\"start\" x=\"1263.54\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1221.16,-117C1271.95,-117 1337.48,-117 1389.64,-117\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1396.91,-117 1389.91,-120.15 1393.41,-117 1389.91,-117 1389.91,-117 1389.91,-117 1393.41,-117 1389.91,-113.85 1396.91,-117 1396.91,-117\"/>\n",
+        "<text text-anchor=\"start\" x=\"1240.64\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- u7 -->\n",
         "<g id=\"node11\" class=\"node\"><title>u7</title>\n",
-        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1519.73,-77.5 1493.73,-77.5 1493.73,-54.5 1519.73,-54.5 1519.73,-77.5\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1492.03,-77.5 1466.03,-77.5 1466.03,-54.5 1492.03,-54.5 1492.03,-77.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1479.03\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;u7 -->\n",
         "<g id=\"edge10\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1243.84,-63.7186C1324.16,-64.4183 1440.61,-65.4327 1486.3,-65.8307\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1493.5,-65.8934 1486.47,-68.9823 1490,-65.8629 1486.5,-65.8324 1486.5,-65.8324 1486.5,-65.8324 1490,-65.8629 1486.53,-62.6825 1493.5,-65.8934 1493.5,-65.8934\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1221.16,-63.7186C1299.76,-64.4166 1413.63,-65.428 1458.66,-65.8279\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1465.76,-65.891 1458.74,-68.9786 1462.26,-65.8599 1458.76,-65.8288 1458.76,-65.8288 1458.76,-65.8288 1462.26,-65.8599 1458.79,-62.6789 1465.76,-65.891 1465.76,-65.891\"/>\n",
         "</g>\n",
         "<!-- 9 -->\n",
         "<g id=\"node12\" class=\"node\"><title>9</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1506.73\" cy=\"-18\" rx=\"83.3857\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1479.03\" cy=\"-18\" rx=\"81.7856\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1479.03\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1 * 1</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;9 -->\n",
         "<g id=\"edge11\" class=\"edge\"><title>7&#45;&gt;9</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1223.24,-51.2056C1235.89,-48.986 1249.12,-46.7999 1261.54,-45 1315.04,-37.2455 1375.42,-30.5512 1422.76,-25.7681\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1429.94,-25.0468 1423.29,-28.8805 1426.46,-25.3965 1422.98,-25.7463 1422.98,-25.7463 1422.98,-25.7463 1426.46,-25.3965 1422.66,-22.612 1429.94,-25.0468 1429.94,-25.0468\"/>\n",
-        "<text text-anchor=\"start\" x=\"1261.54\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1201.34,-51.2154C1213.82,-48.995 1226.88,-46.8062 1239.14,-45 1291.38,-37.303 1350.33,-30.6198 1396.6,-25.828\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1403.62,-25.1051 1396.98,-28.9554 1400.14,-25.4636 1396.65,-25.822 1396.65,-25.822 1396.65,-25.822 1400.14,-25.4636 1396.33,-22.6885 1403.62,-25.1051 1403.62,-25.1051\"/>\n",
+        "<text text-anchor=\"start\" x=\"1239.14\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 8&#45;&gt;8 -->\n",
         "<g id=\"edge12\" class=\"edge\"><title>8&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1476.26,-134.037C1470.04,-143.858 1480.19,-153 1506.73,-153 1526.64,-153 1537.33,-147.858 1538.81,-141.143\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1537.21,-134.037 1541.82,-140.178 1537.98,-137.452 1538.74,-140.868 1538.74,-140.868 1538.74,-140.868 1537.98,-137.452 1535.67,-141.557 1537.21,-134.037 1537.21,-134.037\"/>\n",
-        "<text text-anchor=\"start\" x=\"1438.73\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
-        "<text text-anchor=\"start\" x=\"1498.73\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1449.26,-134.037C1443.19,-143.858 1453.11,-153 1479.03,-153 1498.48,-153 1508.92,-147.858 1510.36,-141.143\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1508.8,-134.037 1513.38,-140.201 1509.55,-137.456 1510.3,-140.875 1510.3,-140.875 1510.3,-140.875 1509.55,-137.456 1507.23,-141.549 1508.8,-134.037 1508.8,-134.037\"/>\n",
+        "<text text-anchor=\"start\" x=\"1412.53\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "<text text-anchor=\"start\" x=\"1471.03\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f426c309600> >"
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x109e19e70> >"
        ]
       }
      ],
-     "prompt_number": 11
+     "prompt_number": 14
     },
     {
      "cell_type": "code",
@@ -1267,7 +1350,23 @@
      "language": "python",
      "metadata": {},
      "outputs": [],
-     "prompt_number": 12
+     "prompt_number": 15
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Note that using %%dve does not require any deletion."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": true,
+     "input": [],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": null
     }
    ],
    "metadata": {}