e146527852
* spot/twaalgos/emptiness.hh, spot/twaalgos/emptiness.cc: Add the method. * tests/python/highlighting.ipynb: Add a small test.
670 lines
No EOL
43 KiB
Text
670 lines
No EOL
43 KiB
Text
{
|
|
"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.4.3+"
|
|
},
|
|
"name": ""
|
|
},
|
|
"nbformat": 3,
|
|
"nbformat_minor": 0,
|
|
"worksheets": [
|
|
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"import spot\n",
|
|
"spot.setup()"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 1
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a = spot.translate('a U b U c')"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 2
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The `#` option of `print_dot()` can be used to display the internal number of each transition "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a.show('.#')"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 3,
|
|
"svg": [
|
|
"<svg height=\"139pt\" viewBox=\"0.00 0.00 307.00 139.00\" width=\"307pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 135)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-135 303,-135 303,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>2</title>\n",
|
|
"<ellipse cx=\"56\" cy=\"-76\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-72.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->2</title>\n",
|
|
"<path d=\"M1.15491,-76C2.79388,-76 17.1543,-76 30.6317,-76\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"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\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>2->2</title>\n",
|
|
"<path d=\"M49.6208,-93.0373C48.3189,-102.858 50.4453,-112 56,-112 60.166,-112 62.4036,-106.858 62.7128,-100.143\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"62.3792,-93.0373 65.8541,-99.8818 62.5434,-96.5335 62.7076,-100.03 62.7076,-100.03 62.7076,-100.03 62.5434,-96.5335 59.561,-100.177 62.3792,-93.0373 62.3792,-93.0373\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-115.8\">a & !c</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"41.1208\" y=\"-96.8373\">#6</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"277\" cy=\"-76\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<ellipse cx=\"277\" cy=\"-76\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"277\" y=\"-72.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->0</title>\n",
|
|
"<path d=\"M74.071,-77.7575C79.7664,-78.2653 86.1506,-78.7498 92,-79 147.13,-81.3584 211.623,-79.169 247.752,-77.4948\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"255.018,-77.1472 248.176,-80.6282 251.522,-77.3145 248.026,-77.4818 248.026,-77.4818 248.026,-77.4818 251.522,-77.3145 247.875,-74.3354 255.018,-77.1472 255.018,-77.1472\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-82.8\">c</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"82.571\" y=\"-66.5575\">#4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
|
|
"<ellipse cx=\"194\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.5\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>2->1</title>\n",
|
|
"<path d=\"M72.8671,-69.2332C97.0256,-58.9303 143.124,-39.2707 170.658,-27.5281\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"177.234,-24.7237 172.031,-30.3673 174.015,-26.0968 170.795,-27.4698 170.795,-27.4698 170.795,-27.4698 174.015,-26.0968 169.559,-24.5723 177.234,-24.7237 177.234,-24.7237\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-63.8\">!a & b & !c</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"81.3671\" y=\"-58.0332\">#5</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M269.317,-96.9908C268.369,-107.087 270.93,-116 277,-116 281.553,-116 284.131,-110.987 284.736,-104.22\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"284.683,-96.9908 287.884,-103.967 284.709,-100.491 284.734,-103.991 284.734,-103.991 284.734,-103.991 284.709,-100.491 281.585,-104.014 284.683,-96.9908 284.683,-96.9908\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272.5\" y=\"-119.8\">1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"260.817\" y=\"-100.791\">#1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>1->0</title>\n",
|
|
"<path d=\"M209.109,-28.1028C221.166,-36.7361 238.75,-49.3269 252.863,-59.4329\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"258.673,-63.5931 251.148,-62.0789 255.827,-61.5555 252.982,-59.5178 252.982,-59.5178 252.982,-59.5178 255.827,-61.5555 254.816,-56.9566 258.673,-63.5931 258.673,-63.5931\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230\" y=\"-50.8\">c</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"217.609\" y=\"-31.9028\">#2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->1</title>\n",
|
|
"<path d=\"M187.266,-35.0373C185.892,-44.8579 188.137,-54 194,-54 198.397,-54 200.759,-48.8576 201.086,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"200.734,-35.0373 204.226,-41.8728 200.907,-38.533 201.08,-42.0287 201.08,-42.0287 201.08,-42.0287 200.907,-38.533 197.934,-42.1847 200.734,-35.0373 200.734,-35.0373\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.5\" y=\"-57.8\">b & !c</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"178.766\" y=\"-38.8373\">#3</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>"
|
|
],
|
|
"text": [
|
|
"<IPython.core.display.SVG object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 3
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Using these numbers you can selectively hightlight some transitions. The second argument is a color number (from a list of predefined colors)."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a.highlight_edges([2, 4, 5], 1)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 4,
|
|
"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=\"307pt\" height=\"139pt\"\n",
|
|
" viewBox=\"0.00 0.00 307.00 139.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 135)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-135 303,-135 303,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>2</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\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->2 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->2</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",
|
|
"<!-- 2->2 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-93.0373C48.3189,-102.858 50.4453,-112 56,-112 60.166,-112 62.4036,-106.858 62.7128,-100.143\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-93.0373 65.8541,-99.8818 62.5434,-96.5335 62.7076,-100.03 62.7076,-100.03 62.7076,-100.03 62.5434,-96.5335 59.561,-100.177 62.3792,-93.0373 62.3792,-93.0373\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"38\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">a & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"277\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"277\" cy=\"-76\" rx=\"22\" ry=\"22\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"277\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->0 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>2->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M74.071,-77.7575C79.7664,-78.2653 86.1506,-78.7498 92,-79 147.13,-81.3584 211.623,-79.169 247.752,-77.4948\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"255.018,-77.1472 248.176,-80.6282 251.545,-77.8139 248.049,-77.9813 248.026,-77.4818 248.002,-76.9824 251.498,-76.8151 247.875,-74.3354 255.018,-77.1472 255.018,-77.1472\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"190.5\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node4\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"194\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"189.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>2->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M72.8671,-69.2332C97.0256,-58.9303 143.124,-39.2707 170.658,-27.5281\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"177.234,-24.7237 172.031,-30.3673 174.211,-26.5567 170.991,-27.9297 170.795,-27.4698 170.599,-27.0099 173.818,-25.6369 169.559,-24.5723 177.234,-24.7237 177.234,-24.7237\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-63.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.317,-96.9908C268.369,-107.087 270.93,-116 277,-116 281.553,-116 284.131,-110.987 284.736,-104.22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"284.683,-96.9908 287.884,-103.967 284.709,-100.491 284.734,-103.991 284.734,-103.991 284.734,-103.991 284.709,-100.491 281.585,-104.014 284.683,-96.9908 284.683,-96.9908\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"272.5\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>1->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M209.109,-28.1028C221.166,-36.7361 238.75,-49.3269 252.863,-59.4329\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"258.673,-63.5931 251.148,-62.0789 255.536,-61.962 252.691,-59.9243 252.982,-59.5178 253.273,-59.1113 256.119,-61.1489 254.816,-56.9566 258.673,-63.5931 258.673,-63.5931\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"230\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M187.266,-35.0373C185.892,-44.8579 188.137,-54 194,-54 198.397,-54 200.759,-48.8576 201.086,-42.1433\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"200.734,-35.0373 204.226,-41.8728 200.907,-38.533 201.08,-42.0287 201.08,-42.0287 201.08,-42.0287 200.907,-38.533 197.934,-42.1847 200.734,-35.0373 200.734,-35.0373\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"175.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">b & !c</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 0x7fd034659540> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 4
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Note that these `highlight_` functions work for edges and states, and come with both singular (changing the color of single state or edge) and plural versions.\n",
|
|
"\n",
|
|
"They modify the automaton in place."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a.highlight_edge(6, 2).highlight_states((0, 1), 0)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 5,
|
|
"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=\"307pt\" height=\"139pt\"\n",
|
|
" viewBox=\"0.00 0.00 307.00 139.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 135)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-135 303,-135 303,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>2</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\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->2 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->2</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",
|
|
"<!-- 2->2 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"#faa43a\" stroke-width=\"2\" d=\"M49.6208,-93.0373C48.3189,-102.858 50.4453,-112 56,-112 60.166,-112 62.4036,-106.858 62.7128,-100.143\"/>\n",
|
|
"<polygon fill=\"#faa43a\" stroke=\"#faa43a\" stroke-width=\"2\" points=\"62.3792,-93.0373 65.8541,-99.8818 63.0428,-96.51 63.207,-100.006 62.7076,-100.03 62.2081,-100.053 62.0439,-96.5569 59.561,-100.177 62.3792,-93.0373 62.3792,-93.0373\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"38\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">a & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#5da5da\" stroke-width=\"2\" cx=\"277\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"#5da5da\" stroke-width=\"2\" cx=\"277\" cy=\"-76\" rx=\"22\" ry=\"22\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"277\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->0 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>2->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M74.071,-77.7575C79.7664,-78.2653 86.1506,-78.7498 92,-79 147.13,-81.3584 211.623,-79.169 247.752,-77.4948\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"255.018,-77.1472 248.176,-80.6282 251.545,-77.8139 248.049,-77.9813 248.026,-77.4818 248.002,-76.9824 251.498,-76.8151 247.875,-74.3354 255.018,-77.1472 255.018,-77.1472\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"190.5\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node4\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#5da5da\" stroke-width=\"2\" cx=\"194\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"189.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>2->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M72.8671,-69.2332C97.0256,-58.9303 143.124,-39.2707 170.658,-27.5281\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"177.234,-24.7237 172.031,-30.3673 174.211,-26.5567 170.991,-27.9297 170.795,-27.4698 170.599,-27.0099 173.818,-25.6369 169.559,-24.5723 177.234,-24.7237 177.234,-24.7237\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-63.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.317,-96.9908C268.369,-107.087 270.93,-116 277,-116 281.553,-116 284.131,-110.987 284.736,-104.22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"284.683,-96.9908 287.884,-103.967 284.709,-100.491 284.734,-103.991 284.734,-103.991 284.734,-103.991 284.709,-100.491 281.585,-104.014 284.683,-96.9908 284.683,-96.9908\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"272.5\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>1->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f17cb0\" stroke-width=\"2\" d=\"M209.109,-28.1028C221.166,-36.7361 238.75,-49.3269 252.863,-59.4329\"/>\n",
|
|
"<polygon fill=\"#f17cb0\" stroke=\"#f17cb0\" stroke-width=\"2\" points=\"258.673,-63.5931 251.148,-62.0789 255.536,-61.962 252.691,-59.9243 252.982,-59.5178 253.273,-59.1113 256.119,-61.1489 254.816,-56.9566 258.673,-63.5931 258.673,-63.5931\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"230\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M187.266,-35.0373C185.892,-44.8579 188.137,-54 194,-54 198.397,-54 200.759,-48.8576 201.086,-42.1433\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"200.734,-35.0373 204.226,-41.8728 200.907,-38.533 201.08,-42.0287 201.08,-42.0287 201.08,-42.0287 200.907,-38.533 197.934,-42.1847 200.734,-35.0373 200.734,-35.0373\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"175.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">b & !c</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text": [
|
|
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fd034190180> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 5
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"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."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"b = spot.translate('X (F(Ga <-> b) & GF!b)'); b"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 6,
|
|
"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->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->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=\"black\" 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->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->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->1 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" 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=\"black\" stroke=\"black\" points=\"144.031,-121.664 147.601,-128.46 144.244,-125.158 144.456,-128.651 144.456,-128.651 144.456,-128.651 144.244,-125.158 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->2 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->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 & !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->3 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M155.109,-105C173.324,-105 202.31,-105 222.956,-105\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"230.149,-105 223.149,-108.15 226.649,-105 223.149,-105 223.149,-105 223.149,-105 226.649,-105 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 & 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->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M151.868,-93.9814C171.203,-78.6193 206.342,-50.7007 228.218,-33.3198\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"233.744,-28.9291 230.223,-35.75 231.004,-31.1064 228.264,-33.2837 228.264,-33.2837 228.264,-33.2837 231.004,-31.1064 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 & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->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->2 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\"><title>2->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->3 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\"><title>3->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 & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\"><title>3->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 & !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->2 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\"><title>4->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 & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\"><title>4->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 & 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 0x7fd034190240> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 6
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"r = spot.couvreur99(b).check().accepting_run(); r"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 7,
|
|
"text": [
|
|
"Prefix:\n",
|
|
" 0\n",
|
|
" | 1\n",
|
|
" 1\n",
|
|
" | !a & !b\n",
|
|
"Cycle:\n",
|
|
" 2\n",
|
|
" | !b\t{0}"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 7
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"r.highlight(5) # the parameter is a color number"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 8
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"b"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 9,
|
|
"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->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->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=\"black\" 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->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" d=\"M74.1418,-105C85.1153,-105 99.5214,-105 111.67,-105\"/>\n",
|
|
"<polygon fill=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"118.892,-105 111.892,-108.15 115.392,-105.5 111.892,-105.5 111.892,-105 111.892,-104.5 115.392,-104.5 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->1 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" 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=\"black\" stroke=\"black\" points=\"144.031,-121.664 147.601,-128.46 144.244,-125.158 144.456,-128.651 144.456,-128.651 144.456,-128.651 144.244,-125.158 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->2 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" 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=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"344.681,-187.252 340.492,-193.684 342.006,-189.563 339.06,-191.454 338.79,-191.033 338.52,-190.612 341.466,-188.722 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 & !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->3 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M155.109,-105C173.324,-105 202.31,-105 222.956,-105\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"230.149,-105 223.149,-108.15 226.649,-105 223.149,-105 223.149,-105 223.149,-105 226.649,-105 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 & 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->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M151.868,-93.9814C171.203,-78.6193 206.342,-50.7007 228.218,-33.3198\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"233.744,-28.9291 230.223,-35.75 231.004,-31.1064 228.264,-33.2837 228.264,-33.2837 228.264,-33.2837 231.004,-31.1064 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 & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->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->2 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\"><title>2->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"#f15854\" stroke-width=\"2\" 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=\"#f15854\" stroke=\"#f15854\" stroke-width=\"2\" points=\"367.672,-193.308 372.264,-199.459 368.919,-196.617 369.677,-200.034 369.189,-200.142 368.701,-200.25 367.943,-196.833 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->3 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\"><title>3->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 & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\"><title>3->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 & !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->2 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\"><title>4->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 & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\"><title>4->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 & 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 0x7fd034190240> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 9
|
|
}
|
|
],
|
|
"metadata": {}
|
|
}
|
|
]
|
|
} |