Commit 3836ea8d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: more examples of highlighting

* tests/python/highlighting.ipynb: Augment.
parent d1aca565
......@@ -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",