71fef458e1
This is to workaround differences in minidom's pretty-printing that occurred between Python 3.7 and 3.8. * python/spot/jupyter.py (SVG): New class. * python/spot/__init__.py: Use it. * tests/python/_altscc.ipynb, tests/python/alternation.ipynb, tests/python/automata.ipynb, tests/python/formulas.ipynb, tests/python/gen.ipynb, tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb, tests/python/product.ipynb, tests/python/randaut.ipynb, tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb, tests/python/word.ipynb: Adjust.
749 lines
48 KiB
Text
749 lines
48 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"from IPython.display import display, HTML\n",
|
|
"import spot\n",
|
|
"spot.setup()"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"To translate a formula into a Testing Automaton\n",
|
|
"\n",
|
|
"Start by building a Buchi automaton"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"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=\"171pt\" height=\"125pt\"\n",
|
|
" viewBox=\"0.00 0.00 171.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120.8)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 167,-120.8 167,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"58.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</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\">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,-22C2.79,-22 17.15,-22 30.63,-22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22 30.94,-25.15 34.44,-22 30.94,-22 30.94,-22 30.94,-22 34.44,-22 30.94,-18.85 37.94,-22 37.94,-22\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M49.62,-39.04C48.32,-48.86 50.45,-58 56,-58 60.17,-58 62.4,-52.86 62.71,-46.14\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-39.04 65.85,-45.88 62.54,-42.53 62.71,-46.03 62.71,-46.03 62.71,-46.03 62.54,-42.53 59.56,-46.18 62.38,-39.04 62.38,-39.04\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"52.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</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\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M74.2,-22C85.07,-22 99.39,-22 111.89,-22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"119,-22 112,-25.15 115.5,-22 112,-22 112,-22 112,-22 115.5,-22 112,-18.85 119,-22 119,-22\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M132.99,-42.58C131.89,-52.84 134.55,-62 141,-62 145.83,-62 148.54,-56.85 149.13,-49.95\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"149.01,-42.58 152.27,-49.53 149.06,-46.08 149.12,-49.58 149.12,-49.58 149.12,-49.58 149.06,-46.08 145.97,-49.63 149.01,-42.58 149.01,-42.58\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"136.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">b</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 0x7f930090abd0> >"
|
|
]
|
|
},
|
|
"execution_count": 2,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"f = spot.formula('a U Gb')\n",
|
|
"a = f.translate('ba')\n",
|
|
"a"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Then, gather all the atomic proposition in the formula, and create an automaton with changesets"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"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",
|
|
"<!-- Title: G Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"265pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 265.23\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7042253521126761 0.7042253521126761) rotate(0) translate(4 372)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-372 1036.55,-372 1036.55,4 -4,4\"/>\n",
|
|
"<!-- 0 -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-252\" rx=\"27\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"118\" y=\"-248.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-252C63.46,-252 73.96,-252 83.7,-252\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-252 83.97,-255.15 87.47,-252 83.97,-252 83.97,-252 83.97,-252 87.47,-252 83.97,-248.85 90.97,-252 90.97,-252\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"540.97\" cy=\"-197\" rx=\"37.45\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-185.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>1->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M134.19,-266.68C169.2,-298.67 258.8,-370.27 340.71,-350 413,-332.11 429.98,-313.63 482.66,-261 491.6,-252.07 492.34,-248.51 500.66,-239 504.91,-234.14 509.52,-229.06 514.04,-224.18\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"518.88,-218.98 516.42,-226.25 516.5,-221.54 514.11,-224.1 514.11,-224.1 514.11,-224.1 516.5,-221.54 511.81,-221.96 518.88,-218.98 518.88,-218.98\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-356.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"250.36\" cy=\"-156\" rx=\"35.21\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M136.85,-238.85C157.77,-223.45 192.79,-197.66 218.21,-178.94\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"224.13,-174.58 220.36,-181.27 221.31,-176.65 218.49,-178.73 218.49,-178.73 218.49,-178.73 221.31,-176.65 216.62,-176.19 224.13,-174.58 224.13,-174.58\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"180\" y=\"-221.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"396.19\" cy=\"-197\" rx=\"37.45\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-185.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.88,-248.75C186.53,-243.23 270.85,-230.86 340.71,-213 345.2,-211.85 349.88,-210.59 354.53,-209.28\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"361.29,-207.36 355.42,-212.31 357.92,-208.32 354.56,-209.28 354.56,-209.28 354.56,-209.28 357.92,-208.32 353.69,-206.25 361.29,-207.36 361.29,-207.36\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"687.63\" cy=\"-147\" rx=\"35.23\" ry=\"26.76\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"687.63\" cy=\"-147\" rx=\"39.21\" ry=\"30.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M575.16,-185.53C595.79,-178.4 622.52,-169.16 644.62,-161.52\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"651.32,-159.2 645.74,-164.47 648.02,-160.35 644.71,-161.49 644.71,-161.49 644.71,-161.49 648.02,-160.35 643.68,-158.51 651.32,-159.2 651.32,-159.2\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"835.46\" cy=\"-148\" rx=\"37.46\" ry=\"26.76\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"835.46\" cy=\"-148\" rx=\"41.45\" ry=\"30.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->6 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>2->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M574.75,-209.11C612.29,-221.14 675.27,-235.72 726.98,-220 755.27,-211.4 782.88,-192.61 803.03,-176.38\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"808.51,-171.88 805.1,-178.76 805.81,-174.1 803.1,-176.32 803.1,-176.32 803.1,-176.32 805.81,-174.1 801.11,-173.89 808.51,-171.88 808.51,-171.88\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-229.8\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node8\" class=\"node\">\n",
|
|
"<title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"988.24\" cy=\"-61\" rx=\"37.46\" ry=\"26.76\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"988.24\" cy=\"-61\" rx=\"41.45\" ry=\"30.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->7 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>2->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M562.66,-174.54C582.69,-154.1 614.86,-124.51 648.27,-107 742.55,-57.61 870.96,-54.83 939.5,-57.6\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"946.75,-57.93 939.62,-60.76 943.25,-57.77 939.76,-57.61 939.76,-57.61 939.76,-57.61 943.25,-57.77 939.9,-54.47 946.75,-57.93 946.75,-57.93\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node9\" class=\"node\">\n",
|
|
"<title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"988.24\" cy=\"-269\" rx=\"40.13\" ry=\"26.76\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"988.24\" cy=\"-269\" rx=\"44.11\" ry=\"30.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-272.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"988.24\" y=\"-257.8\" font-family=\"Lato\" font-size=\"14.00\">!a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->8 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>2->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M568.11,-215.9C577.57,-222.05 588.56,-228.46 599.27,-233 619.92,-241.74 626.28,-240.66 648.27,-245 712.53,-257.69 728.75,-261.13 793.98,-267 838.69,-271.02 850.06,-269.33 894.94,-270 908.32,-270.2 922.8,-270.16 936.23,-270.02\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"943.57,-269.93 936.61,-273.17 940.07,-269.97 936.58,-270.02 936.58,-270.02 936.58,-270.02 940.07,-269.97 936.54,-266.87 943.57,-269.93 943.57,-269.93\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-268.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->2 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>3->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M284.42,-148.77C321.3,-141.95 382.51,-134.36 433.66,-146 459.24,-151.82 485.84,-164.59 506.04,-175.89\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"512.36,-179.5 504.72,-178.77 509.32,-177.77 506.28,-176.03 506.28,-176.03 506.28,-176.03 509.32,-177.77 507.85,-173.3 512.36,-179.5 512.36,-179.5\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-149.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>3->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M237.35,-181.37C236.45,-191.92 240.79,-200.87 250.36,-200.87 257.68,-200.87 261.94,-195.63 263.13,-188.43\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"263.36,-181.37 266.28,-188.47 263.25,-184.87 263.14,-188.37 263.14,-188.37 263.14,-188.37 263.25,-184.87 259.99,-188.26 263.36,-181.37 263.36,-181.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"250.36\" y=\"-204.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>3->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M277.29,-173.59C285.43,-178.34 294.66,-183 303.71,-186 318.72,-190.97 335.77,-193.75 351.05,-195.28\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"358.4,-195.93 351.14,-198.45 354.91,-195.62 351.42,-195.31 351.42,-195.31 351.42,-195.31 354.91,-195.62 351.7,-192.17 358.4,-195.93 358.4,-195.93\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-197.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->5 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\">\n",
|
|
"<title>3->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M281.96,-143.82C289,-141.48 296.53,-139.35 303.71,-138 424.23,-115.34 569.82,-130 641.82,-139.97\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"648.98,-140.98 641.61,-143.12 645.51,-140.49 642.05,-140 642.05,-140 642.05,-140 645.51,-140.49 642.49,-136.88 648.98,-140.98 648.98,-140.98\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-130.8\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M267.59,-132.3C291.51,-100.51 339.45,-48 395.19,-48 395.19,-48 395.19,-48 615.77,-48 686.6,-48 759.6,-91.92 800.78,-121.55\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"806.62,-125.81 799.11,-124.23 803.8,-123.74 800.97,-121.68 800.97,-121.68 800.97,-121.68 803.8,-123.74 802.82,-119.14 806.62,-125.81 806.62,-125.81\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-51.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\">\n",
|
|
"<title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M261.15,-130.24C279.87,-85.93 325.19,0 395.19,0 395.19,0 395.19,0 836.46,0 877.85,0 921.27,-20 950.83,-37.09\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"956.93,-40.69 949.3,-39.84 953.91,-38.91 950.9,-37.13 950.9,-37.13 950.9,-37.13 953.91,-38.91 952.5,-34.42 956.93,-40.69 956.93,-40.69\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->8 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\">\n",
|
|
"<title>3->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M264.51,-180.92C279.97,-210.18 303.55,-254.79 303.71,-255 337.27,-297.69 340.88,-336 395.19,-336 395.19,-336 395.19,-336 836.46,-336 878.45,-336 921.78,-314.04 951.16,-295.26\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"957.21,-291.31 953.07,-297.77 954.28,-293.22 951.35,-295.14 951.35,-295.14 951.35,-295.14 954.28,-293.22 949.63,-292.5 957.21,-291.31 957.21,-291.31\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"614.77\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node10\" class=\"node\">\n",
|
|
"<title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"540.97\" cy=\"-275\" rx=\"40.11\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"540.97\" y=\"-263.8\" font-family=\"Lato\" font-size=\"14.00\">!a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->9 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>3->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M266.43,-180.23C284.59,-206.89 317.81,-248.31 358.71,-266 401.82,-284.65 456.18,-284.63 494.07,-281.36\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"501.42,-280.67 494.75,-284.46 497.94,-281 494.45,-281.33 494.45,-281.33 494.45,-281.33 497.94,-281 494.16,-278.19 501.42,-280.67 501.42,-280.67\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-285.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->2 -->\n",
|
|
"<g id=\"edge18\" class=\"edge\">\n",
|
|
"<title>4->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M433.96,-197C452.94,-197 476.24,-197 496.15,-197\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"503.32,-197 496.32,-200.15 499.82,-197 496.32,-197 496.32,-197 496.32,-197 499.82,-197 496.32,-193.85 503.32,-197 503.32,-197\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-200.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\">\n",
|
|
"<title>4->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M367.84,-179.29C359.43,-174.59 349.96,-169.99 340.71,-167 325.63,-162.12 308.48,-159.38 293.26,-157.85\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"285.96,-157.19 293.21,-154.68 289.45,-157.51 292.93,-157.82 292.93,-157.82 292.93,-157.82 289.45,-157.51 292.65,-160.96 285.96,-157.19 285.96,-157.19\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"322.21\" y=\"-170.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g id=\"edge19\" class=\"edge\">\n",
|
|
"<title>4->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M383.18,-222.37C382.28,-232.92 386.62,-241.87 396.19,-241.87 403.51,-241.87 407.77,-236.63 408.97,-229.43\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"409.2,-222.37 412.12,-229.47 409.08,-225.87 408.97,-229.37 408.97,-229.37 408.97,-229.37 409.08,-225.87 405.82,-229.26 409.2,-222.37 409.2,-222.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"396.19\" y=\"-245.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->9 -->\n",
|
|
"<g id=\"edge20\" class=\"edge\">\n",
|
|
"<title>4->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M426.43,-212.97C448.59,-225.08 479.21,-241.81 503.07,-254.84\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"509.29,-258.24 501.64,-257.65 506.22,-256.56 503.15,-254.88 503.15,-254.88 503.15,-254.88 506.22,-256.56 504.66,-252.12 509.29,-258.24 509.29,-258.24\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"467.16\" y=\"-245.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->5 -->\n",
|
|
"<g id=\"edge21\" class=\"edge\">\n",
|
|
"<title>5->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M674.16,-176.1C673.72,-186.94 678.21,-195.87 687.63,-195.87 694.84,-195.87 699.17,-190.64 700.6,-183.32\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"701.1,-176.1 703.76,-183.3 700.86,-179.59 700.61,-183.08 700.61,-183.08 700.61,-183.08 700.86,-179.59 697.47,-182.86 701.1,-176.1 701.1,-176.1\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"687.63\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->6 -->\n",
|
|
"<g id=\"edge22\" class=\"edge\">\n",
|
|
"<title>5->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M726.12,-140.17C732.4,-139.26 738.86,-138.49 744.98,-138 758.72,-136.91 762.26,-136.83 775.98,-138 780,-138.34 784.14,-138.81 788.3,-139.36\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"795.26,-140.36 787.88,-142.48 791.8,-139.86 788.33,-139.37 788.33,-139.37 788.33,-139.37 791.8,-139.86 788.78,-136.25 795.26,-140.36 795.26,-140.36\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-141.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->7 -->\n",
|
|
"<g id=\"edge23\" class=\"edge\">\n",
|
|
"<title>5->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M719.33,-128.04C739.78,-116.24 767.64,-101.7 793.98,-93 842.17,-77.09 899.84,-68.86 939.57,-64.75\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"946.77,-64.04 940.12,-67.87 943.29,-64.38 939.81,-64.73 939.81,-64.73 939.81,-64.73 943.29,-64.38 939.49,-61.6 946.77,-64.04 946.77,-64.04\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge24\" class=\"edge\">\n",
|
|
"<title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M715.09,-169.77C735.44,-186.2 764.9,-207.74 793.98,-221 840.33,-242.13 897.34,-254.84 937.39,-261.82\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"944.66,-263.06 937.23,-264.99 941.21,-262.47 937.76,-261.88 937.76,-261.88 937.76,-261.88 941.21,-262.47 938.29,-258.78 944.66,-263.06 944.66,-263.06\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->5 -->\n",
|
|
"<g id=\"edge25\" class=\"edge\">\n",
|
|
"<title>6->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M793.93,-152.13C778.6,-153.21 760.99,-153.85 744.98,-153 741.39,-152.81 737.68,-152.55 733.95,-152.25\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"726.78,-151.62 734.03,-149.09 730.27,-151.92 733.75,-152.23 733.75,-152.23 733.75,-152.23 730.27,-151.92 733.48,-155.37 726.78,-151.62 726.78,-151.62\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"760.48\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g id=\"edge26\" class=\"edge\">\n",
|
|
"<title>6->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M821.6,-177.58C821.3,-188.21 825.92,-196.87 835.46,-196.87 842.76,-196.87 847.19,-191.79 848.72,-184.64\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"849.32,-177.58 851.87,-184.83 849.03,-181.07 848.73,-184.56 848.73,-184.56 848.73,-184.56 849.03,-181.07 845.59,-184.29 849.32,-177.58 849.32,-177.58\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"835.46\" y=\"-200.67\" font-family=\"Lato\" font-size=\"14.00\">{}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->7 -->\n",
|
|
"<g id=\"edge27\" class=\"edge\">\n",
|
|
"<title>6->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M869.33,-129.97C886.31,-120.58 907.32,-108.82 925.94,-98 933.5,-93.61 941.53,-88.84 949.2,-84.23\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"955.54,-80.41 951.18,-86.72 952.55,-82.21 949.55,-84.02 949.55,-84.02 949.55,-84.02 952.55,-82.21 947.92,-81.32 955.54,-80.41 955.54,-80.41\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"910.44\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->8 -->\n",
|
|
"<g id=\"edge28\" class=\"edge\">\n",
|
|
"<title>6->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M864.75,-170.29C882.39,-184.23 905.54,-202.59 925.94,-219 934.89,-226.2 944.53,-234.03 953.47,-241.32\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"958.92,-245.77 951.51,-243.78 956.21,-243.56 953.5,-241.34 953.5,-241.34 953.5,-241.34 956.21,-243.56 955.49,-238.9 958.92,-245.77 958.92,-245.77\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"910.44\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.jupyter.SVG object>"
|
|
]
|
|
},
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"propset = spot.atomic_prop_collect_as_bdd(f, a)\n",
|
|
"ta = spot.tgba_to_ta(a, propset, True, True, False, False, True)\n",
|
|
"ta.show('.A')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by `{}`), marking as *livelock accepting* (rectangles) any states from which there exists a an accepting path labeled by `{}`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 4,
|
|
"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",
|
|
"<!-- Title: G Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"136pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 135.62\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.9523809523809523 0.9523809523809523) rotate(0) translate(4 139)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-139 769.95,-139 769.95,4 -4,4\"/>\n",
|
|
"<!-- 0 -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-61\" rx=\"27\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"118\" y=\"-57.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-61C63.46,-61 73.96,-61 83.7,-61\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-61 83.97,-64.15 87.47,-61 83.97,-61 83.97,-61 83.97,-61 87.47,-61 83.97,-57.85 90.97,-61 90.97,-61\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"537.95,-131 483.95,-131 483.95,-93 537.95,-93 537.95,-131\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>1->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M140.65,-71.23C147.68,-74.31 155.58,-77.53 163,-80 240.62,-105.87 260.75,-113.38 342,-123 375.08,-126.92 383.65,-123.68 416.95,-123 438.74,-122.56 444.32,-123.64 465.95,-121 469.35,-120.59 472.88,-120.05 476.4,-119.44\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"483.54,-118.12 477.23,-122.49 480.1,-118.76 476.66,-119.39 476.66,-119.39 476.66,-119.39 480.1,-118.76 476.09,-116.3 483.54,-118.12 483.54,-118.12\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"269,-80 215,-80 215,-42 269,-42 269,-80\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"242\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"242\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M145.17,-61C163.51,-61 188.15,-61 207.86,-61\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"214.87,-61 207.87,-64.15 211.37,-61 207.87,-61 207.87,-61 207.87,-61 211.37,-61 207.87,-57.85 214.87,-61 214.87,-61\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"180\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"379.48\" cy=\"-55\" rx=\"37.45\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-58.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-43.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M138.75,-49.17C157.59,-38.62 187.14,-23.95 215,-18 258.44,-8.72 308.19,-23.66 341.29,-37.24\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"348.09,-40.1 340.42,-40.29 344.87,-38.74 341.64,-37.38 341.64,-37.38 341.64,-37.38 344.87,-38.74 342.87,-34.48 348.09,-40.1 348.09,-40.1\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"242\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"647.95,-102 593.95,-102 593.95,-64 647.95,-64 647.95,-102\"/>\n",
|
|
"<polygon fill=\"none\" stroke=\"black\" points=\"651.95,-106 589.95,-106 589.95,-60 651.95,-60 651.95,-106\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"620.95\" y=\"-86.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"620.95\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M538.1,-104.98C551.51,-101.38 568.08,-96.93 582.79,-92.98\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"589.85,-91.08 583.9,-95.94 586.47,-91.99 583.09,-92.9 583.09,-92.9 583.09,-92.9 586.47,-91.99 582.27,-89.86 589.85,-91.08 589.85,-91.08\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"563.95\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->2 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>3->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.32,-71.84C275.09,-74.03 281.21,-76.21 287,-78 352.37,-98.25 432.39,-106.7 476.6,-110.02\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"483.64,-110.53 476.43,-113.16 480.15,-110.28 476.66,-110.02 476.66,-110.02 476.66,-110.02 480.15,-110.28 476.89,-106.88 483.64,-110.53 483.64,-110.53\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"379.48\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>3->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.01,-48.43C274.8,-46.18 281.01,-44.18 287,-43 303.35,-39.78 321.53,-41.17 337.34,-43.94\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"344.42,-45.3 336.96,-47.07 340.99,-44.64 337.55,-43.98 337.55,-43.98 337.55,-43.98 340.99,-44.64 338.14,-40.88 344.42,-45.3 344.42,-45.3\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"761.95,-64 707.95,-64 707.95,-26 761.95,-26 761.95,-64\"/>\n",
|
|
"<polygon fill=\"none\" stroke=\"black\" points=\"765.95,-68 703.95,-68 703.95,-22 765.95,-22 765.95,-68\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"734.95\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"734.95\" y=\"-33.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M268.45,-41.7C294.6,-23.83 337.21,0 378.48,0 378.48,0 378.48,0 621.95,0 648.54,0 676.28,-11.05 697.51,-22.2\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"703.88,-25.65 696.22,-25.09 700.8,-23.99 697.72,-22.32 697.72,-22.32 697.72,-22.32 700.8,-23.99 699.22,-19.55 703.88,-25.65 703.88,-25.65\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"510.95\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->2 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M413.28,-67.14C429.33,-73.3 448.82,-81.14 465.95,-89 469.67,-90.7 473.51,-92.57 477.32,-94.47\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"483.65,-97.69 475.98,-97.32 480.53,-96.1 477.41,-94.51 477.41,-94.51 477.41,-94.51 480.53,-96.1 478.84,-91.71 483.65,-97.69 483.65,-97.69\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"450.45\" y=\"-92.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>4->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M341.85,-57.11C335.89,-57.42 329.77,-57.73 324,-58 308.44,-58.72 291.19,-59.37 276.62,-59.89\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"269.27,-60.15 276.16,-56.75 272.77,-60.02 276.27,-59.9 276.27,-59.9 276.27,-59.9 272.77,-60.02 276.38,-63.05 269.27,-60.15 269.27,-60.15\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-62.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->6 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>5->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M645.79,-59.86C653,-54.26 661.31,-49.02 669.95,-46 678.31,-43.08 687.67,-41.88 696.59,-41.61\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"703.63,-41.58 696.64,-44.76 700.13,-41.6 696.63,-41.61 696.63,-41.61 696.63,-41.61 700.13,-41.6 696.62,-38.46 703.63,-41.58 703.63,-41.58\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"677.95\" y=\"-49.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->5 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>6->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M703.86,-55.21C690.04,-59.9 673.52,-65.51 658.94,-70.45\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"651.97,-72.82 657.58,-67.58 655.28,-71.69 658.6,-70.57 658.6,-70.57 658.6,-70.57 655.28,-71.69 659.61,-73.55 651.97,-72.82 651.97,-72.82\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"677.95\" y=\"-69.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.jupyter.SVG object>"
|
|
]
|
|
},
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"ta = spot.tgba_to_ta(a, propset, True, True, False, False, False)\n",
|
|
"ta.show('.A')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Finally, use bisimulation to minimize the number of states."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"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",
|
|
"<!-- Title: G Pages: 1 -->\n",
|
|
"<svg width=\"639pt\" height=\"184pt\"\n",
|
|
" viewBox=\"0.00 0.00 639.00 184.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 180)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-180 635,-180 635,4 -4,4\"/>\n",
|
|
"<!-- 0 -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"118\" cy=\"-153\" rx=\"27\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"118\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">init</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M54.22,-153C63.46,-153 73.96,-153 83.7,-153\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"90.97,-153 83.97,-156.15 87.47,-153 83.97,-153 83.97,-153 83.97,-153 87.47,-153 83.97,-149.85 90.97,-153 90.97,-153\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"517,-105 463,-105 463,-69 517,-69 517,-105\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"490\" y=\"-83.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>1->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.03,-158.27C150.2,-159.37 156.82,-160.38 163,-161 186,-163.3 191.89,-161.78 215,-162 295.98,-162.78 317.88,-162.36 396,-141 418.53,-134.84 424.74,-133.62 445,-122 451.22,-118.43 457.5,-114.02 463.29,-109.56\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"468.89,-105.1 465.37,-111.92 466.15,-107.28 463.41,-109.46 463.41,-109.46 463.41,-109.46 466.15,-107.28 461.45,-106.99 468.89,-105.1 468.89,-105.1\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"269,-103 215,-103 215,-67 269,-67 269,-103\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"242\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M137.53,-140.08C145.27,-134.87 154.44,-128.94 163,-124 177.67,-115.54 194.41,-107.02 208.62,-100.12\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"214.95,-97.07 210.01,-102.94 211.8,-98.59 208.64,-100.11 208.64,-100.11 208.64,-100.11 211.8,-98.59 207.27,-97.27 214.95,-97.07 214.95,-97.07\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"180\" y=\"-127.8\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"369\" cy=\"-114\" rx=\"27\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"369\" y=\"-110.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M145.11,-151.04C184.28,-147.81 260.45,-140.33 324,-127 328.4,-126.08 333,-124.93 337.49,-123.7\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"344.43,-121.72 338.56,-126.67 341.06,-122.68 337.7,-123.64 337.7,-123.64 337.7,-123.64 341.06,-122.68 336.83,-120.61 344.43,-121.72 344.43,-121.72\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"242\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"627,-40 573,-40 573,-4 627,-4 627,-40\"/>\n",
|
|
"<polygon fill=\"none\" stroke=\"black\" points=\"631,-44 569,-44 569,0 631,0 631,-44\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"600\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M517.14,-71.27C530.8,-63.05 547.73,-52.86 562.64,-43.88\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"568.89,-40.12 564.52,-46.43 565.89,-41.92 562.9,-43.73 562.9,-43.73 562.9,-43.73 565.89,-41.92 561.27,-41.03 568.89,-40.12 568.89,-40.12\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"543\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->2 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>3->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.03,-80.64C274.93,-79.71 281.17,-78.78 287,-78 335.09,-71.56 347.64,-68.12 396,-72 415.83,-73.59 437.81,-77.05 455.42,-80.25\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"462.68,-81.6 455.22,-83.42 459.24,-80.96 455.8,-80.32 455.8,-80.32 455.8,-80.32 459.24,-80.96 456.37,-77.23 462.68,-81.6 462.68,-81.6\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"369\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>3->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.08,-81.75C285.23,-80.6 306.21,-80.7 324,-86 331.29,-88.17 338.53,-91.93 344.97,-96.01\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"351.12,-100.14 343.55,-98.85 348.22,-98.18 345.31,-96.23 345.31,-96.23 345.31,-96.23 348.22,-98.18 347.07,-93.62 351.12,-100.14 351.12,-100.14\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-89.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->5 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M269.26,-74.49C275.04,-72.45 281.17,-70.48 287,-69 384.49,-44.2 502.67,-30.79 561.68,-25.2\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"568.92,-24.52 562.25,-28.31 565.44,-24.85 561.95,-25.17 561.95,-25.17 561.95,-25.17 565.44,-24.85 561.66,-22.04 568.92,-24.52 568.92,-24.52\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"429.5\" y=\"-47.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->2 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M394.95,-108.34C412.67,-104.32 436.65,-98.88 455.97,-94.49\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"462.85,-92.93 456.72,-97.55 459.44,-93.71 456.02,-94.48 456.02,-94.48 456.02,-94.48 459.44,-93.71 455.33,-91.41 462.85,-92.93 462.85,-92.93\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"429.5\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">{a, b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>4->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M342.21,-111.13C326.16,-109.03 305.2,-105.72 287,-101 283.45,-100.08 279.79,-98.99 276.16,-97.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"269.27,-95.47 276.91,-94.74 272.58,-96.6 275.9,-97.72 275.9,-97.72 275.9,-97.72 272.58,-96.6 274.88,-100.7 269.27,-95.47 269.27,-95.47\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"305.5\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">{b}</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->5 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>5->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M589.63,-44.21C588.78,-53.8 592.23,-62 600,-62 605.7,-62 609.08,-57.58 610.14,-51.43\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"610.37,-44.21 613.29,-51.31 610.26,-47.71 610.15,-51.21 610.15,-51.21 610.15,-51.21 610.26,-47.71 607,-51.11 610.37,-44.21 610.37,-44.21\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"600\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">{a}</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.jupyter.SVG object>"
|
|
]
|
|
},
|
|
"execution_count": 5,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"spot.minimize_ta(ta).show('.A')"
|
|
]
|
|
}
|
|
],
|
|
"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.7.5"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 2
|
|
}
|