diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb
index 1595234e6..5804bd265 100644
--- a/tests/python/highlighting.ipynb
+++ b/tests/python/highlighting.ipynb
@@ -17,7 +17,8 @@
    "pygments_lexer": "ipython3",
    "version": "3.4.3+"
   },
-  "name": ""
+  "name": "",
+  "signature": "sha256:0f4fb50930c6511a58891626864fe3236e91bb2525f9d8b2b1108f3e2a4c5d28"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -29,13 +30,27 @@
      "collapsed": false,
      "input": [
       "import spot\n",
-      "spot.setup()"
+      "spot.setup()\n",
+      "from IPython.display import display"
      ],
      "language": "python",
      "metadata": {},
      "outputs": [],
      "prompt_number": 1
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "This notebook shows you different ways in which states or transitions can be highlighted in Spot.  \n",
+      "\n",
+      "It should be noted that highlighting works using some special [named properties](https://spot.lrde.epita.fr/concepts.html#named-properties): basically, two maps that are attached to the automaton, and associated state or edge numbers to color numbers.  This named properties are fragile: they will be lost if the automaton is transformed into a new automaton, and they can become meaningless of the automaton is modified in place (e.g., if the transitions or states are reordered).\n",
+      "\n",
+      "Nonetheless, highlighting is OK to use right before displaying or printing the automaton.  The `dot` and `hoa` printer both know how to represent highlighted states and transitions.\n",
+      "\n",
+      "# Manual highlighting"
+     ]
+    },
     {
      "cell_type": "code",
      "collapsed": false,
@@ -140,7 +155,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG object>"
+        "<IPython.core.display.SVG at 0x7f44a034f208>"
        ]
       }
      ],
@@ -240,7 +255,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd034659540> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a00f88a0> >"
        ]
       }
      ],
@@ -342,7 +357,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fd034190180> >"
+        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f44a006cf30> >"
        ]
       }
      ],
@@ -352,6 +367,78 @@
      "cell_type": "markdown",
      "metadata": {},
      "source": [
+      "# Saving the HOA 1.1\n",
+      "\n",
+      "When saving to HOA format, the highlighting is only output if version 1.1 of the format is selected, because the headers `spot.highlight.edges` and `spot.highlight.states` contain dots, which are disallowed in version 1.  Compare these two outputs:"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "print(a.to_str('HOA', '1'))\n",
+      "print()\n",
+      "print(a.to_str('HOA', '1.1'))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "output_type": "stream",
+       "stream": "stdout",
+       "text": [
+        "HOA: v1\n",
+        "States: 3\n",
+        "Start: 2\n",
+        "AP: 3 \"a\" \"b\" \"c\"\n",
+        "acc-name: Buchi\n",
+        "Acceptance: 1 Inf(0)\n",
+        "properties: trans-labels explicit-labels state-acc deterministic\n",
+        "properties: stutter-invariant terminal\n",
+        "--BODY--\n",
+        "State: 0 {0}\n",
+        "[t] 0\n",
+        "State: 1\n",
+        "[2] 0\n",
+        "[1&!2] 1\n",
+        "State: 2\n",
+        "[2] 0\n",
+        "[!0&1&!2] 1\n",
+        "[0&!2] 2\n",
+        "--END--\n",
+        "\n",
+        "HOA: v1.1\n",
+        "States: 3\n",
+        "Start: 2\n",
+        "AP: 3 \"a\" \"b\" \"c\"\n",
+        "acc-name: Buchi\n",
+        "Acceptance: 1 Inf(0)\n",
+        "properties: trans-labels explicit-labels state-acc !complete\n",
+        "properties: deterministic stutter-invariant terminal\n",
+        "spot.highlight.states: 0 0 1 0\n",
+        "spot.highlight.edges: 2 1 4 1 5 1 6 2\n",
+        "--BODY--\n",
+        "State: 0 {0}\n",
+        "[t] 0\n",
+        "State: 1\n",
+        "[2] 0\n",
+        "[1&!2] 1\n",
+        "State: 2\n",
+        "[2] 0\n",
+        "[!0&1&!2] 1\n",
+        "[0&!2] 2\n",
+        "--END--\n"
+       ]
+      }
+     ],
+     "prompt_number": 6
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Highlighting a run\n",
+      "\n",
       "One use of this highlighting is to highlight a run in an automaton.\n",
       "\n",
       "The following few command generate an automaton, then an accepting run on this automaton, and highlight that accepting run on the automaton.  Note that a run knows the automaton from which it was generated, so calling `highlight()` will directly decorate that automaton."
@@ -369,7 +456,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 6,
+       "prompt_number": 7,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -485,11 +572,11 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd034190240> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cfc0> >"
        ]
       }
      ],
-     "prompt_number": 6
+     "prompt_number": 7
     },
     {
      "cell_type": "code",
@@ -503,7 +590,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 7,
+       "prompt_number": 8,
        "text": [
         "Prefix:\n",
         "  0\n",
@@ -516,7 +603,7 @@
        ]
       }
      ],
-     "prompt_number": 7
+     "prompt_number": 8
     },
     {
      "cell_type": "code",
@@ -527,7 +614,14 @@
      "language": "python",
      "metadata": {},
      "outputs": [],
-     "prompt_number": 8
+     "prompt_number": 9
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The call of `highlight(5)` on the accepting run `r` modified the original automaton `b`:"
+     ]
     },
     {
      "cell_type": "code",
@@ -541,7 +635,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 9,
+       "prompt_number": 10,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -657,11 +751,962 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd034190240> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cfc0> >"
        ]
       }
      ],
-     "prompt_number": 9
+     "prompt_number": 10
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Highlighting from a product\n",
+      "\n",
+      "Pretty often, accepting runs are found in a product but we want to display them on one of the original automata.  This can be done by projecting the runs on those automata before displaying them."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "left = spot.translate('a U b')\n",
+      "right = spot.translate('GFa')\n",
+      "display(left, right)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"171pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" 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\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50f0> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"82pt\" height=\"125pt\"\n",
+        " viewBox=\"0.00 0.00 82.00 125.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 121)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-121 78,-121 78,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"59.2357,-35.7817 62.4756,-42.7406 59.2808,-39.2814 59.3258,-42.7812 59.3258,-42.7812 59.3258,-42.7812 59.2808,-39.2814 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817\"/>\n",
+        "<text text-anchor=\"start\" x=\"52.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"48\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M50.9906,-35.5771C47.5451,-56.718 49.2148,-84 56,-84 62.043,-84 64.0285,-62.3596 61.9564,-42.6907\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"61.0094,-35.5771 65.0556,-42.1002 61.4713,-39.0465 61.9332,-42.5159 61.9332,-42.5159 61.9332,-42.5159 61.4713,-39.0465 58.8107,-42.9316 61.0094,-35.5771 61.0094,-35.5771\"/>\n",
+        "<text text-anchor=\"start\" x=\"50.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50c0> >"
+       ]
+      }
+     ],
+     "prompt_number": 11
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "prod = spot.product(left, right); prod"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 12,
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"227pt\" height=\"141pt\"\n",
+        " viewBox=\"0.00 0.00 227.00 141.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 137.496)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-137.496 223,-137.496 223,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"65\" cy=\"-21.4964\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"65\" y=\"-17.7964\" font-family=\"Lato\" font-size=\"14.00\">1,0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-21.4964C1.94863,-21.4964 16.101,-21.4964 30.7579,-21.4964\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9378,-21.4964 30.9378,-24.6465 34.4378,-21.4964 30.9378,-21.4965 30.9378,-21.4965 30.9378,-21.4965 34.4378,-21.4964 30.9378,-18.3465 37.9378,-21.4964 37.9378,-21.4964\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-38.9063C55.6785,-48.5843 58.2969,-57.4964 65,-57.4964 69.9226,-57.4964 72.6423,-52.69 73.1591,-46.3036\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"72.8552,-38.9063 76.2899,-45.771 72.9989,-42.4033 73.1426,-45.9004 73.1426,-45.9004 73.1426,-45.9004 72.9989,-42.4033 69.9953,-46.0297 72.8552,-38.9063 72.8552,-38.9063\"/>\n",
+        "<text text-anchor=\"start\" x=\"46.5\" y=\"-76.2964\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"57\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"192\" cy=\"-21.4964\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"192\" y=\"-17.7964\" font-family=\"Lato\" font-size=\"14.00\">0,0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M92.2041,-21.4964C111.288,-21.4964 137.281,-21.4964 157.815,-21.4964\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"164.83,-21.4964 157.83,-24.6465 161.33,-21.4964 157.83,-21.4965 157.83,-21.4965 157.83,-21.4965 161.33,-21.4964 157.83,-18.3465 164.83,-21.4964 164.83,-21.4964\"/>\n",
+        "<text text-anchor=\"start\" x=\"111.5\" y=\"-40.2964\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"120.5\" y=\"-25.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M86.9111,-10.4028C94.0344,-7.18923 102.177,-4.11316 110,-2.49636 126.104,0.83212 130.896,0.83212 147,-2.49636 152.5,-3.63317 158.159,-5.49143 163.51,-7.61164\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"170.089,-10.4028 162.415,-10.5685 166.867,-9.03575 163.645,-7.66873 163.645,-7.66873 163.645,-7.66873 166.867,-9.03575 164.875,-4.76892 170.089,-10.4028 170.089,-10.4028\"/>\n",
+        "<text text-anchor=\"start\" x=\"110\" y=\"-6.29636\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M186.427,-39.2781C185.48,-48.8113 187.338,-57.4964 192,-57.4964 195.424,-57.4964 197.335,-52.8125 197.734,-46.5485\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"197.573,-39.2781 200.877,-46.2066 197.65,-42.7772 197.728,-46.2764 197.728,-46.2764 197.728,-46.2764 197.65,-42.7772 194.579,-46.3462 197.573,-39.2781 197.573,-39.2781\"/>\n",
+        "<text text-anchor=\"start\" x=\"188.5\" y=\"-75.2964\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"176\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"192\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M183.373,-38.7697C177.439,-59.3511 180.314,-85.4964 192,-85.4964 202.407,-85.4964 205.827,-64.7576 202.258,-45.6812\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"200.627,-38.7697 205.301,-44.8591 201.431,-42.1762 202.235,-45.5826 202.235,-45.5826 202.235,-45.5826 201.431,-42.1762 199.169,-46.3061 200.627,-38.7697 200.627,-38.7697\"/>\n",
+        "<text text-anchor=\"start\" x=\"186.5\" y=\"-104.296\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<text text-anchor=\"start\" x=\"184\" y=\"-89.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cf60> >"
+       ]
+      }
+     ],
+     "prompt_number": 12
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "run = spot.couvreur99(prod).check().accepting_run(); run"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 13,
+       "text": [
+        "Prefix:\n",
+        "  0\n",
+        "  |  a & b\t{1}\n",
+        "Cycle:\n",
+        "  1\n",
+        "  |  a\t{0,1}"
+       ]
+      }
+     ],
+     "prompt_number": 13
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "run.highlight(5)\n",
+      "# Note that by default project() needs to know on which side you project, but it cannot \n",
+      "# guess it.  The left-side is assumed unless you pass True as a second argument.\n",
+      "run.project(left).highlight(5)\n",
+      "run.project(right, True).highlight(5)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": 14
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "display(prod, left, right)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"227pt\" height=\"141pt\"\n",
+        " viewBox=\"0.00 0.00 227.00 141.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 137.496)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-137.496 223,-137.496 223,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"65\" cy=\"-21.4964\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"65\" y=\"-17.7964\" font-family=\"Lato\" font-size=\"14.00\">1,0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-21.4964C1.94863,-21.4964 16.101,-21.4964 30.7579,-21.4964\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9378,-21.4964 30.9378,-24.6465 34.4378,-21.4964 30.9378,-21.4965 30.9378,-21.4965 30.9378,-21.4965 34.4378,-21.4964 30.9378,-18.3465 37.9378,-21.4964 37.9378,-21.4964\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-38.9063C55.6785,-48.5843 58.2969,-57.4964 65,-57.4964 69.9226,-57.4964 72.6423,-52.69 73.1591,-46.3036\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"72.8552,-38.9063 76.2899,-45.771 72.9989,-42.4033 73.1426,-45.9004 73.1426,-45.9004 73.1426,-45.9004 72.9989,-42.4033 69.9953,-46.0297 72.8552,-38.9063 72.8552,-38.9063\"/>\n",
+        "<text text-anchor=\"start\" x=\"46.5\" y=\"-76.2964\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"57\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"192\" cy=\"-21.4964\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"192\" y=\"-17.7964\" font-family=\"Lato\" font-size=\"14.00\">0,0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M92.2041,-21.4964C111.288,-21.4964 137.281,-21.4964 157.815,-21.4964\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"164.83,-21.4964 157.83,-24.6465 161.33,-21.9964 157.83,-21.9965 157.83,-21.4965 157.83,-20.9965 161.33,-20.9964 157.83,-18.3465 164.83,-21.4964 164.83,-21.4964\"/>\n",
+        "<text text-anchor=\"start\" x=\"111.5\" y=\"-40.2964\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"120.5\" y=\"-25.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M86.9111,-10.4028C94.0344,-7.18923 102.177,-4.11316 110,-2.49636 126.104,0.83212 130.896,0.83212 147,-2.49636 152.5,-3.63317 158.159,-5.49143 163.51,-7.61164\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"170.089,-10.4028 162.415,-10.5685 166.867,-9.03575 163.645,-7.66873 163.645,-7.66873 163.645,-7.66873 166.867,-9.03575 164.875,-4.76892 170.089,-10.4028 170.089,-10.4028\"/>\n",
+        "<text text-anchor=\"start\" x=\"110\" y=\"-6.29636\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M186.427,-39.2781C185.48,-48.8113 187.338,-57.4964 192,-57.4964 195.424,-57.4964 197.335,-52.8125 197.734,-46.5485\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"197.573,-39.2781 200.877,-46.2066 198.15,-42.7662 198.228,-46.2653 197.728,-46.2764 197.228,-46.2875 197.15,-42.7883 194.579,-46.3462 197.573,-39.2781 197.573,-39.2781\"/>\n",
+        "<text text-anchor=\"start\" x=\"188.5\" y=\"-75.2964\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"176\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"192\" y=\"-61.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M183.373,-38.7697C177.439,-59.3511 180.314,-85.4964 192,-85.4964 202.407,-85.4964 205.827,-64.7576 202.258,-45.6812\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"200.627,-38.7697 205.301,-44.8591 201.431,-42.1762 202.235,-45.5826 202.235,-45.5826 202.235,-45.5826 201.431,-42.1762 199.169,-46.3061 200.627,-38.7697 200.627,-38.7697\"/>\n",
+        "<text text-anchor=\"start\" x=\"186.5\" y=\"-104.296\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<text text-anchor=\"start\" x=\"184\" y=\"-89.2964\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cf60> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"171pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 171.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" 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\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"118.997,-22 111.997,-25.1501 115.497,-22.5 111.997,-22.5001 111.997,-22.0001 111.997,-21.5001 115.497,-21.5 111.997,-18.8501 118.997,-22 118.997,-22\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"149.006,-42.5808 152.273,-49.5273 149.565,-46.072 149.623,-49.5715 149.123,-49.5798 148.623,-49.5882 148.565,-46.0887 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50f0> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"82pt\" height=\"125pt\"\n",
+        " viewBox=\"0.00 0.00 82.00 125.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 121)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-121 78,-121 78,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"59.2357,-35.7817 62.4756,-42.7406 59.7808,-39.275 59.8258,-42.7747 59.3258,-42.7812 58.8259,-42.7876 58.7808,-39.2879 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817\"/>\n",
+        "<text text-anchor=\"start\" x=\"52.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"48\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M50.9906,-35.5771C47.5451,-56.718 49.2148,-84 56,-84 62.043,-84 64.0285,-62.3596 61.9564,-42.6907\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"61.0094,-35.5771 65.0556,-42.1002 61.4713,-39.0465 61.9332,-42.5159 61.9332,-42.5159 61.9332,-42.5159 61.4713,-39.0465 58.8107,-42.9316 61.0094,-35.5771 61.0094,-35.5771\"/>\n",
+        "<text text-anchor=\"start\" x=\"50.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50c0> >"
+       ]
+      }
+     ],
+     "prompt_number": 15
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The projection also works for products generated on-the-fly, but the on-the-fly product itself cannot be highlighted (it does not store states or transitions). "
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "left2 = spot.translate('!b & FG a')\n",
+      "right2 = spot.translate('XXXb')\n",
+      "prod2 = spot.otf_product(left2, right2)  # Note \"otf_product()\"\n",
+      "run2 = spot.couvreur99(prod2).check().accepting_run()\n",
+      "run2.project(left2).highlight(5)\n",
+      "run2.project(right2, True).highlight(5)\n",
+      "display(run2, prod2, left2, right2)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "text": [
+        "Prefix:\n",
+        "  0 * 3\n",
+        "  |  a & !b\n",
+        "  1 * 2\n",
+        "  |  a\t{0}\n",
+        "  1 * 1\n",
+        "  |  a\t{0}\n",
+        "  1 * 0\n",
+        "  |  a & b\t{0}\n",
+        "Cycle:\n",
+        "  1 * 4\n",
+        "  |  a\t{0,1}"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"687pt\" height=\"226pt\"\n",
+        " viewBox=\"0.00 0.00 686.57 226.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 222)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-222 682.567,-222 682.567,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"68.5473\" cy=\"-168\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"68.5473\" y=\"-164.3\" font-family=\"Lato\" font-size=\"14.00\">0 * 3</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.04823,-168C1.96146,-168 15.7044,-168 30.461,-168\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.7348,-168 30.7348,-171.15 34.2348,-168 30.7348,-168 30.7348,-168 30.7348,-168 34.2348,-168 30.7347,-164.85 37.7348,-168 37.7348,-168\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"202.642\" cy=\"-193\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"202.642\" y=\"-189.3\" font-family=\"Lato\" font-size=\"14.00\">1 * 2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M97.8849,-173.363C117.909,-177.153 144.887,-182.259 166.315,-186.314\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"173.351,-187.646 165.887,-189.439 169.912,-186.995 166.473,-186.344 166.473,-186.344 166.473,-186.344 169.912,-186.995 167.059,-183.249 173.351,-187.646 173.351,-187.646\"/>\n",
+        "<text text-anchor=\"start\" x=\"117.095\" y=\"-186.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"202.642\" cy=\"-139\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"202.642\" y=\"-135.3\" font-family=\"Lato\" font-size=\"14.00\">2 * 2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M97.5612,-161.85C117.701,-157.428 144.999,-151.435 166.585,-146.696\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"173.668,-145.141 167.507,-149.719 170.25,-145.892 166.831,-146.642 166.831,-146.642 166.831,-146.642 170.25,-145.892 166.156,-143.566 173.668,-145.141 173.668,-145.141\"/>\n",
+        "<text text-anchor=\"start\" x=\"129.095\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"315.736\" cy=\"-182\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"315.736\" y=\"-178.3\" font-family=\"Lato\" font-size=\"14.00\">1 * 1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M232.831,-190.11C246.753,-188.731 263.551,-187.068 278.302,-185.608\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"285.357,-184.909 278.701,-188.734 281.874,-185.254 278.391,-185.599 278.391,-185.599 278.391,-185.599 281.874,-185.254 278.081,-182.464 285.357,-184.909 285.357,-184.909\"/>\n",
+        "<text text-anchor=\"start\" x=\"255.689\" y=\"-206.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"251.189\" y=\"-191.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M228.574,-148.65C244.726,-154.902 265.901,-163.098 283.217,-169.8\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"289.888,-172.382 282.223,-172.793 286.624,-171.119 283.36,-169.855 283.36,-169.855 283.36,-169.855 286.624,-171.119 284.497,-166.918 289.888,-172.382 289.888,-172.382\"/>\n",
+        "<text text-anchor=\"start\" x=\"255.689\" y=\"-166.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"315.736\" cy=\"-117\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"315.736\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">2 * 1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M225.749,-127.04C233.558,-123.415 242.551,-119.894 251.189,-118 259.864,-116.098 269.365,-115.293 278.316,-115.084\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"285.35,-115.034 278.372,-118.234 281.85,-115.059 278.35,-115.084 278.35,-115.084 278.35,-115.084 281.85,-115.059 278.327,-111.934 285.35,-115.034 285.35,-115.034\"/>\n",
+        "<text text-anchor=\"middle\" x=\"259.189\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"428.831\" cy=\"-171\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"428.831\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">1 * 0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;5 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M345.925,-179.11C359.848,-177.731 376.646,-176.068 391.396,-174.608\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"398.451,-173.909 391.796,-177.734 394.968,-174.254 391.486,-174.599 391.486,-174.599 391.486,-174.599 394.968,-174.254 391.175,-171.464 398.451,-173.909 398.451,-173.909\"/>\n",
+        "<text text-anchor=\"start\" x=\"368.784\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"364.284\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;5 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>4&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M339.755,-128.189C356.736,-136.443 379.98,-147.741 398.325,-156.658\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"404.842,-159.825 397.169,-159.598 401.694,-158.295 398.546,-156.765 398.546,-156.765 398.546,-156.765 401.694,-158.295 399.923,-153.932 404.842,-159.825 404.842,-159.825\"/>\n",
+        "<text text-anchor=\"start\" x=\"368.784\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"428.831\" cy=\"-106\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"428.831\" y=\"-102.3\" font-family=\"Lato\" font-size=\"14.00\">2 * 0</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;6 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>4&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M344.248,-110.281C350.777,-108.947 357.745,-107.732 364.284,-107 372.85,-106.041 382.107,-105.574 390.834,-105.388\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"398.013,-105.294 391.056,-108.536 394.514,-105.34 391.014,-105.386 391.014,-105.386 391.014,-105.386 394.514,-105.34 390.973,-102.236 398.013,-105.294 398.013,-105.294\"/>\n",
+        "<text text-anchor=\"middle\" x=\"372.284\" y=\"-110.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"648.02\" cy=\"-120\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"648.02\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">1 * 4</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;7 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>5&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M457.78,-164.437C497.284,-155.161 569.407,-138.225 612.298,-128.154\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"619.178,-126.538 613.084,-131.205 615.771,-127.338 612.364,-128.138 612.364,-128.138 612.364,-128.138 615.771,-127.338 611.644,-125.071 619.178,-126.538 619.178,-126.538\"/>\n",
+        "<text text-anchor=\"start\" x=\"517.926\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"526.926\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;7 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>6&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M459.575,-107.917C498.892,-110.452 568.127,-114.915 610.553,-117.649\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"617.636,-118.106 610.447,-120.799 614.143,-117.881 610.65,-117.655 610.65,-117.655 610.65,-117.655 614.143,-117.881 610.853,-114.512 617.636,-118.106 617.636,-118.106\"/>\n",
+        "<text text-anchor=\"start\" x=\"517.926\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"534.926\" cy=\"-18\" rx=\"30.5947\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"534.926\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2 * 4</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;8 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>6&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M447.02,-91.4686C464.499,-76.6922 491.685,-53.7096 510.992,-37.388\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"516.711,-32.553 513.399,-39.4778 514.038,-34.8126 511.365,-37.0722 511.365,-37.0722 511.365,-37.0722 514.038,-34.8126 509.332,-34.6666 516.711,-32.553 516.711,-32.553\"/>\n",
+        "<text text-anchor=\"start\" x=\"477.378\" y=\"-68.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;7 -->\n",
+        "<g id=\"edge13\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M638.097,-137.037C636.072,-146.858 639.38,-156 648.02,-156 654.501,-156 657.981,-150.858 658.462,-144.143\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"657.943,-137.037 661.595,-143.789 658.198,-140.528 658.453,-144.019 658.453,-144.019 658.453,-144.019 658.198,-140.528 655.312,-144.248 657.943,-137.037 657.943,-137.037\"/>\n",
+        "<text text-anchor=\"start\" x=\"644.52\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"632.02\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"648.02\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;7 -->\n",
+        "<g id=\"edge14\" class=\"edge\"><title>8&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M552.412,-32.9907C565.257,-44.6835 583.526,-61.3444 599.473,-76 607.951,-83.7912 617.252,-92.3875 625.362,-99.8991\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"630.761,-104.903 623.486,-102.455 628.194,-102.524 625.627,-100.145 625.627,-100.145 625.627,-100.145 628.194,-102.524 627.768,-97.8343 630.761,-104.903 630.761,-104.903\"/>\n",
+        "<text text-anchor=\"start\" x=\"587.973\" y=\"-94.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"583.473\" y=\"-79.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;8 -->\n",
+        "<g id=\"edge15\" class=\"edge\"><title>8&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M525.642,-35.4099C523.909,-45.0879 527.004,-54 534.926,-54 540.743,-54 543.957,-49.1936 544.568,-42.8073\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"544.209,-35.4099 547.695,-42.2489 544.379,-38.9058 544.549,-42.4017 544.549,-42.4017 544.549,-42.4017 544.379,-38.9058 541.402,-42.5544 544.209,-35.4099 544.209,-35.4099\"/>\n",
+        "<text text-anchor=\"start\" x=\"530.426\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"start\" x=\"526.926\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f44a68f5120> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"247pt\" height=\"150pt\"\n",
+        " viewBox=\"0.00 0.00 247.00 150.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 146)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-146 243,-146 243,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-76C2.79388,-76 17.1543,-76 30.6317,-76\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-76 30.9419,-79.1501 34.4419,-76 30.9419,-76.0001 30.9419,-76.0001 30.9419,-76.0001 34.4419,-76 30.9418,-72.8501 37.9419,-76 37.9419,-76\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"221\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"221\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M74.0904,-76.66C87.4132,-77.14 106.38,-77.7482 123,-78 139.443,-78.2491 143.558,-78.274 160,-78 171.769,-77.8039 184.832,-77.3916 195.756,-76.992\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"202.935,-76.7202 196.059,-80.1328 199.456,-77.3523 195.959,-77.4847 195.94,-76.9851 195.921,-76.4855 199.418,-76.353 195.82,-73.8374 202.935,-76.7202 202.935,-76.7202\"/>\n",
+        "<text text-anchor=\"start\" x=\"123\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M71.1646,-66.1611C84.5999,-56.8288 104.934,-42.7047 120.112,-32.1619\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"126.266,-27.8872 122.314,-34.4678 123.391,-29.8839 120.517,-31.8806 120.517,-31.8806 120.517,-31.8806 123.391,-29.8839 118.72,-29.2935 126.266,-27.8872 126.266,-27.8872\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-53.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M214.266,-93.0373C212.892,-102.858 215.137,-112 221,-112 225.397,-112 227.759,-106.858 228.086,-100.143\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"227.734,-93.0373 231.226,-99.8728 228.406,-96.5083 228.58,-100.004 228.08,-100.029 227.581,-100.053 227.408,-96.5578 224.934,-100.185 227.734,-93.0373 227.734,-93.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"217.5\" y=\"-130.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"213\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M156.355,-28.3692C168.513,-37.4677 186.34,-50.8092 200.036,-61.0593\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"206.003,-65.525 198.511,-63.8527 203.201,-63.4279 200.399,-61.3307 200.399,-61.3307 200.399,-61.3307 203.201,-63.4279 202.286,-58.8088 206.003,-65.525 206.003,-65.525\"/>\n",
+        "<text text-anchor=\"start\" x=\"178\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M134.469,-34.6641C132.906,-44.625 135.25,-54 141.5,-54 146.188,-54 148.678,-48.7266 148.971,-41.8876\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"148.531,-34.6641 152.101,-41.4598 148.744,-38.1576 148.956,-41.6511 148.956,-41.6511 148.956,-41.6511 148.744,-38.1576 145.812,-41.8425 148.531,-34.6641 148.531,-34.6641\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5060> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"414pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 414.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 410,-81 410,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" 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\">3</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;3 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M74.1418,-22C85.1153,-22 99.5214,-22 111.67,-22\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"118.892,-22 111.892,-25.1501 115.392,-22.5 111.892,-22.5001 111.892,-22.0001 111.892,-21.5001 115.392,-21.5 111.892,-18.8501 118.892,-22 118.892,-22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"299\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"299\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"384\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"384\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"384\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M317.198,-22C328.073,-22 342.387,-22 354.887,-22\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"361.997,-22 354.997,-25.1501 358.497,-22.5 354.997,-22.5001 354.997,-22.0001 354.997,-21.5001 358.497,-21.5 354.997,-18.8501 361.997,-22 361.997,-22\"/>\n",
+        "<text text-anchor=\"start\" x=\"335\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M375.994,-42.5808C374.886,-52.8447 377.555,-62 384,-62 388.834,-62 391.544,-56.8502 392.129,-49.9451\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"392.006,-42.5808 395.273,-49.5273 392.565,-46.072 392.623,-49.5715 392.123,-49.5798 391.623,-49.5882 391.565,-46.0887 388.973,-49.6324 392.006,-42.5808 392.006,-42.5808\"/>\n",
+        "<text text-anchor=\"middle\" x=\"384\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"218\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M236.142,-22C247.115,-22 261.521,-22 273.67,-22\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"280.892,-22 273.892,-25.1501 277.392,-22.5 273.892,-22.5001 273.892,-22.0001 273.892,-21.5001 277.392,-21.5 273.892,-18.8501 280.892,-22 280.892,-22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"258.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M155.142,-22C166.115,-22 180.521,-22 192.67,-22\"/>\n",
+        "<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"199.892,-22 192.892,-25.1501 196.392,-22.5 192.892,-22.5001 192.892,-22.0001 192.892,-21.5001 196.392,-21.5 192.892,-18.8501 199.892,-22 199.892,-22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"177.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5030> >"
+       ]
+      }
+     ],
+     "prompt_number": 16
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Highlighting nondeterminism\n",
+      "\n",
+      "Sometimes its is hard to locate non-deterministic states inside a large automaton.  Here are two functions that can help for that."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "b = spot.translate('X (F(Ga <-> b) & GF!b)')\n",
+      "spot.highlight_nondet_states(b, 5)\n",
+      "spot.highlight_nondet_edges(b, 4)\n",
+      "b"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 17,
+       "svg": [
+        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"386pt\" height=\"284pt\"\n",
+        " viewBox=\"0.00 0.00 386.00 284.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 280)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-280 382,-280 382,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-105C2.79388,-105 17.1543,-105 30.6317,-105\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-105 30.9419,-108.15 34.4419,-105 30.9419,-105 30.9419,-105 30.9419,-105 34.4419,-105 30.9418,-101.85 37.9419,-105 37.9419,-105\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"#f15854\" stroke-width=\"2\" cx=\"137\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-105C85.1153,-105 99.5214,-105 111.67,-105\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-105 111.892,-108.15 115.392,-105 111.892,-105 111.892,-105 111.892,-105 115.392,-105 111.892,-101.85 118.892,-105 118.892,-105\"/>\n",
+        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M129.969,-121.664C128.406,-131.625 130.75,-141 137,-141 141.688,-141 144.178,-135.727 144.471,-128.888\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"144.031,-121.664 147.601,-128.46 144.743,-125.127 144.955,-128.621 144.456,-128.651 143.957,-128.682 143.745,-125.188 141.312,-128.842 144.031,-121.664 144.031,-121.664\"/>\n",
+        "<text text-anchor=\"start\" x=\"123.5\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"360\" cy=\"-177\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"360\" y=\"-173.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M145.493,-120.895C158.318,-145.976 187.11,-193.848 228,-213 265.175,-230.412 312.353,-207.508 338.749,-191.059\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"344.681,-187.252 340.492,-193.684 341.736,-189.142 338.79,-191.033 338.79,-191.033 338.79,-191.033 341.736,-189.142 337.089,-188.382 344.681,-187.252 344.681,-187.252\"/>\n",
+        "<text text-anchor=\"start\" x=\"228\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M155.109,-105C173.324,-105 202.31,-105 222.956,-105\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"230.149,-105 223.149,-108.15 226.649,-105.5 223.149,-105.5 223.149,-105 223.149,-104.5 226.649,-104.5 223.149,-101.85 230.149,-105 230.149,-105\"/>\n",
+        "<text text-anchor=\"start\" x=\"174.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"248.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"#60bd68\" stroke-width=\"2\" d=\"M151.868,-93.9814C171.203,-78.6193 206.342,-50.7007 228.218,-33.3198\"/>\n",
+        "<polygon fill=\"#60bd68\" stroke=\"#60bd68\" stroke-width=\"2\" points=\"233.744,-28.9291 230.223,-35.75 231.315,-31.4979 228.575,-33.6752 228.264,-33.2837 227.953,-32.8922 230.693,-30.7149 226.304,-30.8174 233.744,-28.9291 233.744,-28.9291\"/>\n",
+        "<text text-anchor=\"start\" x=\"173\" y=\"-79.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M355.18,-194.41C354.28,-204.088 355.887,-213 360,-213 363.021,-213 364.69,-208.194 365.007,-201.807\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"364.82,-194.41 368.146,-201.328 364.908,-197.909 364.997,-201.408 364.997,-201.408 364.997,-201.408 364.908,-197.909 361.848,-201.487 364.82,-194.41 364.82,-194.41\"/>\n",
+        "<text text-anchor=\"start\" x=\"355.5\" y=\"-216.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M352.328,-193.308C347.37,-210.96 349.928,-231 360,-231 368.735,-231 371.818,-215.93 369.25,-200.415\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"367.672,-193.308 372.264,-199.459 368.431,-196.725 369.189,-200.142 369.189,-200.142 369.189,-200.142 368.431,-196.725 366.114,-200.825 367.672,-193.308 367.672,-193.308\"/>\n",
+        "<text text-anchor=\"start\" x=\"353.5\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "<text text-anchor=\"start\" x=\"352\" y=\"-234.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M243.501,-122.41C242.568,-132.088 244.234,-141 248.5,-141 251.633,-141 253.363,-136.194 253.692,-129.807\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"253.499,-122.41 256.831,-129.325 253.59,-125.909 253.682,-129.408 253.682,-129.408 253.682,-129.408 253.59,-125.909 250.533,-129.49 253.499,-122.41 253.499,-122.41\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M240.544,-121.308C235.403,-138.96 238.055,-159 248.5,-159 257.558,-159 260.756,-143.93 258.092,-128.415\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"256.456,-121.308 261.096,-127.423 257.242,-124.719 258.027,-128.13 258.027,-128.13 258.027,-128.13 257.242,-124.719 254.957,-128.837 256.456,-121.308 256.456,-121.308\"/>\n",
+        "<text text-anchor=\"start\" x=\"230\" y=\"-177.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"240.5\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M259.411,-32.3906C278.856,-60.6271 322.078,-123.387 344.648,-156.161\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"348.874,-162.297 342.309,-158.318 346.889,-159.414 344.904,-156.532 344.904,-156.532 344.904,-156.532 346.889,-159.414 347.498,-154.745 348.874,-162.297 348.874,-162.297\"/>\n",
+        "<text text-anchor=\"start\" x=\"287\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M238.925,-33.5414C236.23,-43.9087 239.422,-54 248.5,-54 255.45,-54 258.95,-48.0847 258.999,-40.6591\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"258.075,-33.5414 262.1,-40.0771 258.526,-37.0123 258.977,-40.4831 258.977,-40.4831 258.977,-40.4831 258.526,-37.0123 255.853,-40.889 258.075,-33.5414 258.075,-33.5414\"/>\n",
+        "<text text-anchor=\"start\" x=\"231.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5210> >"
+       ]
+      }
+     ],
+     "prompt_number": 17
     }
    ],
    "metadata": {}