alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/wrap/python/tests/automata.ipynb
Alexandre Duret-Lutz 3c38780d50 python: some bindings for translating formulas and diplaying automata 
* wrap/python/spot.py: Introduce spot.translate (and
spot.formula.translate) as well, as a wrapper around the
spot.translator class.  Also implement spot.tgba.show()
to allow passing argument to dotty_reachable() before
the result is converted to SVG.
* wrap/python/tests/automata.ipynb: New test file.
* wrap/python/tests/Makefile.am: Add it.
2015-03-15 19:50:40 +01:00

844 lines
No EOL
52 KiB
Text
Raw Blame History

{
"metadata": {
"name": "",
"signature": "sha256:6c1898261f2fab59f18fc3b6d75fe387d6f811b02935833fc74fa5e476796d4c"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.translate('(a U b) & GFc & GFd', 'BA', complete=True); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"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=\"488pt\" height=\"186pt\"\n",
" viewBox=\"0.00 0.00 488.00 186.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 182)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-182 484,-182 484,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65\" cy=\"-69\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-65.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-69C1.88296,-69 14.1126,-69 27.573,-69\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"27.9378,-72.5001 37.9378,-69 27.9378,-65.5001 27.9378,-72.5001\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-86.4099C55.6785,-96.0879 58.2969,-105 65,-105 69.1895,-105 71.7833,-101.519 72.7816,-96.5449\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"76.2824,-96.4351 72.8552,-86.4099 69.2826,-96.3842 76.2824,-96.4351\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-108.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"200\" cy=\"-109\" rx=\"27\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"200\" cy=\"-109\" rx=\"31\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"200\" y=\"-105.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M89.7777,-76.1512C109.694,-82.1411 138.477,-90.7975 161.495,-97.7204\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"160.704,-101.137 171.288,-100.666 162.72,-94.4338 160.704,-101.137\"/>\n",
"<text text-anchor=\"middle\" x=\"130.5\" y=\"-96.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node4\" class=\"node\"><title>4</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"200\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"200\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M88.8635,-60.2328C110.274,-52.0226 142.49,-39.6691 166.556,-30.4408\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"167.906,-33.6719 175.99,-26.8235 165.4,-27.1359 167.906,-33.6719\"/>\n",
"<text text-anchor=\"middle\" x=\"130.5\" y=\"-54.8\" font-family=\"Times,serif\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M188.354,-129.581C186.743,-139.845 190.625,-149 200,-149 206.006,-149 209.757,-145.243 211.254,-139.844\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"214.762,-139.707 211.646,-129.581 207.767,-139.44 214.762,-139.707\"/>\n",
"<text text-anchor=\"middle\" x=\"200\" y=\"-152.8\" font-family=\"Times,serif\" font-size=\"14.00\">c &amp; d</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node5\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"453\" cy=\"-99\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"453\" y=\"-95.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M222.782,-123.932C241.9,-136.075 270.957,-152.26 299,-159 322.335,-164.609 329.885,-165.458 353,-159 380.696,-151.262 408.36,-133.43 427.375,-119.205\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"429.683,-121.845 435.472,-112.972 425.413,-116.298 429.683,-121.845\"/>\n",
"<text text-anchor=\"middle\" x=\"326\" y=\"-166.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c &amp; d</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node6\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"326\" cy=\"-99\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"326\" y=\"-95.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M231.069,-108.727C246.096,-108.374 264.539,-107.612 281,-106 283.721,-105.734 286.529,-105.407 289.349,-105.043\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"290.071,-108.475 299.474,-103.594 289.079,-101.546 290.071,-108.475\"/>\n",
"<text text-anchor=\"middle\" x=\"265\" y=\"-111.8\" font-family=\"Times,serif\" font-size=\"14.00\">!d</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M188.75,-34.6641C186.25,-44.625 190,-54 200,-54 206.406,-54 210.247,-50.1525 211.524,-44.7682\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"215.02,-44.5656 211.25,-34.6641 208.022,-44.7552 215.02,-44.5656\"/>\n",
"<text text-anchor=\"middle\" x=\"200\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M431.922,-87.6352C412.452,-77.3145 381.724,-62.8411 353,-57 329.481,-52.2175 322.402,-51.6745 299,-57 274.468,-62.5828 249.456,-76.007 230.841,-87.8168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"228.696,-85.0376 222.246,-93.4432 232.53,-90.8942 228.696,-85.0376\"/>\n",
"<text text-anchor=\"middle\" x=\"326\" y=\"-60.8\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M442.102,-115.664C439.68,-125.625 443.312,-135 453,-135 459.206,-135 462.927,-131.152 464.164,-125.768\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"467.66,-125.569 463.898,-115.664 460.662,-125.752 467.66,-125.569\"/>\n",
"<text text-anchor=\"middle\" x=\"453\" y=\"-138.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M301.585,-90.8211C286.491,-86.65 266.488,-83.1832 249,-87 243.979,-88.0958 238.855,-89.7668 233.914,-91.7084\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"232.497,-88.508 224.713,-95.6958 235.281,-94.9308 232.497,-88.508\"/>\n",
"<text text-anchor=\"middle\" x=\"265\" y=\"-90.8\" font-family=\"Times,serif\" font-size=\"14.00\">c &amp; d</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M353.204,-99C371.371,-99 395.799,-99 415.82,-99\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"415.83,-102.5 425.83,-99 415.83,-95.5001 415.83,-102.5\"/>\n",
"<text text-anchor=\"middle\" x=\"389.5\" y=\"-102.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c &amp; d</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M315.453,-115.664C313.109,-125.625 316.625,-135 326,-135 332.006,-135 335.607,-131.152 336.804,-125.768\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"340.3,-125.572 336.547,-115.664 333.302,-125.75 340.3,-125.572\"/>\n",
"<text text-anchor=\"middle\" x=\"326\" y=\"-138.8\" font-family=\"Times,serif\" font-size=\"14.00\">!d</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f79a4a46090> >"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a.show(\"cs\")"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"svg": [
"<svg height=\"304pt\" viewBox=\"0.00 0.00 433.00 304.00\" width=\"433pt\" 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 300)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-300 429,-300 429,4 -4,4\" stroke=\"none\"/>\n",
"<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
"<polygon fill=\"none\" points=\"143,-101 143,-288 417,-288 417,-101 143,-101\" stroke=\"green\"/>\n",
"</g>\n",
"<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
"<polygon fill=\"none\" points=\"147,-8 147,-93 199,-93 199,-8 147,-8\" stroke=\"grey\"/>\n",
"</g>\n",
"<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
"<polygon fill=\"none\" points=\"30,-18 30,-103 82,-103 82,-18 30,-18\" stroke=\"red\"/>\n",
"</g>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-44\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.3\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
"<path d=\"M1.15491,-44C2.67247,-44 15.0966,-44 27.6277,-44\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"27.9419,-47.5001 37.9419,-44 27.9418,-40.5001 27.9419,-47.5001\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-61.0373C48.3189,-70.8579 50.4453,-80 56,-80 59.4717,-80 61.6042,-76.4289 62.3975,-71.3529\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"65.8971,-71.031 62.3792,-61.0373 58.8971,-71.0435 65.8971,-71.031\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-83.8\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"173\" cy=\"-151\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"173\" cy=\"-151\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"173\" y=\"-147.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
"<path d=\"M69.7464,-55.8597C88.766,-73.5562 124.882,-107.16 148.701,-129.321\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"146.559,-132.109 156.264,-136.359 151.327,-126.984 146.559,-132.109\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"112.5\" y=\"-117.8\">b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"173\" cy=\"-34\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"173\" y=\"-30.3\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
"<path d=\"M73.9686,-42.5245C92.6537,-40.8997 122.957,-38.2646 144.931,-36.3538\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"145.303,-39.8348 154.962,-35.4816 144.696,-32.8611 145.303,-39.8348\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"112.5\" y=\"-44.8\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
"<path d=\"M162.933,-170.757C161.223,-181.35 164.578,-191 173,-191 178.527,-191 181.872,-186.844 183.035,-180.993\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"186.536,-180.768 183.067,-170.757 179.536,-180.747 186.536,-180.768\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"173\" y=\"-194.8\">c &amp; d</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\"><title>3</title>\n",
"<ellipse cx=\"281.5\" cy=\"-178\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"281.5\" y=\"-174.3\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
"<path d=\"M195.066,-147.999C209.497,-146.73 228.868,-146.598 245,-152 250.121,-153.715 255.12,-156.465 259.675,-159.548\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"257.716,-162.454 267.801,-165.702 261.942,-156.874 257.716,-162.454\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"229\" y=\"-155.8\">!d</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"391\" cy=\"-178\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"391\" y=\"-174.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
"<path d=\"M194.285,-144.439C219.359,-137.275 263.224,-127.841 300,-136 323.861,-141.294 348.892,-153.602 366.481,-163.534\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"365.029,-166.739 375.432,-168.747 368.552,-160.69 365.029,-166.739\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"281.5\" y=\"-139.8\">!c &amp; d</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
"<path d=\"M263.344,-176.297C249.559,-174.669 229.796,-171.747 213,-167 209.76,-166.084 206.426,-164.981 203.135,-163.788\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"204.12,-160.415 193.532,-160.032 201.57,-166.934 204.12,-160.415\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"229\" y=\"-177.8\">c &amp; d</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
"<path d=\"M272.521,-193.916C270.179,-204.15 273.172,-214 281.5,-214 286.965,-214 290.133,-209.758 291.003,-203.949\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"294.496,-203.72 290.479,-193.916 287.505,-204.085 294.496,-203.72\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"281.5\" y=\"-217.8\">!d</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
"<path d=\"M299.772,-178C316.698,-178 342.762,-178 362.533,-178\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"362.771,-181.5 372.771,-178 362.771,-174.5 362.771,-181.5\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"336.5\" y=\"-181.8\">!c &amp; d</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
"<path d=\"M378.005,-190.867C355.777,-213.074 306.484,-254.687 263,-238 232.858,-226.434 207.584,-198.732 191.762,-177.671\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"194.474,-175.448 185.773,-169.403 188.805,-179.554 194.474,-175.448\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"281.5\" y=\"-244.8\">c</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
"<path d=\"M381.767,-193.541C379.169,-203.909 382.246,-214 391,-214 396.745,-214 400.045,-209.654 400.9,-203.736\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"404.379,-203.291 400.233,-193.541 397.394,-203.749 404.379,-203.291\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"391\" y=\"-217.8\">!c</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
"<path d=\"M163.425,-49.5414C160.73,-59.9087 163.922,-70 173,-70 178.958,-70 182.38,-65.654 183.267,-59.7362\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"186.744,-59.2812 182.575,-49.5414 179.76,-59.7557 186.744,-59.2812\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"173\" y=\"-73.8\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f79a5729400>"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('a U b'); f"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$a \\mathbin{\\mathsf{U}} b$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"text": [
"a U b"
]
}
],
"prompt_number": 4
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate(f)"
],
"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=\"205pt\" height=\"85pt\"\n",
" viewBox=\"0.00 0.00 205.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 201,-81 201,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-22C1.88296,-22 14.1126,-22 27.573,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"27.9378,-25.5001 37.9378,-22 27.9378,-18.5001 27.9378,-25.5001\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-39.4099C55.6785,-49.0879 58.2969,-58 65,-58 69.1895,-58 71.7833,-54.5187 72.7816,-49.5449\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"76.2824,-49.4351 72.8552,-39.4099 69.2826,-49.3842 76.2824,-49.4351\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"166\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"166\" cy=\"-22\" rx=\"31\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"166\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M92.0111,-22C101.996,-22 113.642,-22 124.66,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"124.957,-25.5001 134.957,-22 124.957,-18.5001 124.957,-25.5001\"/>\n",
"<text text-anchor=\"middle\" x=\"113.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M156.488,-42.9908C155.314,-53.0872 158.484,-62 166,-62 170.815,-62 173.846,-58.3422 175.095,-53.0587\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"178.595,-53.1272 175.512,-42.9908 171.601,-52.8372 178.595,-53.1272\"/>\n",
"<text text-anchor=\"middle\" x=\"166\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f79a4aa1810> >"
]
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate()"
],
"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=\"205pt\" height=\"85pt\"\n",
" viewBox=\"0.00 0.00 205.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 201,-81 201,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-22C1.88296,-22 14.1126,-22 27.573,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"27.9378,-25.5001 37.9378,-22 27.9378,-18.5001 27.9378,-25.5001\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-39.4099C55.6785,-49.0879 58.2969,-58 65,-58 69.1895,-58 71.7833,-54.5187 72.7816,-49.5449\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"76.2824,-49.4351 72.8552,-39.4099 69.2826,-49.3842 76.2824,-49.4351\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"166\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"166\" cy=\"-22\" rx=\"31\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"166\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M92.0111,-22C101.996,-22 113.642,-22 124.66,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"124.957,-25.5001 134.957,-22 124.957,-18.5001 124.957,-25.5001\"/>\n",
"<text text-anchor=\"middle\" x=\"113.5\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M156.488,-42.9908C155.314,-53.0872 158.484,-62 166,-62 170.815,-62 173.846,-58.3422 175.095,-53.0587\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"178.595,-53.1272 175.512,-42.9908 171.601,-52.8372 178.595,-53.1272\"/>\n",
"<text text-anchor=\"middle\" x=\"166\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f79a4aa1930> >"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('mon')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"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=\"197pt\" height=\"77pt\"\n",
" viewBox=\"0.00 0.00 197.00 77.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 73)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 193,-73 193,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"65\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-18C1.88296,-18 14.1126,-18 27.573,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"27.9378,-21.5001 37.9378,-18 27.9378,-14.5001 27.9378,-21.5001\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-35.4099C55.6785,-45.0879 58.2969,-54 65,-54 69.1895,-54 71.7833,-50.5187 72.7816,-45.5449\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"76.2824,-45.4351 72.8552,-35.4099 69.2826,-45.3842 76.2824,-45.4351\"/>\n",
"<text text-anchor=\"middle\" x=\"65\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"162\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"162\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M92.2106,-18C102.283,-18 113.965,-18 124.811,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"124.875,-21.5001 134.875,-18 124.875,-14.5001 124.875,-21.5001\"/>\n",
"<text text-anchor=\"middle\" x=\"113.5\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M153.431,-35.4099C151.831,-45.0879 154.688,-54 162,-54 166.57,-54 169.4,-50.5187 170.489,-45.5449\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"173.99,-45.4374 170.569,-35.4099 166.99,-45.3818 173.99,-45.4374\"/>\n",
"<text text-anchor=\"middle\" x=\"162\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f79a4aa18a0> >"
]
}
],
"prompt_number": 7
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('Ga | Gb | Gc'); f"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 8,
"text": [
"Ga | Gb | Gc"
]
}
],
"prompt_number": 8
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('ba', 'small').show('vc')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 9,
"svg": [
"<svg height=\"177pt\" viewBox=\"0.00 0.00 251.00 177.00\" width=\"251pt\" 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 173)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-173 247,-173 247,4 -4,4\" stroke=\"none\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"109\" cy=\"-113\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-109.3\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
"<path d=\"M109,-167.845C109,-166.328 109,-153.903 109,-141.372\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"112.5,-141.058 109,-131.058 105.5,-141.058 112.5,-141.058\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"22\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"22\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22\" y=\"-18.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M96.903,-99.6249C83.2988,-85.7079 60.9201,-62.8149 44.1599,-45.6694\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"46.3995,-42.9534 36.9064,-38.2491 41.3938,-47.8466 46.3995,-42.9534\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"77.5\" y=\"-65.8\">c</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"109\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"109\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109\" y=\"-18.3\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
"<path d=\"M109,-94.8399C109,-83.4407 109,-68.1336 109,-54.5781\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"112.5,-54.1905 109,-44.1905 105.5,-54.1906 112.5,-54.1905\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"112.5\" y=\"-65.8\">a</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"196\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"196\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196\" y=\"-18.3\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
"<path d=\"M121.097,-99.6249C134.701,-85.7079 157.08,-62.8149 173.84,-45.6694\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"176.606,-47.8466 181.094,-38.2491 171.6,-42.9534 176.606,-47.8466\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"160.5\" y=\"-65.8\">b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
"<path d=\"M42.5808,-30.3702C52.8447,-31.5284 62,-28.7383 62,-22 62,-17.6833 58.2427,-14.9869 52.8436,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"52.6729,-10.405 42.5808,-13.6298 52.4812,-17.4024 52.6729,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"65.5\" y=\"-18.3\">c</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
"<path d=\"M129.581,-30.3702C139.845,-31.5284 149,-28.7383 149,-22 149,-17.6833 145.243,-14.9869 139.844,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"139.673,-10.405 129.581,-13.6298 139.481,-17.4024 139.673,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"152.5\" y=\"-18.3\">a</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
"<path d=\"M216.581,-30.3702C226.845,-31.5284 236,-28.7383 236,-22 236,-17.6833 232.243,-14.9869 226.844,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"226.673,-10.405 216.581,-13.6298 226.481,-17.4024 226.673,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"239.5\" y=\"-18.3\">b</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f798ea6e9b0>"
]
}
],
"prompt_number": 9
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('ba', 'det').show('vc')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 12,
"svg": [
"<svg height=\"280pt\" viewBox=\"0.00 0.00 591.82 280.00\" width=\"592pt\" 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 276)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-276 587.821,-276 587.821,4 -4,4\" stroke=\"none\"/>\n",
"<!-- I -->\n",
"<!-- 6 -->\n",
"<g class=\"node\" id=\"node2\"><title>6</title>\n",
"<ellipse cx=\"277.821\" cy=\"-212\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"277.821\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"277.821\" y=\"-208.3\">6</text>\n",
"</g>\n",
"<!-- I&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
"<path d=\"M277.821,-270.834C277.821,-269.282 277.821,-257.111 277.821,-244.332\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"281.321,-244.144 277.821,-234.144 274.321,-244.144 281.321,-244.144\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 6&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
"<path d=\"M298.811,-219.317C308.908,-220.22 317.821,-217.781 317.821,-212 317.821,-208.296 314.163,-205.964 308.879,-205.004\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"308.918,-201.504 298.811,-204.683 308.695,-208.5 308.918,-201.504\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"346.321\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
"<ellipse cx=\"96.8206\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"96.8206\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"96.8206\" y=\"-18.3\">0</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
"<path d=\"M255.721,-208.524C196.826,-201.426 38.4848,-178.913 7.82057,-139 -19.6942,-103.186 34.0271,-61.1222 69.3557,-38.795\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"71.1909,-41.7753 77.8807,-33.5596 67.5277,-35.8104 71.1909,-41.7753\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"40.8206\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"323.821\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"323.821\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"323.821\" y=\"-18.3\">1</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
"<path d=\"M293.596,-196.107C299.73,-189.363 306.154,-180.909 309.821,-172 325.565,-133.743 327.14,-85.434 326.081,-54.3777\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"329.567,-53.9873 325.615,-44.1569 322.574,-54.3058 329.567,-53.9873\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"357.821\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"475.821\" cy=\"-22\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"475.821\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"475.821\" y=\"-18.3\">2</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
"<path d=\"M299.754,-207.718C353.012,-199.238 486.572,-174.735 510.821,-139 529.65,-111.25 511.455,-73.0765 495.046,-48.2235\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"497.724,-45.9426 489.153,-39.7138 491.969,-49.9277 497.724,-45.9426\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"550.821\" y=\"-113.3\">a &amp; !b &amp; !c</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"104.821\" cy=\"-117\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"104.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.821\" y=\"-113.3\">3</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
"<path d=\"M256.67,-205.151C235.049,-198.702 200.895,-187.194 173.821,-172 157.607,-162.901 141.147,-150.181 128.371,-139.372\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"130.4,-136.498 120.548,-132.602 125.819,-141.792 130.4,-136.498\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"204.321\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node7\"><title>4</title>\n",
"<ellipse cx=\"429.821\" cy=\"-117\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"429.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"429.821\" y=\"-113.3\">4</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
"<path d=\"M296.155,-199.782C322.631,-183.583 371.758,-153.525 402.512,-134.709\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"404.717,-137.462 411.421,-129.258 401.064,-131.491 404.717,-137.462\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"393.321\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node8\"><title>5</title>\n",
"<ellipse cx=\"216.821\" cy=\"-117\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<ellipse cx=\"216.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"216.821\" y=\"-113.3\">5</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
"<path d=\"M264.723,-194.191C259.599,-187.412 253.776,-179.446 248.821,-172 243.19,-163.539 237.415,-154.075 232.347,-145.463\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"235.215,-143.431 227.167,-136.54 229.161,-146.945 235.215,-143.431\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"279.321\" y=\"-160.8\">a &amp; !b &amp; c</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
"<path d=\"M117.401,-30.3702C127.665,-31.5284 136.821,-28.7383 136.821,-22 136.821,-17.6833 133.063,-14.9869 127.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"127.493,-10.405 117.401,-13.6298 127.302,-17.4024 127.493,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"140.321\" y=\"-18.3\">c</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
"<path d=\"M344.401,-30.3702C354.665,-31.5284 363.821,-28.7383 363.821,-22 363.821,-17.6833 360.063,-14.9869 354.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"354.493,-10.405 344.401,-13.6298 354.302,-17.4024 354.493,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"367.321\" y=\"-18.3\">b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
"<path d=\"M496.401,-30.3702C506.665,-31.5284 515.821,-28.7383 515.821,-22 515.821,-17.6833 512.063,-14.9869 506.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"506.493,-10.405 496.401,-13.6298 506.302,-17.4024 506.493,-10.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"519.321\" y=\"-18.3\">a</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>3-&gt;0</title>\n",
"<path d=\"M100.426,-95.0356C99.3798,-89.2207 98.3997,-82.8875 97.8206,-77 97.0968,-69.6426 96.724,-61.6951 96.5546,-54.2187\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"100.053,-54.0318 96.4353,-44.0737 93.0533,-54.1142 100.053,-54.0318\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"116.321\" y=\"-65.8\">!b &amp; c</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;1</title>\n",
"<path d=\"M118.176,-99.186C129.593,-85.226 145.463,-66.8933 153.821,-62 197.157,-36.6256 255.69,-27.7601 291.543,-24.6629\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"292.194,-28.1235 301.899,-23.8749 291.662,-21.1437 292.194,-28.1235\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"172.321\" y=\"-65.8\">b &amp; !c</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
"<path d=\"M125.401,-125.37C135.665,-126.528 144.821,-123.738 144.821,-117 144.821,-112.683 141.063,-109.987 135.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"135.493,-105.405 125.401,-108.63 135.302,-112.402 135.493,-105.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"160.821\" y=\"-113.3\">b &amp; c</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>4-&gt;1</title>\n",
"<path d=\"M420.21,-97.1109C413.838,-85.9186 404.665,-72.013 393.821,-62 382.059,-51.1404 366.728,-42.1637 353.413,-35.5713\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"354.69,-32.3041 344.153,-31.1996 351.702,-38.634 354.69,-32.3041\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"424.321\" y=\"-65.8\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M441.69,-98.1028C445.777,-91.5928 450.225,-84.0908 453.821,-77 457.791,-69.1689 461.597,-60.4456 464.893,-52.3336\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"468.223,-53.4297 468.639,-42.843 461.712,-50.86 468.223,-53.4297\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.321\" y=\"-65.8\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
"<path d=\"M450.401,-125.37C460.665,-126.528 469.821,-123.738 469.821,-117 469.821,-112.683 466.063,-109.987 460.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"460.493,-105.405 450.401,-108.63 460.302,-112.402 460.493,-105.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"485.821\" y=\"-113.3\">a &amp; b</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>5-&gt;0</title>\n",
"<path d=\"M212.569,-95.3163C209.347,-84.2043 203.876,-70.9826 194.821,-62 176.833,-44.1578 149.662,-34.2098 128.489,-28.8346\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"129.176,-25.401 118.644,-26.5487 127.593,-32.2197 129.176,-25.401\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"222.821\" y=\"-65.8\">!a &amp; c</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge12\"><title>5-&gt;2</title>\n",
"<path d=\"M237.087,-107.526C263.687,-96.5156 311.919,-76.937 353.821,-62 384.748,-50.9751 420.585,-39.6937 445.38,-32.1195\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"446.406,-35.4656 454.958,-29.2102 444.372,-28.7677 446.406,-35.4656\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"371.821\" y=\"-65.8\">a &amp; !c</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
"<path d=\"M237.401,-125.37C247.665,-126.528 256.821,-123.738 256.821,-117 256.821,-112.683 253.063,-109.987 247.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"247.493,-105.405 237.401,-108.63 247.302,-112.402 247.493,-105.405\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"272.321\" y=\"-113.3\">a &amp; c</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x7f798e982eb8>"
]
}
],
"prompt_number": 12
}
],
"metadata": {}
}
]
}
Reference in a new issue View git blame Copy permalink