753d572e4d
* spot/twaalgos/dot.cc (print_dot): Add some detection of Mealy machines, and some code to render its I/O in a <table>. * tests/python/synthesis.ipynb: Adjust expected output. * tests/python/_mealy.ipynb: New file. * tests/Makefile.am: Add python/_mealy.ipynb. * NEWS: Mention the new feature.
421 lines
22 KiB
Text
421 lines
22 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"id": "99baf49c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"import spot\n",
|
|
"spot.setup()"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "066489fd",
|
|
"metadata": {},
|
|
"source": [
|
|
"Test the Mealy printer."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"id": "08d7d512",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"g = spot.ltl_to_game('G((a|c) <-> (b|d))', [\"b\", \"d\"])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"id": "4e5b66f4",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"text/plain": [
|
|
"True"
|
|
]
|
|
},
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"spot.solve_game(g)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 4,
|
|
"id": "ce2ff962",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"247pt\" height=\"212pt\"\n",
|
|
" viewBox=\"0.00 0.00 247.00 212.07\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 208.07)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-208.07 243,-208.07 243,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"8\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"29\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"<text text-anchor=\"start\" x=\"45\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"87\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
|
|
"<text text-anchor=\"start\" x=\"103\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) & (Inf(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"149\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
|
|
"<text text-anchor=\"start\" x=\"165\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"203\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
|
"<text text-anchor=\"start\" x=\"219\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
|
|
"<text text-anchor=\"start\" x=\"64\" y=\"-175.87\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"73.5\" cy=\"-75.07\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"73.5\" y=\"-71.37\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M18.65,-75.07C20.29,-75.07 34.65,-75.07 48.13,-75.07\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"55.44,-75.07 48.44,-78.22 51.94,-75.07 48.44,-75.07 48.44,-75.07 48.44,-75.07 51.94,-75.07 48.44,-71.92 55.44,-75.07 55.44,-75.07\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"194.5,-133.07 167.5,-115.07 194.5,-97.07 221.5,-115.07 194.5,-133.07\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"194.5\" y=\"-111.37\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M79.63,-92.21C84.76,-105.97 94.14,-124.4 109.5,-133.07 129.34,-144.27 155.4,-135.7 173.2,-126.96\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"179.82,-123.52 175.06,-129.54 176.72,-125.13 173.61,-126.75 173.61,-126.75 173.61,-126.75 176.72,-125.13 172.16,-123.95 179.82,-123.52 179.82,-123.52\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"110\" y=\"-156.87\" font-family=\"Lato\" font-size=\"14.00\">!a & !c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"121.5\" y=\"-141.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"194.5,-53.07 167.5,-35.07 194.5,-17.07 221.5,-35.07 194.5,-53.07\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"194.5\" y=\"-31.37\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M87.62,-63.58C93.86,-58.69 101.65,-53.37 109.5,-50.07 126.19,-43.04 146.1,-39.3 162.35,-37.32\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"169.53,-36.52 162.92,-40.42 166.05,-36.91 162.57,-37.29 162.57,-37.29 162.57,-37.29 166.05,-36.91 162.23,-34.16 169.53,-36.52 169.53,-36.52\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"117\" y=\"-68.87\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"121.5\" y=\"-53.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M176.84,-108.84C168.63,-105.81 158.58,-102.17 149.5,-99.07 132.27,-93.18 112.66,-86.92 97.82,-82.27\"/>\n",
|
|
"<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"90.95,-80.13 98.57,-79.21 94.44,-80.69 97.78,-81.74 97.63,-82.21 97.48,-82.69 94.14,-81.65 96.69,-85.22 90.95,-80.13 90.95,-80.13\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"109.5\" y=\"-117.87\" font-family=\"Lato\" font-size=\"14.00\">!b & !d</text>\n",
|
|
"<text text-anchor=\"start\" x=\"121.5\" y=\"-102.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->0 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>2->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M182.23,-25.06C165.46,-11.43 133.34,9.67 109.5,-5.07 93.56,-14.92 84.64,-34.46 79.8,-50.4\"/>\n",
|
|
"<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"77.85,-57.43 76.69,-49.84 78.31,-53.92 79.24,-50.55 79.72,-50.68 80.2,-50.82 79.27,-54.19 82.76,-51.52 77.85,-57.43 77.85,-57.43\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"116\" y=\"-23.87\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
|
|
"<text text-anchor=\"start\" x=\"121.5\" y=\"-8.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f720> >"
|
|
]
|
|
},
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"spot.highlight_strategy(g)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"id": "3bcbeef2",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"x = spot.apply_strategy(g, True, False)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 6,
|
|
"id": "47d298f0",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"117pt\" height=\"126pt\"\n",
|
|
" viewBox=\"0.00 0.00 117.00 126.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.0 1.0) rotate(0) translate(4 122)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-122 113,-122 113,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<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->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M52.76,-35.78C52.21,-45.31 53.29,-54 56,-54 57.99,-54 59.1,-49.32 59.33,-43.05\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"59.24,-35.78 62.48,-42.74 59.28,-39.28 59.33,-42.78 59.33,-42.78 59.33,-42.78 59.28,-39.28 56.18,-42.82 59.24,-35.78 59.24,-35.78\"/>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"5,-55.5 5,-74.5 48,-74.5 48,-55.5 5,-55.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"7\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">!a & !c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"52\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"63,-55.5 63,-74.5 107,-74.5 107,-55.5 63,-55.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"65\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">!b & !d</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M50.83,-35.41C47.6,-54.42 49.32,-77 56,-77 61.84,-77 63.89,-59.71 62.15,-42.65\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"61.17,-35.41 65.23,-41.93 61.64,-38.88 62.11,-42.35 62.11,-42.35 62.11,-42.35 61.64,-38.88 58.98,-42.77 61.17,-35.41 61.17,-35.41\"/>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"19,-78.5 19,-97.5 48,-97.5 48,-78.5 19,-78.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"21\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"52\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"63,-78.5 63,-97.5 94,-97.5 94,-78.5 63,-78.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"65\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f630> >"
|
|
]
|
|
},
|
|
"execution_count": 6,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"x"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 7,
|
|
"id": "f0d098ac",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"x.merge_edges()"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 8,
|
|
"id": "adf92ac7",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"121pt\" height=\"106pt\"\n",
|
|
" viewBox=\"0.00 0.00 121.00 106.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.0 1.0) rotate(0) translate(4 102)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-102 117,-102 117,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"60\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"60\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.17,-18C3.01,-18 19.75,-18 34.75,-18\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"41.9,-18 34.9,-21.15 38.4,-18 34.9,-18 34.9,-18 34.9,-18 38.4,-18 34.9,-14.85 41.9,-18 41.9,-18\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M52.97,-34.66C51.41,-44.62 53.75,-54 60,-54 64.69,-54 67.18,-48.73 67.47,-41.89\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"67.03,-34.66 70.6,-41.46 67.24,-38.16 67.46,-41.65 67.46,-41.65 67.46,-41.65 67.24,-38.16 64.31,-41.84 67.03,-34.66 67.03,-34.66\"/>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"9,-77 9,-96 52,-96 52,-77 9,-77\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"11\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!a & !c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"56\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"67,-77 67,-96 111,-96 111,-77 67,-77\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"69\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!b & !d</text>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"9,-56 9,-75 52,-75 52,-56 9,-56\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"25\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"56\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"67,-56 67,-75 111,-75 111,-56 67,-56\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"69\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f630> >"
|
|
]
|
|
},
|
|
"execution_count": 8,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"x"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 9,
|
|
"id": "6e8cd892",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"247pt\" height=\"204pt\"\n",
|
|
" viewBox=\"0.00 0.00 247.00 204.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.0 1.0) rotate(0) translate(4 200)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-200 243,-200 243,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"8\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"29\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"<text text-anchor=\"start\" x=\"45\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"87\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
|
|
"<text text-anchor=\"start\" x=\"103\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) & (Inf(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"149\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
|
|
"<text text-anchor=\"start\" x=\"165\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
|
|
"<text text-anchor=\"start\" x=\"203\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
|
"<text text-anchor=\"start\" x=\"219\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
|
|
"<text text-anchor=\"start\" x=\"64\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"123\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"123\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M64.17,-18C66.01,-18 82.75,-18 97.75,-18\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"104.9,-18 97.9,-21.15 101.4,-18 97.9,-18 97.9,-18 97.9,-18 101.4,-18 97.9,-14.85 104.9,-18 104.9,-18\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M119.4,-35.78C118.79,-45.31 119.99,-54 123,-54 125.21,-54 126.44,-49.32 126.7,-43.05\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"126.6,-35.78 129.85,-42.74 126.65,-39.28 126.7,-42.78 126.7,-42.78 126.7,-42.78 126.65,-39.28 123.55,-42.83 126.6,-35.78 126.6,-35.78\"/>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"72,-77 72,-96 115,-96 115,-77 72,-77\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"74\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!a & !c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"119\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"130,-77 130,-96 174,-96 174,-77 130,-77\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"132\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!b & !d</text>\n",
|
|
"<text text-anchor=\"start\" x=\"115\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M117.81,-35.4C113.5,-60.54 115.23,-98 123,-98 130.08,-98 132.14,-66.97 129.21,-42.44\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"128.19,-35.4 132.31,-41.88 128.69,-38.86 129.19,-42.33 129.19,-42.33 129.19,-42.33 128.69,-38.86 126.07,-42.78 128.19,-35.4 128.19,-35.4\"/>\n",
|
|
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"86,-121 86,-140 115,-140 115,-121 86,-121\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"88\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
|
|
"<text text-anchor=\"start\" x=\"119\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
|
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"130,-121 130,-140 161,-140 161,-121 130,-121\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"132\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
|
|
"<text text-anchor=\"start\" x=\"115.5\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d76e561e0> >"
|
|
]
|
|
},
|
|
"execution_count": 9,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"spot.apply_strategy(g, True, True)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "5948f923",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.9.2"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 5
|
|
}
|