ltsmin-dve.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import spot\n",
    "import spot.ltsmin\n",
    "# The following line causes the notebook to exit with 77 if divine is not \n",
    "# installed, therefore skipping this test in the test suite.\n",
    "spot.ltsmin.require('divine')\n",
    "# This notebook also tests the limitation of the number of states in the GraphViz output\n",
    "spot.setup(max_states=10)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are two ways to load a DiVinE model: from a file or from a cell.   \n",
    "\n",
    "Loading from a file\n",
    "-------------------\n",
    "\n",
    "We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "!rm -f test1.dve"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Writing test1.dve\n"
     ]
    }
   ],
   "source": [
    "%%file test1.dve\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;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `spot.ltsmin.load` function compiles the model using the `ltlmin` interface and load it.  This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "m = spot.ltsmin.load('test1.dve')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Compiling the model creates all several kinds of files.  The `test1.dve` file is converted into a C++ source code `test1.dve.cpp` which is then compiled into a shared library `test1.dve2c`.  Becauce `spot.ltsmin.load()` has already loaded this shared library, all those files can be erased.  If you do not erase the files, `spot.ltsmin.load()` will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.\n",
    "\n",
    "For editing and loading DVE file from a notebook, it is a better to use the `%%dve` as shown next."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "!rm -f test1.dve test1.dve.cpp test1.dve2C"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Loading from a notebook cell\n",
    "----------------------------\n",
    "\n",
    "The `%%dve` cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files).  The variable name that should receive the model (here `m`) should be indicated on the first line, after `%dve`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%dve m\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;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Working with an ltsmin model\n",
    "----------------------------\n",
    "\n",
    "Printing an ltsmin model shows some information about the variables it contains and their types, however the `info()` methods provide the data in a map that is easier to work with."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "ltsmin model with the following variables:\n",
       "  a: int\n",
       "  b: int\n",
       "  P: ['x']\n",
       "  Q: ['wait', 'work']"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[('state_size', 4),\n",
       " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
       " ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sorted(m.info().items())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To obtain a Kripke structure, call `kripke` and supply a list of atomic propositions to observe in the model."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"734pt\" height=\"242pt\"\n",
       " viewBox=\"0.00 0.00 734.00 242.46\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.6487 .6487) rotate(0) translate(4 369.7401)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-369.7401 1127.4104,-369.7401 1127.4104,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"558.7052\" y=\"-350.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">t</text>\n",
       "<text text-anchor=\"start\" x=\"550.7052\" y=\"-335.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"150.1371\" cy=\"-154.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"105.1371\" y=\"-158.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"78.1371\" y=\"-143.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&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\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1671,-154.8701C3.9097,-154.8701 14.8741,-154.8701 29.7057,-154.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"36.7767,-154.8701 29.7767,-158.0202 33.2767,-154.8701 29.7767,-154.8702 29.7767,-154.8702 29.7767,-154.8702 33.2767,-154.8701 29.7766,-151.7202 36.7767,-154.8701 36.7767,-154.8701\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"415.2397\" cy=\"-190.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"370.2397\" y=\"-194.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"341.2397\" y=\"-179.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&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\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M248.4748,-168.224C267.7667,-170.8437 288.0966,-173.6045 307.6721,-176.2628\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"314.8467,-177.237 307.4865,-179.4164 311.3786,-176.766 307.9104,-176.295 307.9104,-176.295 307.9104,-176.295 311.3786,-176.766 308.3343,-173.1737 314.8467,-177.237 314.8467,-177.237\"/>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"415.2397\" cy=\"-118.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"370.2397\" y=\"-122.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"343.2397\" y=\"-107.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&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\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M248.4748,-141.5161C268.3786,-138.8133 289.3872,-135.9604 309.5324,-133.2247\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"316.6187,-132.2624 310.1063,-136.3258 313.1506,-132.7334 309.6824,-133.2045 309.6824,-133.2045 309.6824,-133.2045 313.1506,-132.7334 309.2585,-130.0831 316.6187,-132.2624 316.6187,-132.2624\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-226.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-230.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=2, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"609.1707\" y=\"-215.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&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\">\n",
       "<title>1&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M515.7696,-204.3776C535.2954,-207.0011 555.8335,-209.7607 575.576,-212.4133\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5231,-213.3467 575.1659,-215.5364 579.0543,-212.8806 575.5854,-212.4145 575.5854,-212.4145 575.5854,-212.4145 579.0543,-212.8806 576.0049,-209.2926 582.5231,-213.3467 582.5231,-213.3467\"/>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-154.8701\" rx=\"115.931\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-158.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"609.1707\" y=\"-143.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&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\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M515.7696,-177.3626C535.2954,-174.739 555.8335,-171.9795 575.576,-169.3268\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5231,-168.3934 576.0049,-172.4476 579.0543,-168.8595 575.5854,-169.3256 575.5854,-169.3256 575.5854,-169.3256 579.0543,-168.8595 575.1659,-166.2037 582.5231,-168.3934 582.5231,-168.3934\"/>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M513.8659,-132.1218C533.8869,-134.8118 555.0421,-137.6543 575.3619,-140.3845\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"582.5112,-141.3451 575.154,-143.5348 579.0423,-140.879 575.5735,-140.4129 575.5735,-140.4129 575.5735,-140.4129 579.0423,-140.879 575.993,-137.291 582.5112,-141.3451 582.5112,-141.3451\"/>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>5</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"683.1707\" cy=\"-82.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"638.1707\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=2, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"611.1707\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&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\">\n",
       "<title>2&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M513.8659,-105.6184C534.5106,-102.8445 556.3611,-99.9086 577.2583,-97.1008\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"584.3054,-96.1539 577.7873,-100.2081 580.8366,-96.62 577.3678,-97.0861 577.3678,-97.0861 577.3678,-97.0861 580.8366,-96.62 576.9483,-93.9642 584.3054,-96.1539 584.3054,-96.1539\"/>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>6</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-282.8701\" rx=\"113.2743\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-286.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=3, b=0, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"876.2733\" y=\"-271.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!&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\">\n",
       "<title>3&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M768.8758,-244.9743C796.7674,-250.8661 827.8348,-257.4288 856.1739,-263.4151\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"863.3164,-264.9239 855.8165,-266.559 859.892,-264.2004 856.4676,-263.477 856.4676,-263.477 856.4676,-263.477 859.892,-264.2004 857.1186,-260.395 863.3164,-264.9239 863.3164,-264.9239\"/>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>7</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-210.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-214.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=2, b=1, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-199.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;7 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M795.5981,-220.0846C819.5378,-218.6398 844.3743,-217.1408 866.8851,-215.7822\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"874.108,-215.3462 867.3105,-218.9123 870.6144,-215.5571 867.1207,-215.768 867.1207,-215.768 867.1207,-215.768 870.6144,-215.5571 866.9309,-212.6238 874.108,-215.3462 874.108,-215.3462\"/>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>4&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M768.8758,-172.9743C803.6186,-180.3133 843.289,-188.6933 876.4758,-195.7036\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.455,-197.1779 875.9551,-198.8131 880.0306,-196.4545 876.6062,-195.7311 876.6062,-195.7311 876.6062,-195.7311 880.0306,-196.4545 877.2572,-192.6491 883.455,-197.1779 883.455,-197.1779\"/>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>8</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-138.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-142.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=2, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-127.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;8 -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>4&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M795.5981,-148.0846C819.5378,-146.6398 844.3743,-145.1408 866.8851,-143.7822\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"874.108,-143.3462 867.3105,-146.9123 870.6144,-143.5571 867.1207,-143.768 867.1207,-143.768 867.1207,-143.768 870.6144,-143.5571 866.9309,-140.6238 874.108,-143.3462 874.108,-143.3462\"/>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>5&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M767.7797,-100.7428C802.7225,-108.1241 842.8025,-116.5905 876.3042,-123.6674\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.349,-125.1555 875.8491,-126.7907 879.9246,-124.4321 876.5001,-123.7087 876.5001,-123.7087 876.5001,-123.7087 879.9246,-124.4321 877.1512,-120.6267 883.349,-125.1555 883.349,-125.1555\"/>\n",
       "</g>\n",
       "<!-- u5 -->\n",
       "<g id=\"node11\" class=\"node\">\n",
       "<title>u5</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"961.2733,-94.3701 935.2733,-94.3701 935.2733,-71.3701 961.2733,-71.3701 961.2733,-94.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"948.2733\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;u5 -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>5&#45;&gt;u5</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M796.367,-82.8701C846.0208,-82.8701 899.3777,-82.8701 927.7542,-82.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"935.0716,-82.8701 928.0716,-86.0202 931.5716,-82.8701 928.0716,-82.8702 928.0716,-82.8702 928.0716,-82.8702 931.5716,-82.8701 928.0715,-79.7202 935.0716,-82.8701 935.0716,-82.8701\"/>\n",
       "</g>\n",
       "<!-- 9 -->\n",
       "<g id=\"node12\" class=\"node\">\n",
       "<title>9</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"948.2733\" cy=\"-26.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
       "<text text-anchor=\"start\" x=\"903.2733\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=3, Q=0</text>\n",
       "<text text-anchor=\"start\" x=\"943.2733\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>5&#45;&gt;9</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M767.7797,-64.9973C802.7225,-57.6161 842.8025,-49.1496 876.3042,-42.0727\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"883.349,-40.5846 877.1512,-45.1134 879.9246,-41.308 876.5001,-42.0314 876.5001,-42.0314 876.5001,-42.0314 879.9246,-41.308 875.8491,-38.9494 883.349,-40.5846 883.349,-40.5846\"/>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>6&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M918.017,-309.1406C916.6722,-319.2978 926.7577,-327.7401 948.2733,-327.7401 964.41,-327.7401 974.1173,-322.9913 977.395,-316.3318\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"978.5297,-309.1406 980.5501,-316.546 977.9841,-312.5978 977.4386,-316.055 977.4386,-316.055 977.4386,-316.055 977.9841,-312.5978 974.3271,-315.5641 978.5297,-309.1406 978.5297,-309.1406\"/>\n",
       "</g>\n",
       "<!-- u7 -->\n",
       "<g id=\"node13\" class=\"node\">\n",
       "<title>u7</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-222.3701 1097.4104,-222.3701 1097.4104,-199.3701 1123.4104,-199.3701 1123.4104,-222.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-207.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;u7 -->\n",
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>7&#45;&gt;u7</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-210.8701C1048.0287,-210.8701 1073.1021,-210.8701 1089.9848,-210.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-210.8701 1090.1335,-214.0202 1093.6334,-210.8701 1090.1334,-210.8702 1090.1334,-210.8702 1090.1334,-210.8702 1093.6334,-210.8701 1090.1334,-207.7202 1097.1334,-210.8701 1097.1334,-210.8701\"/>\n",
       "</g>\n",
       "<!-- u8 -->\n",
       "<g id=\"node14\" class=\"node\">\n",
       "<title>u8</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-150.3701 1097.4104,-150.3701 1097.4104,-127.3701 1123.4104,-127.3701 1123.4104,-150.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-135.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;u8 -->\n",
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>8&#45;&gt;u8</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-138.8701C1048.0287,-138.8701 1073.1021,-138.8701 1089.9848,-138.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-138.8701 1090.1335,-142.0202 1093.6334,-138.8701 1090.1334,-138.8702 1090.1334,-138.8702 1090.1334,-138.8702 1093.6334,-138.8701 1090.1334,-135.7202 1097.1334,-138.8701 1097.1334,-138.8701\"/>\n",
       "</g>\n",
       "<!-- u9 -->\n",
       "<g id=\"node15\" class=\"node\">\n",
       "<title>u9</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1123.4104,-38.3701 1097.4104,-38.3701 1097.4104,-15.3701 1123.4104,-15.3701 1123.4104,-38.3701\"/>\n",
       "<text text-anchor=\"middle\" x=\"1110.4104\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;u9 -->\n",
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>9&#45;&gt;u9</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1023.6459,-26.8701C1048.0287,-26.8701 1073.1021,-26.8701 1089.9848,-26.8701\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1097.1334,-26.8701 1090.1335,-30.0202 1093.6334,-26.8701 1090.1334,-26.8702 1090.1334,-26.8702 1090.1334,-26.8702 1093.6334,-26.8701 1090.1334,-23.7202 1097.1334,-26.8701 1097.1334,-26.8701\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fb8f84f9870> >"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k = m.kripke([\"a<1\", \"b>2\"])\n",
    "k"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<svg height=\"219pt\" viewBox=\"0.00 0.00 734.00 219.12\" 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(.5245 .5245) rotate(0) translate(4 413.7401)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-413.7401 1395.3414,-413.7401 1395.3414,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"692.6707\" y=\"-394.5401\">t</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"684.6707\" y=\"-379.5401\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"150.1371\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"105.1371\" y=\"-186.6701\">a=0, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.1371\" y=\"-171.6701\">&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\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.1671,-182.8701C3.9097,-182.8701 14.8741,-182.8701 29.7057,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"36.7767,-182.8701 29.7767,-186.0202 33.2767,-182.8701 29.7767,-182.8702 29.7767,-182.8702 29.7767,-182.8702 33.2767,-182.8701 29.7766,-179.7202 36.7767,-182.8701 36.7767,-182.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g class=\"node\" id=\"node3\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-218.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-222.6701\">a=1, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341.2397\" y=\"-207.6701\">!&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\">\n",
       "<title>0-&gt;1</title>\n",
       "<path d=\"M248.4748,-196.224C267.7667,-198.8437 288.0966,-201.6045 307.6721,-204.2628\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"314.8467,-205.237 307.4865,-207.4164 311.3786,-204.766 307.9104,-204.295 307.9104,-204.295 307.9104,-204.295 311.3786,-204.766 308.3343,-201.1737 314.8467,-205.237 314.8467,-205.237\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g class=\"node\" id=\"node4\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-146.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-150.6701\">a=0, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343.2397\" y=\"-135.6701\">&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\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M248.4748,-169.5161C268.3786,-166.8133 289.3872,-163.9604 309.5324,-161.2247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"316.6187,-160.2624 310.1063,-164.3258 313.1506,-160.7334 309.6824,-161.2045 309.6824,-161.2045 309.6824,-161.2045 313.1506,-160.7334 309.2585,-158.0831 316.6187,-160.2624 316.6187,-160.2624\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g class=\"node\" id=\"node5\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-258.6701\">a=2, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-243.6701\">!&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\">\n",
       "<title>1-&gt;3</title>\n",
       "<path d=\"M515.7696,-232.3776C535.2954,-235.0011 555.8335,-237.7607 575.576,-240.4133\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-241.3467 575.1659,-243.5364 579.0543,-240.8806 575.5854,-240.4145 575.5854,-240.4145 575.5854,-240.4145 579.0543,-240.8806 576.0049,-237.2926 582.5231,-241.3467 582.5231,-241.3467\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g class=\"node\" id=\"node6\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-186.6701\">a=1, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-171.6701\">!&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\">\n",
       "<title>1-&gt;4</title>\n",
       "<path d=\"M515.7696,-205.3626C535.2954,-202.739 555.8335,-199.9795 575.576,-197.3268\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-196.3934 576.0049,-200.4476 579.0543,-196.8595 575.5854,-197.3256 575.5854,-197.3256 575.5854,-197.3256 579.0543,-196.8595 575.1659,-194.2037 582.5231,-196.3934 582.5231,-196.3934\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;4</title>\n",
       "<path d=\"M513.8659,-160.1218C533.8869,-162.8118 555.0421,-165.6543 575.3619,-168.3845\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5112,-169.3451 575.154,-171.5348 579.0423,-168.879 575.5735,-168.4129 575.5735,-168.4129 575.5735,-168.4129 579.0423,-168.879 575.993,-165.291 582.5112,-169.3451 582.5112,-169.3451\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g class=\"node\" id=\"node7\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-114.6701\">a=0, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"611.1707\" y=\"-99.6701\">&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\">\n",
       "<title>2-&gt;5</title>\n",
       "<path d=\"M513.8659,-133.6184C534.5106,-130.8445 556.3611,-127.9086 577.2583,-125.1008\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"584.3054,-124.1539 577.7873,-128.2081 580.8366,-124.62 577.3678,-125.0861 577.3678,-125.0861 577.3678,-125.0861 580.8366,-124.62 576.9483,-121.9642 584.3054,-124.1539 584.3054,-124.1539\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g class=\"node\" id=\"node8\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-326.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-330.6701\">a=3, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-315.6701\">!&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\">\n",
       "<title>3-&gt;6</title>\n",
       "<path d=\"M759.2323,-275.3098C793.4622,-284.5082 833.9374,-295.385 868.8685,-304.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.7773,-306.6284 868.1996,-307.8538 872.3972,-305.7201 869.0171,-304.8117 869.0171,-304.8117 869.0171,-304.8117 872.3972,-305.7201 869.8346,-301.7697 875.7773,-306.6284 875.7773,-306.6284\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g class=\"node\" id=\"node9\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-258.6701\">a=2, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-243.6701\">!&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\">\n",
       "<title>3-&gt;7</title>\n",
       "<path d=\"M799.5202,-254.8701C808.8609,-254.8701 818.3179,-254.8701 827.7052,-254.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-254.8701 827.8671,-258.0202 831.3671,-254.8701 827.8671,-254.8702 827.8671,-254.8702 827.8671,-254.8702 831.3671,-254.8701 827.867,-251.7202 834.8671,-254.8701 834.8671,-254.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>4-&gt;7</title>\n",
       "<path d=\"M759.2323,-203.3098C793.3171,-212.4693 833.5945,-223.2928 868.4242,-232.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.314,-234.5039 867.7363,-235.7293 871.9339,-233.5956 868.5538,-232.6872 868.5538,-232.6872 868.5538,-232.6872 871.9339,-233.5956 869.3714,-229.6452 875.314,-234.5039 875.314,-234.5039\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g class=\"node\" id=\"node10\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-186.6701\">a=1, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-171.6701\">!&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\">\n",
       "<title>4-&gt;8</title>\n",
       "<path d=\"M799.5202,-182.8701C808.8609,-182.8701 818.3179,-182.8701 827.7052,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-182.8701 827.8671,-186.0202 831.3671,-182.8701 827.8671,-182.8702 827.8671,-182.8702 827.8671,-182.8702 831.3671,-182.8701 827.867,-179.7202 834.8671,-182.8701 834.8671,-182.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>5-&gt;8</title>\n",
       "<path d=\"M758.1607,-131.0218C792.4127,-140.2262 833.0911,-151.1575 868.2457,-160.6045\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.1995,-162.4732 867.6218,-163.6985 871.8194,-161.5648 868.4393,-160.6564 868.4393,-160.6564 868.4393,-160.6564 871.8194,-161.5648 869.2568,-157.6144 875.1995,-162.4732 875.1995,-162.4732\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 9 -->\n",
       "<g class=\"node\" id=\"node11\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"946.1017\" y=\"-15.6701\">...</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;9 -->\n",
       "<g class=\"edge\" id=\"edge13\">\n",
       "<title>5-&gt;9</title>\n",
       "<path d=\"M751.8217,-89.3471C793.6799,-76.2239 846.8016,-59.5696 887.6708,-46.7565\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"894.3784,-44.6536 888.6413,-49.7535 891.0386,-45.7007 887.6989,-46.7478 887.6989,-46.7478 887.6989,-46.7478 891.0386,-45.7007 886.7565,-43.742 894.3784,-44.6536 894.3784,-44.6536\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 10 -->\n",
       "<g class=\"node\" id=\"node12\">\n",
       "<title>10</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-114.6701\">a=0, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-99.6701\">&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\">\n",
       "<title>5-&gt;10</title>\n",
       "<path d=\"M796.4092,-110.8701C807.7635,-110.8701 819.3214,-110.8701 830.7458,-110.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"837.8389,-110.8701 830.839,-114.0202 834.3389,-110.8701 830.8389,-110.8702 830.8389,-110.8702 830.8389,-110.8702 834.3389,-110.8701 830.8389,-107.7202 837.8389,-110.8701 837.8389,-110.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M902.3752,-351.3317C897.7345,-362.2753 913.9767,-371.7401 951.1017,-371.7401 979.5256,-371.7401 995.7083,-366.192 999.6499,-358.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"999.8283,-351.3317 1002.8073,-358.4061 999.7433,-354.8307 999.6583,-358.3296 999.6583,-358.3296 999.6583,-358.3296 999.7433,-354.8307 996.5092,-358.2531 999.8283,-351.3317 999.8283,-351.3317\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 11 -->\n",
       "<g class=\"node\" id=\"node13\">\n",
       "<title>11</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-326.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-330.6701\">a=3, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1144.2043\" y=\"-315.6701\">!&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\">\n",
       "<title>7-&gt;11</title>\n",
       "<path d=\"M1026.7147,-275.406C1060.4316,-284.5633 1100.2171,-295.3687 1134.6056,-304.7084\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.408,-306.5559 1133.827,-307.761 1138.0303,-305.6385 1134.6527,-304.7211 1134.6527,-304.7211 1134.6527,-304.7211 1138.0303,-305.6385 1135.4783,-301.6813 1141.408,-306.5559 1141.408,-306.5559\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 12 -->\n",
       "<g class=\"node\" id=\"node14\">\n",
       "<title>12</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-254.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-258.6701\">a=2, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-243.6701\">...</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;12 -->\n",
       "<g class=\"edge\" id=\"edge17\">\n",
       "<title>7-&gt;12</title>\n",
       "<path d=\"M1067.3796,-254.8701C1089.878,-254.8701 1113.0114,-254.8701 1134.1342,-254.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.2167,-254.8701 1134.2167,-258.0202 1137.7167,-254.8701 1134.2167,-254.8702 1134.2167,-254.8702 1134.2167,-254.8702 1137.7167,-254.8701 1134.2166,-251.7202 1141.2167,-254.8701 1141.2167,-254.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;12 -->\n",
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>8-&gt;12</title>\n",
       "<path d=\"M1026.7147,-203.406C1065.3265,-213.8927 1111.8969,-226.5409 1149.2066,-236.674\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1156.0614,-238.5357 1148.4805,-239.7408 1152.6837,-237.6183 1149.3061,-236.7009 1149.3061,-236.7009 1149.3061,-236.7009 1152.6837,-237.6183 1150.1317,-233.661 1156.0614,-238.5357 1156.0614,-238.5357\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 13 -->\n",
       "<g class=\"node\" id=\"node15\">\n",
       "<title>13</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-182.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-186.6701\">a=1, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-171.6701\">...</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;13 -->\n",
       "<g class=\"edge\" id=\"edge19\">\n",
       "<title>8-&gt;13</title>\n",
       "<path d=\"M1067.3796,-182.8701C1089.878,-182.8701 1113.0114,-182.8701 1134.1342,-182.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1141.2167,-182.8701 1134.2167,-186.0202 1137.7167,-182.8701 1134.2167,-182.8702 1134.2167,-182.8702 1134.2167,-182.8702 1137.7167,-182.8701 1134.2166,-179.7202 1141.2167,-182.8701 1141.2167,-182.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 14 -->\n",
       "<g class=\"node\" id=\"node16\">\n",
       "<title>14</title>\n",
       "<ellipse cx=\"1216.2043\" cy=\"-110.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1171.2043\" y=\"-114.6701\">a=1, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1211.2043\" y=\"-99.6701\">...</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;14 -->\n",
       "<g class=\"edge\" id=\"edge20\">\n",
       "<title>8-&gt;14</title>\n",
       "<path d=\"M1026.7147,-162.3341C1065.3265,-151.8474 1111.8969,-139.1992 1149.2066,-129.0662\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1156.0614,-127.2045 1150.1317,-132.0791 1152.6837,-128.1218 1149.3061,-129.0392 1149.3061,-129.0392 1149.3061,-129.0392 1152.6837,-128.1218 1148.4805,-125.9993 1156.0614,-127.2045 1156.0614,-127.2045\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- u9 -->\n",
       "<g class=\"node\" id=\"node17\">\n",
       "<title>u9</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1229.2043,-25.3701 1203.2043,-25.3701 1203.2043,-2.3701 1229.2043,-2.3701 1229.2043,-25.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2043\" y=\"-10.1701\">...</text>\n",
       "</g>\n",
       "<!-- 9&#45;&gt;u9 -->\n",
       "<g class=\"edge\" id=\"edge21\">\n",
       "<title>9-&gt;u9</title>\n",
       "<path d=\"M1025.6531,-23.2142C1083.7014,-20.3677 1160.2356,-16.6146 1196.0712,-14.8573\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1203.0791,-14.5137 1196.2418,-18.0029 1199.5833,-14.6852 1196.0875,-14.8566 1196.0875,-14.8566 1196.0875,-14.8566 1199.5833,-14.6852 1195.9331,-11.7104 1203.0791,-14.5137 1203.0791,-14.5137\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;14 -->\n",
       "<g class=\"edge\" id=\"edge23\">\n",
       "<title>10-&gt;14</title>\n",
       "<path d=\"M1064.2981,-110.8701C1087.6637,-110.8701 1111.8495,-110.8701 1133.8663,-110.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1140.9346,-110.8701 1133.9347,-114.0202 1137.4346,-110.8701 1133.9346,-110.8702 1133.9346,-110.8702 1133.9346,-110.8702 1137.4346,-110.8701 1133.9346,-107.7202 1140.9346,-110.8701 1140.9346,-110.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- u10 -->\n",
       "<g class=\"node\" id=\"node18\">\n",
       "<title>u10</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1229.2043,-66.3701 1203.2043,-66.3701 1203.2043,-43.3701 1229.2043,-43.3701 1229.2043,-66.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1216.2043\" y=\"-51.1701\">...</text>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;u10 -->\n",
       "<g class=\"edge\" id=\"edge22\">\n",
       "<title>10-&gt;u10</title>\n",
       "<path d=\"M1029.3911,-91.4126C1053.0061,-85.7898 1079.0376,-79.8359 1103.0672,-74.8701 1135.3588,-68.1968 1173.1233,-61.8022 1195.8271,-58.109\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1202.9195,-56.9636 1196.5113,-61.1894 1199.4643,-57.5217 1196.0091,-58.0797 1196.0091,-58.0797 1196.0091,-58.0797 1199.4643,-57.5217 1195.5068,-54.97 1202.9195,-56.9636 1202.9195,-56.9636\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 11&#45;&gt;11 -->\n",
       "<g class=\"edge\" id=\"edge24\">\n",
       "<title>11-&gt;11</title>\n",
       "<path d=\"M1185.948,-353.1406C1184.6033,-363.2978 1194.6887,-371.7401 1216.2043,-371.7401 1232.341,-371.7401 1242.0483,-366.9913 1245.3261,-360.3318\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1246.4607,-353.1406 1248.4812,-360.546 1245.9152,-356.5978 1245.3697,-360.055 1245.3697,-360.055 1245.3697,-360.055 1245.9152,-356.5978 1242.2581,-359.5641 1246.4607,-353.1406 1246.4607,-353.1406\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- u12 -->\n",
       "<g class=\"node\" id=\"node19\">\n",
       "<title>u12</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-266.3701 1365.3414,-266.3701 1365.3414,-243.3701 1391.3414,-243.3701 1391.3414,-266.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-251.1701\">...</text>\n",
       "</g>\n",
       "<!-- 12&#45;&gt;u12 -->\n",
       "<g class=\"edge\" id=\"edge25\">\n",
       "<title>12-&gt;u12</title>\n",
       "<path d=\"M1291.5769,-254.8701C1315.9597,-254.8701 1341.0331,-254.8701 1357.9158,-254.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-254.8701 1358.0645,-258.0202 1361.5645,-254.8701 1358.0645,-254.8702 1358.0645,-254.8702 1358.0645,-254.8702 1361.5645,-254.8701 1358.0644,-251.7202 1365.0645,-254.8701 1365.0645,-254.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- u13 -->\n",
       "<g class=\"node\" id=\"node20\">\n",
       "<title>u13</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-194.3701 1365.3414,-194.3701 1365.3414,-171.3701 1391.3414,-171.3701 1391.3414,-194.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-179.1701\">...</text>\n",
       "</g>\n",
       "<!-- 13&#45;&gt;u13 -->\n",
       "<g class=\"edge\" id=\"edge26\">\n",
       "<title>13-&gt;u13</title>\n",
       "<path d=\"M1291.5769,-182.8701C1315.9597,-182.8701 1341.0331,-182.8701 1357.9158,-182.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-182.8701 1358.0645,-186.0202 1361.5645,-182.8701 1358.0645,-182.8702 1358.0645,-182.8702 1358.0645,-182.8702 1361.5645,-182.8701 1358.0644,-179.7202 1365.0645,-182.8701 1365.0645,-182.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- u14 -->\n",
       "<g class=\"node\" id=\"node21\">\n",
       "<title>u14</title>\n",
       "<polygon fill=\"#ffffaa\" points=\"1391.3414,-122.3701 1365.3414,-122.3701 1365.3414,-99.3701 1391.3414,-99.3701 1391.3414,-122.3701\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1378.3414\" y=\"-107.1701\">...</text>\n",
       "</g>\n",
       "<!-- 14&#45;&gt;u14 -->\n",
       "<g class=\"edge\" id=\"edge27\">\n",
       "<title>14-&gt;u14</title>\n",
       "<path d=\"M1291.5769,-110.8701C1315.9597,-110.8701 1341.0331,-110.8701 1357.9158,-110.8701\" fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\"/>\n",
       "<polygon fill=\"#000000\" points=\"1365.0645,-110.8701 1358.0645,-114.0202 1361.5645,-110.8701 1358.0645,-110.8702 1358.0645,-110.8702 1358.0645,-110.8702 1361.5645,-110.8701 1358.0644,-107.7202 1365.0645,-110.8701 1365.0645,-110.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k.show('.<15')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<svg height=\"166pt\" viewBox=\"0.00 0.00 734.00 165.54\" 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(.3907 .3907) rotate(0) translate(4 419.7401)\">\n",
       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-419.7401 1874.8603,-419.7401 1874.8603,4 -4,4\" stroke=\"transparent\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"932.4302\" y=\"-400.5401\">t</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"924.4302\" y=\"-385.5401\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g class=\"node\" id=\"node2\">\n",
       "<title>0</title>\n",
       "<ellipse cx=\"150.1371\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"105.1371\" y=\"-192.6701\">a=0, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.1371\" y=\"-177.6701\">&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\">\n",
       "<title>I-&gt;0</title>\n",
       "<path d=\"M1.1671,-188.8701C3.9097,-188.8701 14.8741,-188.8701 29.7057,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"36.7767,-188.8701 29.7767,-192.0202 33.2767,-188.8701 29.7767,-188.8702 29.7767,-188.8702 29.7767,-188.8702 33.2767,-188.8701 29.7766,-185.7202 36.7767,-188.8701 36.7767,-188.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g class=\"node\" id=\"node3\">\n",
       "<title>1</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-224.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-228.6701\">a=1, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341.2397\" y=\"-213.6701\">!&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\">\n",
       "<title>0-&gt;1</title>\n",
       "<path d=\"M248.4748,-202.224C267.7667,-204.8437 288.0966,-207.6045 307.6721,-210.2628\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"314.8467,-211.237 307.4865,-213.4164 311.3786,-210.766 307.9104,-210.295 307.9104,-210.295 307.9104,-210.295 311.3786,-210.766 308.3343,-207.1737 314.8467,-211.237 314.8467,-211.237\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g class=\"node\" id=\"node4\">\n",
       "<title>2</title>\n",
       "<ellipse cx=\"415.2397\" cy=\"-152.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.2397\" y=\"-156.6701\">a=0, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343.2397\" y=\"-141.6701\">&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\">\n",
       "<title>0-&gt;2</title>\n",
       "<path d=\"M248.4748,-175.5161C268.3786,-172.8133 289.3872,-169.9604 309.5324,-167.2247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"316.6187,-166.2624 310.1063,-170.3258 313.1506,-166.7334 309.6824,-167.2045 309.6824,-167.2045 309.6824,-167.2045 313.1506,-166.7334 309.2585,-164.0831 316.6187,-166.2624 316.6187,-166.2624\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g class=\"node\" id=\"node5\">\n",
       "<title>3</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-264.6701\">a=2, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-249.6701\">!&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\">\n",
       "<title>1-&gt;3</title>\n",
       "<path d=\"M515.7696,-238.3776C535.2954,-241.0011 555.8335,-243.7607 575.576,-246.4133\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-247.3467 575.1659,-249.5364 579.0543,-246.8806 575.5854,-246.4145 575.5854,-246.4145 575.5854,-246.4145 579.0543,-246.8806 576.0049,-243.2926 582.5231,-247.3467 582.5231,-247.3467\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g class=\"node\" id=\"node6\">\n",
       "<title>4</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-192.6701\">a=1, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"609.1707\" y=\"-177.6701\">!&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\">\n",
       "<title>1-&gt;4</title>\n",
       "<path d=\"M515.7696,-211.3626C535.2954,-208.739 555.8335,-205.9795 575.576,-203.3268\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5231,-202.3934 576.0049,-206.4476 579.0543,-202.8595 575.5854,-203.3256 575.5854,-203.3256 575.5854,-203.3256 579.0543,-202.8595 575.1659,-200.2037 582.5231,-202.3934 582.5231,-202.3934\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g class=\"edge\" id=\"edge6\">\n",
       "<title>2-&gt;4</title>\n",
       "<path d=\"M513.8659,-166.1218C533.8869,-168.8118 555.0421,-171.6543 575.3619,-174.3845\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"582.5112,-175.3451 575.154,-177.5348 579.0423,-174.879 575.5735,-174.4129 575.5735,-174.4129 575.5735,-174.4129 579.0423,-174.879 575.993,-171.291 582.5112,-175.3451 582.5112,-175.3451\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g class=\"node\" id=\"node7\">\n",
       "<title>5</title>\n",
       "<ellipse cx=\"683.1707\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"638.1707\" y=\"-120.6701\">a=0, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"611.1707\" y=\"-105.6701\">&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\">\n",
       "<title>2-&gt;5</title>\n",
       "<path d=\"M513.8659,-139.6184C534.5106,-136.8445 556.3611,-133.9086 577.2583,-131.1008\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"584.3054,-130.1539 577.7873,-134.2081 580.8366,-130.62 577.3678,-131.0861 577.3678,-131.0861 577.3678,-131.0861 580.8366,-130.62 576.9483,-127.9642 584.3054,-130.1539 584.3054,-130.1539\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g class=\"node\" id=\"node8\">\n",
       "<title>6</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-336.6701\">a=3, b=0, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-321.6701\">!&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\">\n",
       "<title>3-&gt;6</title>\n",
       "<path d=\"M759.2323,-281.3098C793.4622,-290.5082 833.9374,-301.385 868.8685,-310.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.7773,-312.6284 868.1996,-313.8538 872.3972,-311.7201 869.0171,-310.8117 869.0171,-310.8117 869.0171,-310.8117 872.3972,-311.7201 869.8346,-307.7697 875.7773,-312.6284 875.7773,-312.6284\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g class=\"node\" id=\"node9\">\n",
       "<title>7</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-264.6701\">a=2, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-249.6701\">!&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\">\n",
       "<title>3-&gt;7</title>\n",
       "<path d=\"M799.5202,-260.8701C808.8609,-260.8701 818.3179,-260.8701 827.7052,-260.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-260.8701 827.8671,-264.0202 831.3671,-260.8701 827.8671,-260.8702 827.8671,-260.8702 827.8671,-260.8702 831.3671,-260.8701 827.867,-257.7202 834.8671,-260.8701 834.8671,-260.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;7 -->\n",
       "<g class=\"edge\" id=\"edge10\">\n",
       "<title>4-&gt;7</title>\n",
       "<path d=\"M759.2323,-209.3098C793.3171,-218.4693 833.5945,-229.2928 868.4242,-238.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.314,-240.5039 867.7363,-241.7293 871.9339,-239.5956 868.5538,-238.6872 868.5538,-238.6872 868.5538,-238.6872 871.9339,-239.5956 869.3714,-235.6452 875.314,-240.5039 875.314,-240.5039\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g class=\"node\" id=\"node10\">\n",
       "<title>8</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-192.6701\">a=1, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"877.1017\" y=\"-177.6701\">!&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\">\n",
       "<title>4-&gt;8</title>\n",
       "<path d=\"M799.5202,-188.8701C808.8609,-188.8701 818.3179,-188.8701 827.7052,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"834.8671,-188.8701 827.8671,-192.0202 831.3671,-188.8701 827.8671,-188.8702 827.8671,-188.8702 827.8671,-188.8702 831.3671,-188.8701 827.867,-185.7202 834.8671,-188.8701 834.8671,-188.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;8 -->\n",
       "<g class=\"edge\" id=\"edge12\">\n",
       "<title>5-&gt;8</title>\n",
       "<path d=\"M758.1607,-137.0218C792.4127,-146.2262 833.0911,-157.1575 868.2457,-166.6045\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"875.1995,-168.4732 867.6218,-169.6985 871.8194,-167.5648 868.4393,-166.6564 868.4393,-166.6564 868.4393,-166.6564 871.8194,-167.5648 869.2568,-163.6144 875.1995,-168.4732 875.1995,-168.4732\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 9 -->\n",
       "<g class=\"node\" id=\"node11\">\n",
       "<title>9</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-35.8701\" fill=\"#ffffaa\" rx=\"110.1176\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-39.6701\">a=0, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"881.1017\" 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\">\n",
       "<title>5-&gt;9</title>\n",
       "<path d=\"M753.2165,-95.6941C790.4375,-84.4415 836.2572,-70.5895 874.4299,-59.0492\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"881.4648,-56.9225 875.6759,-61.9634 878.1145,-57.9353 874.7643,-58.9482 874.7643,-58.9482 874.7643,-58.9482 878.1145,-57.9353 873.8527,-55.933 881.4648,-56.9225 881.4648,-56.9225\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 10 -->\n",
       "<g class=\"node\" id=\"node12\">\n",
       "<title>10</title>\n",
       "<ellipse cx=\"951.1017\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"906.1017\" y=\"-120.6701\">a=0, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"879.1017\" y=\"-105.6701\">&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\">\n",
       "<title>5-&gt;10</title>\n",
       "<path d=\"M796.4092,-116.8701C807.7635,-116.8701 819.3214,-116.8701 830.7458,-116.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"837.8389,-116.8701 830.839,-120.0202 834.3389,-116.8701 830.8389,-116.8702 830.8389,-116.8702 830.8389,-116.8702 834.3389,-116.8701 830.8389,-113.7202 837.8389,-116.8701 837.8389,-116.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g class=\"edge\" id=\"edge15\">\n",
       "<title>6-&gt;6</title>\n",
       "<path d=\"M902.006,-357.3317C897.3302,-368.2753 913.6955,-377.7401 951.1017,-377.7401 979.7409,-377.7401 996.0462,-372.192 1000.0176,-364.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1000.1974,-357.3317 1003.1752,-364.4067 1000.1118,-360.8306 1000.0261,-364.3296 1000.0261,-364.3296 1000.0261,-364.3296 1000.1118,-360.8306 996.8771,-364.2525 1000.1974,-357.3317 1000.1974,-357.3317\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 11 -->\n",
       "<g class=\"node\" id=\"node13\">\n",
       "<title>11</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-336.6701\">a=3, b=1, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1147.0328\" y=\"-321.6701\">!&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\">\n",
       "<title>7-&gt;11</title>\n",
       "<path d=\"M1027.1633,-281.3098C1061.3932,-290.5082 1101.8684,-301.385 1136.7995,-310.7719\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.7083,-312.6284 1136.1306,-313.8538 1140.3282,-311.7201 1136.9482,-310.8117 1136.9482,-310.8117 1136.9482,-310.8117 1140.3282,-311.7201 1137.7657,-307.7697 1143.7083,-312.6284 1143.7083,-312.6284\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 12 -->\n",
       "<g class=\"node\" id=\"node14\">\n",
       "<title>12</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-264.6701\">a=2, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1145.0328\" y=\"-249.6701\">!&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\">\n",
       "<title>7-&gt;12</title>\n",
       "<path d=\"M1067.4513,-260.8701C1076.7919,-260.8701 1086.2489,-260.8701 1095.6362,-260.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1102.7981,-260.8701 1095.7981,-264.0202 1099.2981,-260.8701 1095.7981,-260.8702 1095.7981,-260.8702 1095.7981,-260.8702 1099.2981,-260.8701 1095.798,-257.7202 1102.7981,-260.8701 1102.7981,-260.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;12 -->\n",
       "<g class=\"edge\" id=\"edge18\">\n",
       "<title>8-&gt;12</title>\n",
       "<path d=\"M1027.1633,-209.3098C1061.2481,-218.4693 1101.5255,-229.2928 1136.3552,-238.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.245,-240.5039 1135.6673,-241.7293 1139.8649,-239.5956 1136.4849,-238.6872 1136.4849,-238.6872 1136.4849,-238.6872 1139.8649,-239.5956 1137.3024,-235.6452 1143.245,-240.5039 1143.245,-240.5039\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 13 -->\n",
       "<g class=\"node\" id=\"node15\">\n",
       "<title>13</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-192.6701\">a=1, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1147.0328\" y=\"-177.6701\">!&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\">\n",
       "<title>8-&gt;13</title>\n",
       "<path d=\"M1067.4513,-188.8701C1077.7783,-188.8701 1088.2475,-188.8701 1098.6075,-188.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1105.7593,-188.8701 1098.7594,-192.0202 1102.2593,-188.8701 1098.7593,-188.8702 1098.7593,-188.8702 1098.7593,-188.8702 1102.2593,-188.8701 1098.7593,-185.7202 1105.7593,-188.8701 1105.7593,-188.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 14 -->\n",
       "<g class=\"node\" id=\"node16\">\n",
       "<title>14</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-116.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-120.6701\">a=1, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1145.0328\" y=\"-105.6701\">!&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\">\n",
       "<title>8-&gt;14</title>\n",
       "<path d=\"M1027.1633,-168.4303C1061.2481,-159.2709 1101.5255,-148.4473 1136.3552,-139.0877\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1143.245,-137.2362 1137.3024,-142.095 1139.8649,-138.1445 1136.4849,-139.0529 1136.4849,-139.0529 1136.4849,-139.0529 1139.8649,-138.1445 1135.6673,-136.0108 1143.245,-137.2362 1143.245,-137.2362\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 15 -->\n",
       "<g class=\"node\" id=\"node17\">\n",
       "<title>15</title>\n",
       "<ellipse cx=\"1219.0328\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"107.4605\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1174.0328\" y=\"-30.6701\">a=0, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1151.0328\" 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\">\n",
       "<title>9-&gt;15</title>\n",
       "<path d=\"M1060.466,-32.1964C1075.1393,-31.7035 1090.2205,-31.197 1104.9723,-30.7014\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1112.1844,-30.4592 1105.2941,-33.8425 1108.6864,-30.5767 1105.1883,-30.6943 1105.1883,-30.6943 1105.1883,-30.6943 1108.6864,-30.5767 1105.0825,-27.546 1112.1844,-30.4592 1112.1844,-30.4592\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;14 -->\n",
       "<g class=\"edge\" id=\"edge22\">\n",
       "<title>10-&gt;14</title>\n",
       "<path d=\"M1064.3403,-116.8701C1074.668,-116.8701 1085.1642,-116.8701 1095.5752,-116.8701\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1102.7661,-116.8701 1095.7662,-120.0202 1099.2661,-116.8701 1095.7661,-116.8702 1095.7661,-116.8702 1095.7661,-116.8702 1099.2661,-116.8701 1095.7661,-113.7202 1102.7661,-116.8701 1102.7661,-116.8701\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 10&#45;&gt;15 -->\n",
       "<g class=\"edge\" id=\"edge23\">\n",
       "<title>10-&gt;15</title>\n",
       "<path d=\"M1016.645,-94.8536C1056.4152,-81.4945 1107.1826,-64.4413 1147.9219,-50.7567\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1154.6289,-48.5038 1148.9963,-53.7189 1151.3111,-49.6183 1147.9933,-50.7328 1147.9933,-50.7328 1147.9933,-50.7328 1151.3111,-49.6183 1146.9902,-47.7468 1154.6289,-48.5038 1154.6289,-48.5038\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 11&#45;&gt;11 -->\n",
       "<g class=\"edge\" id=\"edge24\">\n",
       "<title>11-&gt;11</title>\n",
       "<path d=\"M1169.9371,-357.3317C1165.2613,-368.2753 1181.6265,-377.7401 1219.0328,-377.7401 1247.6719,-377.7401 1263.9772,-372.192 1267.9487,-364.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1268.1285,-357.3317 1271.1062,-364.4067 1268.0428,-360.8306 1267.9571,-364.3296 1267.9571,-364.3296 1267.9571,-364.3296 1268.0428,-360.8306 1264.8081,-364.2525 1268.1285,-357.3317 1268.1285,-357.3317\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 16 -->\n",
       "<g class=\"node\" id=\"node18\">\n",
       "<title>16</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-336.6701\">a=3, b=2, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1412.9638\" y=\"-321.6701\">!&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\">\n",
       "<title>12-&gt;16</title>\n",
       "<path d=\"M1295.0944,-281.3098C1329.1792,-290.4693 1369.4566,-301.2928 1404.2862,-310.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1411.1761,-312.5039 1403.5984,-313.7293 1407.796,-311.5956 1404.4159,-310.6872 1404.4159,-310.6872 1404.4159,-310.6872 1407.796,-311.5956 1405.2334,-307.6452 1411.1761,-312.5039 1411.1761,-312.5039\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 17 -->\n",
       "<g class=\"node\" id=\"node19\">\n",
       "<title>17</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-192.6701\">a=2, b=3, Q=0</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1414.9638\" y=\"-177.6701\">!&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\">\n",
       "<title>12-&gt;17</title>\n",
       "<path d=\"M1295.0944,-240.4303C1329.3242,-231.2319 1369.7995,-220.3551 1404.7305,-210.9683\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1411.6393,-209.1117 1405.6967,-213.9705 1408.2593,-210.02 1404.8792,-210.9284 1404.8792,-210.9284 1404.8792,-210.9284 1408.2593,-210.02 1404.0617,-207.8863 1411.6393,-209.1117 1411.6393,-209.1117\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 18 -->\n",
       "<g class=\"node\" id=\"node20\">\n",
       "<title>18</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-260.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-264.6701\">a=2, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1412.9638\" y=\"-249.6701\">!&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\">\n",
       "<title>12-&gt;18</title>\n",
       "<path d=\"M1331.4951,-254.1979C1343.3466,-254.1114 1355.4287,-254.097 1367.3571,-254.1546\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1374.3598,-254.1969 1367.3408,-257.3045 1370.8598,-254.1757 1367.3599,-254.1546 1367.3599,-254.1546 1367.3599,-254.1546 1370.8598,-254.1757 1367.379,-251.0046 1374.3598,-254.1969 1374.3598,-254.1969\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 19 -->\n",
       "<g class=\"node\" id=\"node21\">\n",
       "<title>19</title>\n",
       "<ellipse cx=\"1486.9638\" cy=\"-98.8701\" fill=\"#ffffaa\" rx=\"110.1176\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1441.9638\" y=\"-102.6701\">a=1, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1416.9638\" 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\">\n",
       "<title>13-&gt;19</title>\n",
       "<path d=\"M1289.087,-167.6232C1304.2622,-162.8811 1320.1964,-157.7952 1334.9983,-152.8701 1362.5563,-143.7004 1392.7319,-133.0958 1418.8792,-123.7247\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1425.7876,-121.2438 1420.2641,-126.5743 1422.4936,-122.4268 1419.1995,-123.6097 1419.1995,-123.6097 1419.1995,-123.6097 1422.4936,-122.4268 1418.1349,-120.645 1425.7876,-121.2438 1425.7876,-121.2438\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 14&#45;&gt;18 -->\n",
       "<g class=\"edge\" id=\"edge29\">\n",
       "<title>14-&gt;18</title>\n",
       "<path d=\"M1305.4887,-134.9763C1316.1455,-139.6391 1326.3216,-145.5011 1334.9983,-152.8701 1362.2679,-176.0296 1343.7286,-201.7105 1370.9983,-224.8701 1377.9125,-230.7422 1385.7788,-235.6574 1394.0818,-239.7714\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1400.5078,-242.7638 1392.8323,-242.6643 1397.335,-241.2863 1394.1621,-239.8087 1394.1621,-239.8087 1394.1621,-239.8087 1397.335,-241.2863 1395.4919,-236.9532 1400.5078,-242.7638 1400.5078,-242.7638\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 14&#45;&gt;19 -->\n",
       "<g class=\"edge\" id=\"edge30\">\n",
       "<title>14-&gt;19</title>\n",
       "<path d=\"M1330.7195,-109.3668C1344.7811,-108.4221 1359.1795,-107.4548 1373.2717,-106.5081\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1380.6096,-106.0151 1373.8365,-109.6273 1377.1175,-106.2497 1373.6253,-106.4844 1373.6253,-106.4844 1373.6253,-106.4844 1377.1175,-106.2497 1373.4141,-103.3415 1380.6096,-106.0151 1380.6096,-106.0151\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 15&#45;&gt;15 -->\n",
       "<g class=\"edge\" id=\"edge31\">\n",
       "<title>15-&gt;15</title>\n",
       "<path d=\"M1170.1441,-50.8749C1164.8107,-62.0106 1181.107,-71.7401 1219.0328,-71.7401 1248.6623,-71.7401 1265.0902,-65.8017 1268.3164,-57.8937\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1267.9215,-50.8749 1271.4599,-57.6868 1268.1181,-54.3693 1268.3148,-57.8638 1268.3148,-57.8638 1268.3148,-57.8638 1268.1181,-54.3693 1265.1698,-58.0408 1267.9215,-50.8749 1267.9215,-50.8749\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 20 -->\n",
       "<g class=\"node\" id=\"node22\">\n",
       "<title>20</title>\n",
       "<ellipse cx=\"1754.8948\" cy=\"-332.8701\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1709.8948\" y=\"-336.6701\">a=3, b=2, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1680.8948\" y=\"-321.6701\">!&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\">\n",
       "<title>16-&gt;20</title>\n",
       "<path d=\"M1599.4261,-326.1979C1611.2776,-326.1114 1623.3597,-326.097 1635.2882,-326.1546\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1642.2908,-326.1969 1635.2719,-329.3045 1638.7909,-326.1757 1635.2909,-326.1546 1635.2909,-326.1546 1635.2909,-326.1546 1638.7909,-326.1757 1635.31,-323.0046 1642.2908,-326.1969 1642.2908,-326.1969\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 21 -->\n",
       "<g class=\"node\" id=\"node23\">\n",
       "<title>21</title>\n",
       "<ellipse cx=\"1754.8948\" cy=\"-188.8701\" fill=\"#ffffaa\" rx=\"113.2743\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1709.8948\" y=\"-192.6701\">a=2, b=3, Q=1</text>\n",
       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1682.8948\" y=\"-177.6701\">!&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\">\n",
       "<title>17-&gt;21</title>\n",
       "<path d=\"M1596.7147,-182.219C1610.2518,-182.1073 1624.1303,-182.0902 1637.772,-182.1677\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1644.881,-182.2169 1637.8594,-185.3183 1641.3811,-182.1926 1637.8812,-182.1684 1637.8812,-182.1684 1637.8812,-182.1684 1641.3811,-182.1926 1637.903,-179.0184 1644.881,-182.2169 1644.881,-182.2169\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 18&#45;&gt;12 -->\n",
       "<g class=\"edge\" id=\"edge36\">\n",
       "<title>18-&gt;12</title>\n",
       "<path d=\"M1374.3598,-267.5432C1362.5064,-267.6292 1350.424,-267.643 1338.4968,-267.5848\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1331.4951,-267.5422 1338.5141,-264.4349 1334.995,-267.5635 1338.4949,-267.5849 1338.4949,-267.5849 1338.4949,-267.5849 1334.995,-267.5635 1338.4757,-270.7348 1331.4951,-267.5422 1331.4951,-267.5422\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 18&#45;&gt;20 -->\n",
       "<g class=\"edge\" id=\"edge34\">\n",
       "<title>18-&gt;20</title>\n",
       "<path d=\"M1563.0254,-281.3098C1597.1102,-290.4693 1637.3876,-301.2928 1672.2172,-310.6525\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1679.1071,-312.5039 1671.5294,-313.7293 1675.727,-311.5956 1672.3469,-310.6872 1672.3469,-310.6872 1672.3469,-310.6872 1675.727,-311.5956 1673.1644,-307.6452 1679.1071,-312.5039 1679.1071,-312.5039\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 18&#45;&gt;21 -->\n",
       "<g class=\"edge\" id=\"edge35\">\n",
       "<title>18-&gt;21</title>\n",
       "<path d=\"M1563.0254,-240.4303C1597.2552,-231.2319 1637.7305,-220.3551 1672.6616,-210.9683\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1679.5704,-209.1117 1673.6277,-213.9705 1676.1903,-210.02 1672.8102,-210.9284 1672.8102,-210.9284 1672.8102,-210.9284 1676.1903,-210.02 1671.9927,-207.8863 1679.5704,-209.1117 1679.5704,-209.1117\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 19&#45;&gt;19 -->\n",
       "<g class=\"edge\" id=\"edge37\">\n",
       "<title>19-&gt;19</title>\n",
       "<path d=\"M1437.8681,-123.3317C1433.1923,-134.2753 1449.5575,-143.7401 1486.9638,-143.7401 1515.6029,-143.7401 1531.9082,-138.192 1535.8797,-130.6799\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1536.0595,-123.3317 1539.0372,-130.4067 1535.9738,-126.8306 1535.8882,-130.3296 1535.8882,-130.3296 1535.8882,-130.3296 1535.9738,-126.8306 1532.7391,-130.2525 1536.0595,-123.3317 1536.0595,-123.3317\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 20&#45;&gt;16 -->\n",
       "<g class=\"edge\" id=\"edge38\">\n",
       "<title>20-&gt;16</title>\n",
       "<path d=\"M1642.2908,-339.5432C1630.4374,-339.6292 1618.3551,-339.643 1606.4278,-339.5848\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1599.4261,-339.5422 1606.4452,-336.4349 1602.926,-339.5635 1606.426,-339.5849 1606.426,-339.5849 1606.426,-339.5849 1602.926,-339.5635 1606.4067,-342.7348 1599.4261,-339.5422 1599.4261,-339.5422\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "<!-- 21&#45;&gt;17 -->\n",
       "<g class=\"edge\" id=\"edge39\">\n",
       "<title>21-&gt;17</title>\n",
       "<path d=\"M1644.881,-195.5232C1631.3394,-195.6338 1617.4604,-195.6497 1603.8218,-195.5709\" fill=\"none\" stroke=\"#000000\"/>\n",
       "<polygon fill=\"#000000\" points=\"1596.7147,-195.5211 1603.7366,-192.4203 1600.2146,-195.5457 1603.7145,-195.5702 1603.7145,-195.5702 1603.7145,-195.5702 1600.2146,-195.5457 1603.6924,-198.7202 1596.7147,-195.5211 1596.7147,-195.5211\" stroke=\"#000000\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<IPython.core.display.SVG object>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "k.show('.<0')  # unlimited output"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we have an LTL proposition to check, we can convert it into an automaton using `spot.translate()`, and synchronize that automaton with the Kripke structure using `spot.otf_product()`.  This `otf_product()` function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm \"consumes\" it (here the display routine). "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"198pt\" height=\"125pt\"\n",
       " viewBox=\"0.00 0.00 198.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 194,-120.8 194,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"72\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<!-- I -->\n",
       "<!-- 1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;1 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" 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=\"#000000\" stroke=\"#000000\" 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\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot;</text>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"168\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
       "<ellipse fill=\"none\" stroke=\"#000000\" 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\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M74.4945,-22C91.8699,-22 118.1605,-22 138.4436,-22\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"145.6169,-22 138.6169,-25.1501 142.1169,-22 138.6169,-22.0001 138.6169,-22.0001 138.6169,-22.0001 142.1169,-22 138.6169,-18.8501 145.6169,-22 145.6169,-22\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;b&gt;2&quot;</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M157.5737,-41.7575C155.8019,-52.3499 159.2773,-62 168,-62 174.6783,-62 178.2807,-56.3433 178.8074,-48.9379\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"178.4263,-41.7575 181.9429,-48.5807 178.6118,-45.2526 178.7974,-48.7476 178.7974,-48.7476 178.7974,-48.7476 178.6118,-45.2526 175.6518,-48.9146 178.4263,-41.7575 178.4263,-41.7575\"/>\n",
       "<text text-anchor=\"middle\" x=\"168\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb8f84691e0> >"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = spot.translate('\"a<1\" U \"b>2\"'); a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"734pt\" height=\"119pt\"\n",
       " viewBox=\"0.00 0.00 734.00 119.43\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.4593 .4593) rotate(0) translate(4 256)\">\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-256 1593.9262,-256 1593.9262,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"773.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
       "<text text-anchor=\"start\" x=\"795.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"811.9631\" y=\"-237.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
       "<text text-anchor=\"start\" x=\"771.9631\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"121.1926\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"65.1926\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=0, Q=0 * 1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M1.2707,-171C4.3,-171 15.9594,-171 30.899,-171\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9747,-171 30.9748,-174.1501 34.4747,-171 30.9747,-171.0001 30.9747,-171.0001 30.9747,-171.0001 34.4747,-171 30.9747,-167.8501 37.9747,-171 37.9747,-171\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"467.5779\" cy=\"-198\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"411.5779\" y=\"-194.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=0, Q=0 * 1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M199.7928,-177.1267C254.1557,-181.3642 326.4549,-186.9998 382.2262,-191.347\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"389.2887,-191.8975 382.0651,-194.4939 385.7993,-191.6255 382.3099,-191.3535 382.3099,-191.3535 382.3099,-191.3535 385.7993,-191.6255 382.5547,-188.213 389.2887,-191.8975 389.2887,-191.8975\"/>\n",
       "<text text-anchor=\"start\" x=\"222.3852\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"467.5779\" cy=\"-144\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"411.5779\" y=\"-140.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=1, Q=0 * 1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M193.2785,-161.9424C203.0521,-160.8635 212.9584,-159.8466 222.3852,-159 274.2017,-154.3465 332.3106,-150.7219 378.9492,-148.2023\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"386.0386,-147.823 379.217,-151.3426 382.5436,-148.0101 379.0486,-148.1971 379.0486,-148.1971 379.0486,-148.1971 382.5436,-148.0101 378.8803,-145.0516 386.0386,-147.823 386.0386,-147.823\"/>\n",
       "<text text-anchor=\"start\" x=\"222.3852\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"813.9631\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"757.9631\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=1, b=1, Q=0 * 1</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M546.178,-150.1267C600.541,-154.3642 672.8402,-159.9998 728.6114,-164.347\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"735.674,-164.8975 728.4503,-167.4939 732.1846,-164.6255 728.6951,-164.3535 728.6951,-164.3535 728.6951,-164.3535 732.1846,-164.6255 728.94,-161.213 735.674,-164.8975 735.674,-164.8975\"/>\n",
       "<text text-anchor=\"start\" x=\"568.7705\" y=\"-166.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"813.9631\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
       "<text text-anchor=\"start\" x=\"757.9631\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a=0, b=2, Q=0 * 1</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M539.6637,-134.9424C549.4373,-133.8635 559.3436,-132.8466 568.7705,-132 620.587,-127.3465 678.6958,-123.7219 725.3344,-121.2023\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"732.4239,-120.823 725.6022,-124.3426 728.9289,-121.0101 725.4339,-121.1971 725.4339,-121.1971 725.4339,-121.1971 728.9289,-121.0101 725.2655,-118.0516 732.4239,-120.823 732.4239,-120.823\"/>\n",
       "<text text-anchor=\"start\" x=\"568.7705\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",