1375 lines
No EOL
94 KiB
Text
1375 lines
No EOL
94 KiB
Text
{
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.5.1"
|
|
},
|
|
"name": ""
|
|
},
|
|
"nbformat": 3,
|
|
"nbformat_minor": 0,
|
|
"worksheets": [
|
|
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"This first chunk just makes sure the version of DiVinE installed accepts the `--LTSmin` option. If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"import sys\n",
|
|
"# Make sure we have divine and that it is patched to accept the --LTSmin option.\n",
|
|
"import shutil\n",
|
|
"if shutil.which(\"divine\") == None:\n",
|
|
" sys.exit(77)\n",
|
|
"import subprocess\n",
|
|
"out = subprocess.check_output(['divine', 'compile', '--help'], stderr=subprocess.STDOUT)\n",
|
|
"if b'LTSmin' not in out:\n",
|
|
" sys.exit(77)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 1
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The real test case starts here."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"import spot\n",
|
|
"import spot.ltsmin\n",
|
|
"# This is notebook also tests the limitation of the number of states in the GraphViz output\n",
|
|
"spot.setup(max_states=10)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 2
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The check of DiVinE and the setup of Spot can also be done with only:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": true,
|
|
"input": [
|
|
"import spot\n",
|
|
"import spot.ltsmin\n",
|
|
"%require divine\n",
|
|
"spot.setup(max_states=10)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 3
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Write an example DiVinE model. "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"!rm -f test1.dve"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 4
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"%%file test1.dve\n",
|
|
"int a = 0, b = 0;\n",
|
|
"\n",
|
|
"process P {\n",
|
|
" state x;\n",
|
|
" init x;\n",
|
|
"\n",
|
|
" trans\n",
|
|
" x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
|
|
" x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
|
|
"}\n",
|
|
"\n",
|
|
"process Q {\n",
|
|
" state wait, work;\n",
|
|
" init wait;\n",
|
|
" trans\n",
|
|
" wait -> work { guard b > 1; },\n",
|
|
" work -> wait { guard a > 1; };\n",
|
|
"}\n",
|
|
"\n",
|
|
"system async;"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"Writing test1.dve\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 5
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Compile the model using the `ltlmin` interface and load it. This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed.\n",
|
|
"\n",
|
|
"Printing an ltsmin model shows some information about the variables it contains and their types."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"m = spot.ltsmin.load('test1.dve')\n",
|
|
"m"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 6,
|
|
"text": [
|
|
"ltsmin model with the following variables:\n",
|
|
" a: int\n",
|
|
" b: int\n",
|
|
" P: ['x']\n",
|
|
" Q: ['wait', 'work']"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 6
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"You can also directly load the model into variable m1 by using %dve command"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": true,
|
|
"input": [
|
|
"%%dve m1\n",
|
|
"int a = 0, b = 0;\n",
|
|
"\n",
|
|
"process P {\n",
|
|
" state x;\n",
|
|
" init x;\n",
|
|
"\n",
|
|
" trans\n",
|
|
" x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
|
|
" x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
|
|
"}\n",
|
|
"\n",
|
|
"process Q {\n",
|
|
" state wait, work;\n",
|
|
" init wait;\n",
|
|
" trans\n",
|
|
" wait -> work { guard b > 1; },\n",
|
|
" work -> wait { guard a > 1; };\n",
|
|
"}\n",
|
|
"\n",
|
|
"system async;"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 7
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"m1"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 8,
|
|
"text": [
|
|
"ltsmin model with the following variables:\n",
|
|
" a: int\n",
|
|
" b: int\n",
|
|
" P: ['x']\n",
|
|
" Q: ['wait', 'work']"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 8
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"sorted(m.info().items())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 9,
|
|
"text": [
|
|
"[('state_size', 4),\n",
|
|
" ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
|
|
" ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 9
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"k = m.kripke([\"a<1\", \"b>2\"])\n",
|
|
"k"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 10,
|
|
"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=\"734pt\" height=\"222pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 222.26\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.661987 0.661987) rotate(0) translate(4 331.74)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-331.74 1104.78,-331.74 1104.78,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"147.309\" cy=\"-154.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"147.309\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"147.309\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.10532,-154.87C2.30847,-154.87 13.7102,-154.87 29.6433,-154.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"36.7326,-154.87 29.7326,-158.02 33.2326,-154.87 29.7326,-154.87 29.7326,-154.87 29.7326,-154.87 33.2326,-154.87 29.7326,-151.72 36.7326,-154.87 36.7326,-154.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"406.754\" cy=\"-190.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"406.754\" y=\"-194.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"406.754\" y=\"-179.67\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M243.441,-168.173C262.448,-170.831 282.507,-173.636 301.795,-176.333\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"308.862,-177.321 301.493,-179.471 305.396,-176.836 301.93,-176.352 301.93,-176.352 301.93,-176.352 305.396,-176.836 302.366,-173.232 308.862,-177.321 308.862,-177.321\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"406.754\" cy=\"-118.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"406.754\" y=\"-122.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"406.754\" y=\"-107.67\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M243.441,-141.567C263.044,-138.826 283.766,-135.928 303.606,-133.154\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"310.584,-132.178 304.088,-136.267 307.118,-132.663 303.651,-133.148 303.651,-133.148 303.651,-133.148 307.118,-132.663 303.215,-130.028 310.584,-132.178 310.584,-132.178\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-226.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-230.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-215.67\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M505.041,-204.326C524.202,-206.977 544.379,-209.767 563.759,-212.448\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"570.86,-213.43 563.494,-215.591 567.393,-212.951 563.926,-212.471 563.926,-212.471 563.926,-212.471 567.393,-212.951 564.357,-209.351 570.86,-213.43 570.86,-213.43\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\"><title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-154.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M505.041,-177.414C524.202,-174.764 544.379,-171.973 563.759,-169.292\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"570.86,-168.31 564.357,-172.389 567.393,-168.79 563.926,-169.269 563.926,-169.269 563.926,-169.269 567.393,-168.79 563.494,-166.149 570.86,-168.31 570.86,-168.31\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M503.193,-132.071C522.92,-134.799 543.794,-137.686 563.815,-140.456\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"570.858,-141.43 563.492,-143.591 567.391,-140.95 563.924,-140.471 563.924,-140.471 563.924,-140.471 567.391,-140.95 564.355,-137.35 570.858,-141.43 570.858,-141.43\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\"><title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"669.029\" cy=\"-82.8701\" rx=\"110.118\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"669.029\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M503.193,-105.669C523.527,-102.857 545.081,-99.8757 565.662,-97.0289\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"572.602,-96.0691 566.099,-100.149 569.135,-96.5487 565.668,-97.0283 565.668,-97.0283 565.668,-97.0283 569.135,-96.5487 565.236,-93.908 572.602,-96.0691 572.602,-96.0691\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\"><title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-282.87\" rx=\"110.118\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-286.67\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-271.67\" font-family=\"Lato\" font-size=\"14.00\">!"a<1" & !"b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\"><title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M753.258,-244.974C780.48,-250.896 810.816,-257.494 838.448,-263.505\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"845.411,-265.019 837.901,-266.61 841.991,-264.275 838.571,-263.532 838.571,-263.532 838.571,-263.532 841.991,-264.275 839.24,-260.454 845.411,-265.019 845.411,-265.019\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\"><title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-210.87\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-214.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\"><title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M778.836,-220.108C802.116,-218.661 826.286,-217.159 848.202,-215.797\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"855.234,-215.36 848.443,-218.938 851.741,-215.577 848.248,-215.794 848.248,-215.794 848.248,-215.794 851.741,-215.577 848.052,-212.65 855.234,-215.36 855.234,-215.36\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\"><title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M753.258,-172.974C786.856,-180.283 825.2,-188.623 857.346,-195.616\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"864.528,-197.178 857.019,-198.768 861.108,-196.434 857.688,-195.69 857.688,-195.69 857.688,-195.69 861.108,-196.434 858.358,-192.612 864.528,-197.178 864.528,-197.178\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\"><title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-138.87\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-142.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-127.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\"><title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M778.836,-148.108C802.116,-146.661 826.286,-145.159 848.202,-143.797\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"855.234,-143.36 848.443,-146.938 851.741,-143.577 848.248,-143.794 848.248,-143.794 848.248,-143.794 851.741,-143.577 848.052,-140.65 855.234,-143.36 855.234,-143.36\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\"><title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M751.84,-100.666C785.792,-108.051 824.788,-116.533 857.397,-123.627\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"864.255,-125.118 856.745,-126.708 860.835,-124.374 857.414,-123.63 857.414,-123.63 857.414,-123.63 860.835,-124.374 858.084,-120.552 864.255,-125.118 864.255,-125.118\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u5 -->\n",
|
|
"<g id=\"node11\" class=\"node\"><title>u5</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"941.474,-94.3701 915.474,-94.3701 915.474,-71.3701 941.474,-71.3701 941.474,-94.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->u5 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\"><title>5->u5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M779.582,-82.8701C828.369,-82.8701 880.914,-82.8701 908.333,-82.8701\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"915.376,-82.8701 908.376,-86.0202 911.876,-82.8701 908.376,-82.8702 908.376,-82.8702 908.376,-82.8702 911.876,-82.8701 908.376,-79.7202 915.376,-82.8701 915.376,-82.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node12\" class=\"node\"><title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"928.474\" cy=\"-26.8701\" rx=\"74.4932\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n",
|
|
"<text text-anchor=\"middle\" x=\"928.474\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\"><title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M751.84,-65.0744C785.792,-57.6891 824.788,-49.2066 857.397,-42.1134\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"864.255,-40.6217 858.084,-45.1877 860.835,-41.3657 857.414,-42.1097 857.414,-42.1097 857.414,-42.1097 860.835,-41.3657 856.745,-39.0316 864.255,-40.6217 864.255,-40.6217\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\"><title>6->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M898.965,-309.141C897.654,-319.298 907.49,-327.74 928.474,-327.74 944.213,-327.74 953.68,-322.991 956.877,-316.332\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"957.984,-309.141 960.032,-316.538 957.451,-312.6 956.919,-316.059 956.919,-316.059 956.919,-316.059 957.451,-312.6 953.806,-315.58 957.984,-309.141 957.984,-309.141\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u7 -->\n",
|
|
"<g id=\"node13\" class=\"node\"><title>u7</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-222.37 1074.78,-222.37 1074.78,-199.37 1100.78,-199.37 1100.78,-222.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1087.78\" y=\"-207.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->u7 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\"><title>7->u7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-210.87C1026.7,-210.87 1050.95,-210.87 1067.23,-210.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-210.87 1067.54,-214.02 1071.04,-210.87 1067.54,-210.87 1067.54,-210.87 1067.54,-210.87 1071.04,-210.87 1067.54,-207.72 1074.54,-210.87 1074.54,-210.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u8 -->\n",
|
|
"<g id=\"node14\" class=\"node\"><title>u8</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-150.37 1074.78,-150.37 1074.78,-127.37 1100.78,-127.37 1100.78,-150.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1087.78\" y=\"-135.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->u8 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\"><title>8->u8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-138.87C1026.7,-138.87 1050.95,-138.87 1067.23,-138.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-138.87 1067.54,-142.02 1071.04,-138.87 1067.54,-138.87 1067.54,-138.87 1067.54,-138.87 1071.04,-138.87 1067.54,-135.72 1074.54,-138.87 1074.54,-138.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u9 -->\n",
|
|
"<g id=\"node15\" class=\"node\"><title>u9</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1100.78,-38.3701 1074.78,-38.3701 1074.78,-15.3701 1100.78,-15.3701 1100.78,-38.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1087.78\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->u9 -->\n",
|
|
"<g id=\"edge18\" class=\"edge\"><title>9->u9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1003.06,-26.8701C1026.7,-26.8701 1050.95,-26.8701 1067.23,-26.8701\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1074.54,-26.8701 1067.54,-30.0202 1071.04,-26.8701 1067.54,-26.8702 1067.54,-26.8702 1067.54,-26.8702 1071.04,-26.8701 1067.54,-23.7202 1074.54,-26.8701 1074.54,-26.8701\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text": [
|
|
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x109e19ed0> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 10
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"k.show('.<15')"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 11,
|
|
"svg": [
|
|
"<svg height=\"204pt\" viewBox=\"0.00 0.00 734.00 203.83\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.535353 0.535353) rotate(0) translate(4 376.74)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-376.74 1367.06,-376.74 1367.06,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"147.309\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-187.67\">a=0, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-172.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M1.10532,-183.87C2.30847,-183.87 13.7102,-183.87 29.6433,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"36.7326,-183.87 29.7326,-187.02 33.2326,-183.87 29.7326,-183.87 29.7326,-183.87 29.7326,-183.87 33.2326,-183.87 29.7326,-180.72 36.7326,-183.87 36.7326,-183.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"406.754\" cy=\"-219.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-223.67\">a=1, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-208.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M243.441,-197.173C262.448,-199.831 282.507,-202.636 301.795,-205.333\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"308.862,-206.321 301.493,-208.471 305.396,-205.836 301.93,-205.352 301.93,-205.352 301.93,-205.352 305.396,-205.836 302.366,-202.232 308.862,-206.321 308.862,-206.321\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"406.754\" cy=\"-147.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-151.67\">a=0, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-136.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M243.441,-170.567C263.044,-167.826 283.766,-164.928 303.606,-162.154\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"310.584,-161.178 304.088,-165.267 307.118,-161.663 303.651,-162.148 303.651,-162.148 303.651,-162.148 307.118,-161.663 303.215,-159.028 310.584,-161.178 310.584,-161.178\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-259.67\">a=2, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-244.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->3</title>\n",
|
|
"<path d=\"M505.041,-233.326C524.202,-235.977 544.379,-238.767 563.759,-241.448\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.86,-242.43 563.494,-244.591 567.393,-241.951 563.926,-241.471 563.926,-241.471 563.926,-241.471 567.393,-241.951 564.357,-238.351 570.86,-242.43 570.86,-242.43\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-187.67\">a=1, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-172.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->4</title>\n",
|
|
"<path d=\"M505.041,-206.414C524.202,-203.764 544.379,-200.973 563.759,-198.292\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.86,-197.31 564.357,-201.389 567.393,-197.79 563.926,-198.269 563.926,-198.269 563.926,-198.269 567.393,-197.79 563.494,-195.149 570.86,-197.31 570.86,-197.31\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>2->4</title>\n",
|
|
"<path d=\"M503.193,-161.071C522.92,-163.799 543.794,-166.686 563.815,-169.456\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.858,-170.43 563.492,-172.591 567.391,-169.95 563.924,-169.471 563.924,-169.471 563.924,-169.471 567.391,-169.95 564.355,-166.35 570.858,-170.43 570.858,-170.43\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g class=\"node\" id=\"node7\"><title>5</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-115.67\">a=0, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-100.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>2->5</title>\n",
|
|
"<path d=\"M503.193,-134.669C523.527,-131.857 545.081,-128.876 565.662,-126.029\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"572.602,-125.069 566.099,-129.149 569.135,-125.549 565.668,-126.028 565.668,-126.028 565.668,-126.028 569.135,-125.549 565.236,-122.908 572.602,-125.069 572.602,-125.069\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g class=\"node\" id=\"node8\"><title>6</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-331.67\">a=3, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-316.67\">!"a<1" & !"b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>3->6</title>\n",
|
|
"<path d=\"M743.569,-276.214C776.83,-285.415 816.217,-296.31 850.223,-305.718\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"857.394,-307.701 849.808,-308.871 854.021,-306.768 850.648,-305.835 850.648,-305.835 850.648,-305.835 854.021,-306.768 851.487,-302.799 857.394,-307.701 857.394,-307.701\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g class=\"node\" id=\"node9\"><title>7</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-259.67\">a=2, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-244.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>3->7</title>\n",
|
|
"<path d=\"M782.297,-255.87C791.726,-255.87 801.282,-255.87 810.763,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"817.995,-255.87 810.995,-259.02 814.495,-255.87 810.995,-255.87 810.995,-255.87 810.995,-255.87 814.495,-255.87 810.995,-252.72 817.995,-255.87 817.995,-255.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>4->7</title>\n",
|
|
"<path d=\"M743.569,-204.214C776.69,-213.376 815.885,-224.218 849.793,-233.598\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"856.944,-235.577 849.357,-236.746 853.571,-234.644 850.197,-233.71 850.197,-233.71 850.197,-233.71 853.571,-234.644 851.037,-230.674 856.944,-235.577 856.944,-235.577\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g class=\"node\" id=\"node10\"><title>8</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-187.67\">a=1, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-172.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>4->8</title>\n",
|
|
"<path d=\"M782.297,-183.87C791.726,-183.87 801.282,-183.87 810.763,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"817.995,-183.87 810.995,-187.02 814.495,-183.87 810.995,-183.87 810.995,-183.87 810.995,-183.87 814.495,-183.87 810.995,-180.72 817.995,-183.87 817.995,-183.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>5->8</title>\n",
|
|
"<path d=\"M742.529,-131.926C775.95,-141.171 815.726,-152.175 850.047,-161.669\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"856.835,-163.547 849.249,-164.716 853.462,-162.614 850.089,-161.68 850.089,-161.68 850.089,-161.68 853.462,-162.614 850.929,-158.644 856.835,-163.547 856.835,-163.547\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g class=\"node\" id=\"node11\"><title>9</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-15.6701\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>5->9</title>\n",
|
|
"<path d=\"M735.707,-90.421C776.564,-77.078 828.761,-60.0315 868.808,-46.953\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"875.632,-44.7245 869.955,-49.892 872.305,-45.811 868.978,-46.8976 868.978,-46.8976 868.978,-46.8976 872.305,-45.811 868,-43.9033 875.632,-44.7245 875.632,-44.7245\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10 -->\n",
|
|
"<g class=\"node\" id=\"node12\"><title>10</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-115.67\">a=0, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-100.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->10 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>5->10</title>\n",
|
|
"<path d=\"M779.654,-111.87C790.929,-111.87 802.414,-111.87 813.761,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"820.804,-111.87 813.804,-115.02 817.304,-111.87 813.804,-111.87 813.804,-111.87 813.804,-111.87 817.304,-111.87 813.804,-108.72 820.804,-111.87 820.804,-111.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>6->6</title>\n",
|
|
"<path d=\"M883.684,-352.332C879.148,-363.275 895.021,-372.74 931.303,-372.74 959.081,-372.74 974.895,-367.192 978.747,-359.68\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"978.922,-352.332 981.905,-359.404 978.839,-355.831 978.756,-359.33 978.756,-359.33 978.756,-359.33 978.839,-355.831 975.607,-359.255 978.922,-352.332 978.922,-352.332\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11 -->\n",
|
|
"<g class=\"node\" id=\"node13\"><title>11</title>\n",
|
|
"<ellipse cx=\"1190.75\" cy=\"-327.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-331.67\">a=3, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-316.67\">!"a<1" & !"b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->11 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>7->11</title>\n",
|
|
"<path d=\"M1005.39,-276.31C1038.14,-285.47 1076.85,-296.294 1110.31,-305.654\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1117.37,-307.628 1109.78,-308.777 1114,-306.686 1110.63,-305.743 1110.63,-305.743 1110.63,-305.743 1114,-306.686 1111.48,-302.709 1117.37,-307.628 1117.37,-307.628\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12 -->\n",
|
|
"<g class=\"node\" id=\"node14\"><title>12</title>\n",
|
|
"<ellipse cx=\"1190.75\" cy=\"-255.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-259.67\">a=2, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-244.67\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->12 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>7->12</title>\n",
|
|
"<path d=\"M1044.47,-255.87C1066.29,-255.87 1088.75,-255.87 1109.3,-255.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1116.48,-255.87 1109.48,-259.02 1112.98,-255.87 1109.48,-255.87 1109.48,-255.87 1109.48,-255.87 1112.98,-255.87 1109.48,-252.72 1116.48,-255.87 1116.48,-255.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8->12 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>8->12</title>\n",
|
|
"<path d=\"M1005.39,-204.31C1042.88,-214.794 1088.16,-227.46 1124.47,-237.614\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1131.61,-239.609 1124.02,-240.758 1128.24,-238.667 1124.87,-237.724 1124.87,-237.724 1124.87,-237.724 1128.24,-238.667 1125.71,-234.69 1131.61,-239.609 1131.61,-239.609\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13 -->\n",
|
|
"<g class=\"node\" id=\"node15\"><title>13</title>\n",
|
|
"<ellipse cx=\"1190.75\" cy=\"-183.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-187.67\">a=1, b=3, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-172.67\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->13 -->\n",
|
|
"<g class=\"edge\" id=\"edge19\"><title>8->13</title>\n",
|
|
"<path d=\"M1044.47,-183.87C1066.29,-183.87 1088.75,-183.87 1109.3,-183.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1116.48,-183.87 1109.48,-187.02 1112.98,-183.87 1109.48,-183.87 1109.48,-183.87 1109.48,-183.87 1112.98,-183.87 1109.48,-180.72 1116.48,-183.87 1116.48,-183.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14 -->\n",
|
|
"<g class=\"node\" id=\"node16\"><title>14</title>\n",
|
|
"<ellipse cx=\"1190.75\" cy=\"-111.87\" fill=\"#ffffaa\" rx=\"74.4932\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-115.67\">a=1, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-100.67\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->14 -->\n",
|
|
"<g class=\"edge\" id=\"edge20\"><title>8->14</title>\n",
|
|
"<path d=\"M1005.39,-163.43C1042.88,-152.946 1088.16,-140.281 1124.47,-130.127\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1131.61,-128.131 1125.71,-133.05 1128.24,-129.073 1124.87,-130.016 1124.87,-130.016 1124.87,-130.016 1128.24,-129.073 1124.02,-126.982 1131.61,-128.131 1131.61,-128.131\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u9 -->\n",
|
|
"<g class=\"node\" id=\"node17\"><title>u9</title>\n",
|
|
"<polygon fill=\"#ffffaa\" points=\"1203.75,-26.3701 1177.75,-26.3701 1177.75,-3.37006 1203.75,-3.37006 1203.75,-26.3701\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-11.1701\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->u9 -->\n",
|
|
"<g class=\"edge\" id=\"edge21\"><title>9->u9</title>\n",
|
|
"<path d=\"M1005.04,-23.4795C1061.44,-20.8505 1135.65,-17.3916 1170.33,-15.7753\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1177.49,-15.4414 1170.65,-18.914 1173.99,-15.6044 1170.5,-15.7674 1170.5,-15.7674 1170.5,-15.7674 1173.99,-15.6044 1170.35,-12.6208 1177.49,-15.4414 1177.49,-15.4414\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10->14 -->\n",
|
|
"<g class=\"edge\" id=\"edge23\"><title>10->14</title>\n",
|
|
"<path d=\"M1041.86,-111.87C1064.48,-111.87 1087.91,-111.87 1109.27,-111.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1116.43,-111.87 1109.43,-115.02 1112.93,-111.87 1109.43,-111.87 1109.43,-111.87 1109.43,-111.87 1112.93,-111.87 1109.43,-108.72 1116.43,-111.87 1116.43,-111.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u10 -->\n",
|
|
"<g class=\"node\" id=\"node18\"><title>u10</title>\n",
|
|
"<polygon fill=\"#ffffaa\" points=\"1203.75,-67.3701 1177.75,-67.3701 1177.75,-44.3701 1203.75,-44.3701 1203.75,-67.3701\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1190.75\" y=\"-52.1701\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 10->u10 -->\n",
|
|
"<g class=\"edge\" id=\"edge22\"><title>10->u10</title>\n",
|
|
"<path d=\"M1008.23,-92.5305C1031.35,-86.8813 1056.88,-80.8833 1080.44,-75.8701 1111.84,-69.1887 1148.59,-62.744 1170.48,-59.0506\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1177.57,-57.863 1171.19,-62.1263 1174.12,-58.4413 1170.67,-59.0196 1170.67,-59.0196 1170.67,-59.0196 1174.12,-58.4413 1170.15,-55.9129 1177.57,-57.863 1177.57,-57.863\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11->11 -->\n",
|
|
"<g class=\"edge\" id=\"edge24\"><title>11->11</title>\n",
|
|
"<path d=\"M1161.24,-354.141C1159.93,-364.298 1169.76,-372.74 1190.75,-372.74 1206.49,-372.74 1215.95,-367.991 1219.15,-361.332\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1220.26,-354.141 1222.31,-361.538 1219.73,-357.6 1219.19,-361.059 1219.19,-361.059 1219.19,-361.059 1219.73,-357.6 1216.08,-360.58 1220.26,-354.141 1220.26,-354.141\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u12 -->\n",
|
|
"<g class=\"node\" id=\"node19\"><title>u12</title>\n",
|
|
"<polygon fill=\"#ffffaa\" points=\"1363.06,-267.37 1337.06,-267.37 1337.06,-244.37 1363.06,-244.37 1363.06,-267.37\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-252.17\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12->u12 -->\n",
|
|
"<g class=\"edge\" id=\"edge25\"><title>12->u12</title>\n",
|
|
"<path d=\"M1265.34,-255.87C1288.98,-255.87 1313.23,-255.87 1329.5,-255.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1336.82,-255.87 1329.82,-259.02 1333.32,-255.87 1329.82,-255.87 1329.82,-255.87 1329.82,-255.87 1333.32,-255.87 1329.82,-252.72 1336.82,-255.87 1336.82,-255.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u13 -->\n",
|
|
"<g class=\"node\" id=\"node20\"><title>u13</title>\n",
|
|
"<polygon fill=\"#ffffaa\" points=\"1363.06,-195.37 1337.06,-195.37 1337.06,-172.37 1363.06,-172.37 1363.06,-195.37\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-180.17\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 13->u13 -->\n",
|
|
"<g class=\"edge\" id=\"edge26\"><title>13->u13</title>\n",
|
|
"<path d=\"M1265.34,-183.87C1288.98,-183.87 1313.23,-183.87 1329.5,-183.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1336.82,-183.87 1329.82,-187.02 1333.32,-183.87 1329.82,-183.87 1329.82,-183.87 1329.82,-183.87 1333.32,-183.87 1329.82,-180.72 1336.82,-183.87 1336.82,-183.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u14 -->\n",
|
|
"<g class=\"node\" id=\"node21\"><title>u14</title>\n",
|
|
"<polygon fill=\"#ffffaa\" points=\"1363.06,-123.37 1337.06,-123.37 1337.06,-100.37 1363.06,-100.37 1363.06,-123.37\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1350.06\" y=\"-108.17\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 14->u14 -->\n",
|
|
"<g class=\"edge\" id=\"edge27\"><title>14->u14</title>\n",
|
|
"<path d=\"M1265.34,-111.87C1288.98,-111.87 1313.23,-111.87 1329.5,-111.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1336.82,-111.87 1329.82,-115.02 1333.32,-111.87 1329.82,-111.87 1329.82,-111.87 1329.82,-111.87 1333.32,-111.87 1329.82,-108.72 1336.82,-111.87 1336.82,-111.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>"
|
|
],
|
|
"text": [
|
|
"<IPython.core.display.SVG object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 11
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"k.show('.<0') # unlimited output"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 12,
|
|
"svg": [
|
|
"<svg height=\"154pt\" viewBox=\"0.00 0.00 734.00 153.94\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.399073 0.399073) rotate(0) translate(4 381.74)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-381.74 1835.26,-381.74 1835.26,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"147.309\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-192.67\">a=0, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"147.309\" y=\"-177.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M1.10532,-188.87C2.30847,-188.87 13.7102,-188.87 29.6433,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"36.7326,-188.87 29.7326,-192.02 33.2326,-188.87 29.7326,-188.87 29.7326,-188.87 29.7326,-188.87 33.2326,-188.87 29.7326,-185.72 36.7326,-188.87 36.7326,-188.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"406.754\" cy=\"-224.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-228.67\">a=1, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-213.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M243.441,-202.173C262.448,-204.831 282.507,-207.636 301.795,-210.333\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"308.862,-211.321 301.493,-213.471 305.396,-210.836 301.93,-210.352 301.93,-210.352 301.93,-210.352 305.396,-210.836 302.366,-207.232 308.862,-211.321 308.862,-211.321\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"406.754\" cy=\"-152.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-156.67\">a=0, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"406.754\" y=\"-141.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M243.441,-175.567C263.044,-172.826 283.766,-169.928 303.606,-167.154\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"310.584,-166.178 304.088,-170.267 307.118,-166.663 303.651,-167.148 303.651,-167.148 303.651,-167.148 307.118,-166.663 303.215,-164.028 310.584,-166.178 310.584,-166.178\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-264.67\">a=2, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-249.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->3</title>\n",
|
|
"<path d=\"M505.041,-238.326C524.202,-240.977 544.379,-243.767 563.759,-246.448\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.86,-247.43 563.494,-249.591 567.393,-246.951 563.926,-246.471 563.926,-246.471 563.926,-246.471 567.393,-246.951 564.357,-243.351 570.86,-247.43 570.86,-247.43\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-192.67\">a=1, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-177.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->4</title>\n",
|
|
"<path d=\"M505.041,-211.414C524.202,-208.764 544.379,-205.973 563.759,-203.292\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.86,-202.31 564.357,-206.389 567.393,-202.79 563.926,-203.269 563.926,-203.269 563.926,-203.269 567.393,-202.79 563.494,-200.149 570.86,-202.31 570.86,-202.31\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>2->4</title>\n",
|
|
"<path d=\"M503.193,-166.071C522.92,-168.799 543.794,-171.686 563.815,-174.456\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"570.858,-175.43 563.492,-177.591 567.391,-174.95 563.924,-174.471 563.924,-174.471 563.924,-174.471 567.391,-174.95 564.355,-171.35 570.858,-175.43 570.858,-175.43\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g class=\"node\" id=\"node7\"><title>5</title>\n",
|
|
"<ellipse cx=\"669.029\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-120.67\">a=0, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"669.029\" y=\"-105.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>2->5</title>\n",
|
|
"<path d=\"M503.193,-139.669C523.527,-136.857 545.081,-133.876 565.662,-131.029\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"572.602,-130.069 566.099,-134.149 569.135,-130.549 565.668,-131.028 565.668,-131.028 565.668,-131.028 569.135,-130.549 565.236,-127.908 572.602,-130.069 572.602,-130.069\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g class=\"node\" id=\"node8\"><title>6</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-336.67\">a=3, b=0, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-321.67\">!"a<1" & !"b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>3->6</title>\n",
|
|
"<path d=\"M743.569,-281.214C776.83,-290.415 816.217,-301.31 850.223,-310.718\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"857.394,-312.701 849.808,-313.871 854.021,-311.768 850.648,-310.835 850.648,-310.835 850.648,-310.835 854.021,-311.768 851.487,-307.799 857.394,-312.701 857.394,-312.701\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g class=\"node\" id=\"node9\"><title>7</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-264.67\">a=2, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-249.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>3->7</title>\n",
|
|
"<path d=\"M782.297,-260.87C791.726,-260.87 801.282,-260.87 810.763,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"817.995,-260.87 810.995,-264.02 814.495,-260.87 810.995,-260.87 810.995,-260.87 810.995,-260.87 814.495,-260.87 810.995,-257.72 817.995,-260.87 817.995,-260.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>4->7</title>\n",
|
|
"<path d=\"M743.569,-209.214C776.69,-218.376 815.885,-229.218 849.793,-238.598\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"856.944,-240.577 849.357,-241.746 853.571,-239.644 850.197,-238.71 850.197,-238.71 850.197,-238.71 853.571,-239.644 851.037,-235.674 856.944,-240.577 856.944,-240.577\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g class=\"node\" id=\"node10\"><title>8</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-192.67\">a=1, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-177.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>4->8</title>\n",
|
|
"<path d=\"M782.297,-188.87C791.726,-188.87 801.282,-188.87 810.763,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"817.995,-188.87 810.995,-192.02 814.495,-188.87 810.995,-188.87 810.995,-188.87 810.995,-188.87 814.495,-188.87 810.995,-185.72 817.995,-188.87 817.995,-188.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>5->8</title>\n",
|
|
"<path d=\"M742.529,-136.926C775.95,-146.171 815.726,-157.175 850.047,-166.669\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"856.835,-168.547 849.249,-169.716 853.462,-167.614 850.089,-166.68 850.089,-166.68 850.089,-166.68 853.462,-167.614 850.929,-163.644 856.835,-168.547 856.835,-168.547\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g class=\"node\" id=\"node11\"><title>9</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-35.8701\" fill=\"#ffffaa\" rx=\"108.375\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-39.6701\">a=0, b=3, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-24.6701\">"a<1" & "b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>5->9</title>\n",
|
|
"<path d=\"M737.733,-95.7997C774.033,-84.5029 818.826,-70.5628 856.074,-58.9709\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"862.937,-56.8349 857.189,-61.9228 859.595,-57.875 856.253,-58.915 856.253,-58.915 856.253,-58.915 859.595,-57.875 855.317,-55.9073 862.937,-56.8349 862.937,-56.8349\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10 -->\n",
|
|
"<g class=\"node\" id=\"node12\"><title>10</title>\n",
|
|
"<ellipse cx=\"931.303\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-120.67\">a=0, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"931.303\" y=\"-105.67\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->10 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>5->10</title>\n",
|
|
"<path d=\"M779.654,-116.87C790.929,-116.87 802.414,-116.87 813.761,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"820.804,-116.87 813.804,-120.02 817.304,-116.87 813.804,-116.87 813.804,-116.87 813.804,-116.87 817.304,-116.87 813.804,-113.72 820.804,-116.87 820.804,-116.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>6->6</title>\n",
|
|
"<path d=\"M882.945,-357.332C878.34,-368.275 894.459,-377.74 931.303,-377.74 959.511,-377.74 975.571,-372.192 979.483,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"979.66,-357.332 982.641,-364.406 979.576,-360.831 979.491,-364.33 979.491,-364.33 979.491,-364.33 979.576,-360.831 976.342,-364.254 979.66,-357.332 979.66,-357.332\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11 -->\n",
|
|
"<g class=\"node\" id=\"node13\"><title>11</title>\n",
|
|
"<ellipse cx=\"1193.58\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-336.67\">a=3, b=1, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-321.67\">!"a<1" & !"b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->11 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>7->11</title>\n",
|
|
"<path d=\"M1005.84,-281.214C1039.1,-290.415 1078.49,-301.31 1112.5,-310.718\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1119.67,-312.701 1112.08,-313.871 1116.3,-311.768 1112.92,-310.835 1112.92,-310.835 1112.92,-310.835 1116.3,-311.768 1113.76,-307.799 1119.67,-312.701 1119.67,-312.701\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12 -->\n",
|
|
"<g class=\"node\" id=\"node14\"><title>12</title>\n",
|
|
"<ellipse cx=\"1193.58\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-264.67\">a=2, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-249.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->12 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>7->12</title>\n",
|
|
"<path d=\"M1044.57,-260.87C1054,-260.87 1063.56,-260.87 1073.04,-260.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1080.27,-260.87 1073.27,-264.02 1076.77,-260.87 1073.27,-260.87 1073.27,-260.87 1073.27,-260.87 1076.77,-260.87 1073.27,-257.72 1080.27,-260.87 1080.27,-260.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8->12 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>8->12</title>\n",
|
|
"<path d=\"M1005.84,-209.214C1038.96,-218.376 1078.16,-229.218 1112.07,-238.598\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1119.22,-240.577 1111.63,-241.746 1115.84,-239.644 1112.47,-238.71 1112.47,-238.71 1112.47,-238.71 1115.84,-239.644 1113.31,-235.674 1119.22,-240.577 1119.22,-240.577\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13 -->\n",
|
|
"<g class=\"node\" id=\"node15\"><title>13</title>\n",
|
|
"<ellipse cx=\"1193.58\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-192.67\">a=1, b=3, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-177.67\">!"a<1" & "b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->13 -->\n",
|
|
"<g class=\"edge\" id=\"edge19\"><title>8->13</title>\n",
|
|
"<path d=\"M1044.57,-188.87C1054.97,-188.87 1065.52,-188.87 1075.95,-188.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1083.15,-188.87 1076.15,-192.02 1079.65,-188.87 1076.15,-188.87 1076.15,-188.87 1076.15,-188.87 1079.65,-188.87 1076.15,-185.72 1083.15,-188.87 1083.15,-188.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14 -->\n",
|
|
"<g class=\"node\" id=\"node16\"><title>14</title>\n",
|
|
"<ellipse cx=\"1193.58\" cy=\"-116.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-120.67\">a=1, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-105.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->14 -->\n",
|
|
"<g class=\"edge\" id=\"edge20\"><title>8->14</title>\n",
|
|
"<path d=\"M1005.84,-168.526C1038.96,-159.364 1078.16,-148.522 1112.07,-139.142\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1119.22,-137.163 1113.31,-142.066 1115.84,-138.097 1112.47,-139.03 1112.47,-139.03 1112.47,-139.03 1115.84,-138.097 1111.63,-135.994 1119.22,-137.163 1119.22,-137.163\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 15 -->\n",
|
|
"<g class=\"node\" id=\"node17\"><title>15</title>\n",
|
|
"<ellipse cx=\"1193.58\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"105.218\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-30.6701\">a=0, b=3, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1193.58\" y=\"-15.6701\">"a<1" & "b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->15 -->\n",
|
|
"<g class=\"edge\" id=\"edge21\"><title>9->15</title>\n",
|
|
"<path d=\"M1038.54,-32.1964C1052.8,-31.7035 1067.45,-31.197 1081.78,-30.7014\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1088.78,-30.4592 1081.9,-33.8493 1085.28,-30.5802 1081.79,-30.7012 1081.79,-30.7012 1081.79,-30.7012 1085.28,-30.5802 1081.68,-27.5531 1088.78,-30.4592 1088.78,-30.4592\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10->14 -->\n",
|
|
"<g class=\"edge\" id=\"edge22\"><title>10->14</title>\n",
|
|
"<path d=\"M1041.93,-116.87C1052.2,-116.87 1062.65,-116.87 1073,-116.87\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1080.16,-116.87 1073.16,-120.02 1076.66,-116.87 1073.16,-116.87 1073.16,-116.87 1073.16,-116.87 1076.66,-116.87 1073.16,-113.72 1080.16,-116.87 1080.16,-116.87\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10->15 -->\n",
|
|
"<g class=\"edge\" id=\"edge23\"><title>10->15</title>\n",
|
|
"<path d=\"M995.64,-94.9687C1034.33,-81.59 1083.83,-64.4742 1123.52,-50.7489\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1130.31,-48.4023 1124.72,-53.667 1127,-49.5461 1123.69,-50.69 1123.69,-50.69 1123.69,-50.69 1127,-49.5461 1122.66,-47.7129 1130.31,-48.4023 1130.31,-48.4023\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11->11 -->\n",
|
|
"<g class=\"edge\" id=\"edge24\"><title>11->11</title>\n",
|
|
"<path d=\"M1145.22,-357.332C1140.61,-368.275 1156.73,-377.74 1193.58,-377.74 1221.79,-377.74 1237.85,-372.192 1241.76,-364.68\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1241.93,-357.332 1244.91,-364.406 1241.85,-360.831 1241.77,-364.33 1241.77,-364.33 1241.77,-364.33 1241.85,-360.831 1238.62,-364.254 1241.93,-357.332 1241.93,-357.332\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 16 -->\n",
|
|
"<g class=\"node\" id=\"node18\"><title>16</title>\n",
|
|
"<ellipse cx=\"1455.85\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-336.67\">a=3, b=2, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-321.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12->16 -->\n",
|
|
"<g class=\"edge\" id=\"edge25\"><title>12->16</title>\n",
|
|
"<path d=\"M1268.12,-281.214C1301.24,-290.376 1340.43,-301.218 1374.34,-310.598\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1381.49,-312.577 1373.91,-313.746 1378.12,-311.644 1374.75,-310.71 1374.75,-310.71 1374.75,-310.71 1378.12,-311.644 1375.59,-307.674 1381.49,-312.577 1381.49,-312.577\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 17 -->\n",
|
|
"<g class=\"node\" id=\"node19\"><title>17</title>\n",
|
|
"<ellipse cx=\"1455.85\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-192.67\">a=2, b=3, Q=0</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-177.67\">!"a<1" & "b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12->17 -->\n",
|
|
"<g class=\"edge\" id=\"edge26\"><title>12->17</title>\n",
|
|
"<path d=\"M1268.12,-240.526C1301.38,-231.325 1340.77,-220.43 1374.77,-211.023\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1381.94,-209.039 1376.04,-213.941 1378.57,-209.972 1375.2,-210.905 1375.2,-210.905 1375.2,-210.905 1378.57,-209.972 1374.36,-207.869 1381.94,-209.039 1381.94,-209.039\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 18 -->\n",
|
|
"<g class=\"node\" id=\"node20\"><title>18</title>\n",
|
|
"<ellipse cx=\"1455.85\" cy=\"-260.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-264.67\">a=2, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-249.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12->18 -->\n",
|
|
"<g class=\"edge\" id=\"edge27\"><title>12->18</title>\n",
|
|
"<path d=\"M1303.45,-254.201C1315.1,-254.112 1326.98,-254.096 1338.72,-254.155\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1346,-254.201 1338.98,-257.307 1342.5,-254.179 1339,-254.157 1339,-254.157 1339,-254.157 1342.5,-254.179 1339.02,-251.007 1346,-254.201 1346,-254.201\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 19 -->\n",
|
|
"<g class=\"node\" id=\"node21\"><title>19</title>\n",
|
|
"<ellipse cx=\"1455.85\" cy=\"-98.8701\" fill=\"#ffffaa\" rx=\"108.375\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-102.67\">a=1, b=3, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1455.85\" y=\"-87.6701\">!"a<1" & "b>2" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 13->19 -->\n",
|
|
"<g class=\"edge\" id=\"edge28\"><title>13->19</title>\n",
|
|
"<path d=\"M1262.02,-167.688C1276.78,-162.92 1292.3,-157.808 1306.71,-152.87 1333.58,-143.666 1362.99,-133.055 1388.48,-123.688\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1395.21,-121.209 1389.73,-126.584 1391.93,-122.418 1388.65,-123.628 1388.65,-123.628 1388.65,-123.628 1391.93,-122.418 1387.56,-120.671 1395.21,-121.209 1395.21,-121.209\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14->18 -->\n",
|
|
"<g class=\"edge\" id=\"edge29\"><title>14->18</title>\n",
|
|
"<path d=\"M1277.62,-135.06C1288.13,-139.712 1298.18,-145.549 1306.71,-152.87 1333.87,-176.161 1315.56,-201.579 1342.71,-224.87 1349.52,-230.704 1357.28,-235.595 1365.47,-239.696\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1371.81,-242.681 1364.13,-242.549 1368.64,-241.19 1365.47,-239.699 1365.47,-239.699 1365.47,-239.699 1368.64,-241.19 1366.81,-236.849 1371.81,-242.681 1371.81,-242.681\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14->19 -->\n",
|
|
"<g class=\"edge\" id=\"edge30\"><title>14->19</title>\n",
|
|
"<path d=\"M1302.32,-109.419C1316.13,-108.463 1330.3,-107.484 1344.16,-106.525\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1351.37,-106.026 1344.61,-109.652 1347.88,-106.268 1344.39,-106.509 1344.39,-106.509 1344.39,-106.509 1347.88,-106.268 1344.17,-103.367 1351.37,-106.026 1351.37,-106.026\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 15->15 -->\n",
|
|
"<g class=\"edge\" id=\"edge31\"><title>15->15</title>\n",
|
|
"<path d=\"M1145.42,-50.8749C1140.17,-62.0106 1156.22,-71.7401 1193.58,-71.7401 1222.76,-71.7401 1238.94,-65.8017 1242.12,-57.8937\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1241.73,-50.8749 1245.26,-57.6898 1241.92,-54.3695 1242.12,-57.8641 1242.12,-57.8641 1242.12,-57.8641 1241.92,-54.3695 1238.97,-58.0385 1241.73,-50.8749 1241.73,-50.8749\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 20 -->\n",
|
|
"<g class=\"node\" id=\"node22\"><title>20</title>\n",
|
|
"<ellipse cx=\"1718.13\" cy=\"-332.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-336.67\">a=3, b=2, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-321.67\">!"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 16->20 -->\n",
|
|
"<g class=\"edge\" id=\"edge32\"><title>16->20</title>\n",
|
|
"<path d=\"M1565.72,-326.201C1577.37,-326.112 1589.26,-326.096 1600.99,-326.155\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1608.27,-326.201 1601.25,-329.307 1604.77,-326.179 1601.27,-326.157 1601.27,-326.157 1601.27,-326.157 1604.77,-326.179 1601.29,-323.007 1608.27,-326.201 1608.27,-326.201\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 21 -->\n",
|
|
"<g class=\"node\" id=\"node23\"><title>21</title>\n",
|
|
"<ellipse cx=\"1718.13\" cy=\"-188.87\" fill=\"#ffffaa\" rx=\"110.118\" ry=\"26.7407\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-192.67\">a=2, b=3, Q=1</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1718.13\" y=\"-177.67\">!"a<1" & "b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 17->21 -->\n",
|
|
"<g class=\"edge\" id=\"edge33\"><title>17->21</title>\n",
|
|
"<path d=\"M1563.09,-182.222C1576.62,-182.105 1590.5,-182.089 1604.13,-182.172\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1611.23,-182.225 1604.2,-185.323 1607.73,-182.199 1604.23,-182.173 1604.23,-182.173 1604.23,-182.173 1607.73,-182.199 1604.25,-179.023 1611.23,-182.225 1611.23,-182.225\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 18->12 -->\n",
|
|
"<g class=\"edge\" id=\"edge36\"><title>18->12</title>\n",
|
|
"<path d=\"M1346,-267.539C1334.35,-267.628 1322.46,-267.644 1310.73,-267.585\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1303.45,-267.539 1310.47,-264.434 1306.95,-267.561 1310.45,-267.584 1310.45,-267.584 1310.45,-267.584 1306.95,-267.561 1310.43,-270.734 1303.45,-267.539 1303.45,-267.539\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 18->20 -->\n",
|
|
"<g class=\"edge\" id=\"edge34\"><title>18->20</title>\n",
|
|
"<path d=\"M1530.39,-281.214C1563.51,-290.376 1602.71,-301.218 1636.62,-310.598\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1643.77,-312.577 1636.18,-313.746 1640.39,-311.644 1637.02,-310.71 1637.02,-310.71 1637.02,-310.71 1640.39,-311.644 1637.86,-307.674 1643.77,-312.577 1643.77,-312.577\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 18->21 -->\n",
|
|
"<g class=\"edge\" id=\"edge35\"><title>18->21</title>\n",
|
|
"<path d=\"M1530.39,-240.526C1563.65,-231.325 1603.04,-220.43 1637.05,-211.023\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1644.22,-209.039 1638.31,-213.941 1640.84,-209.972 1637.47,-210.905 1637.47,-210.905 1637.47,-210.905 1640.84,-209.972 1636.63,-207.869 1644.22,-209.039 1644.22,-209.039\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 19->19 -->\n",
|
|
"<g class=\"edge\" id=\"edge37\"><title>19->19</title>\n",
|
|
"<path d=\"M1407.49,-123.332C1402.89,-134.275 1419.01,-143.74 1455.85,-143.74 1484.06,-143.74 1500.12,-138.192 1504.03,-130.68\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1504.21,-123.332 1507.19,-130.406 1504.12,-126.831 1504.04,-130.33 1504.04,-130.33 1504.04,-130.33 1504.12,-126.831 1500.89,-130.254 1504.21,-123.332 1504.21,-123.332\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 20->16 -->\n",
|
|
"<g class=\"edge\" id=\"edge38\"><title>20->16</title>\n",
|
|
"<path d=\"M1608.27,-339.539C1596.62,-339.628 1584.74,-339.644 1573,-339.585\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1565.72,-339.539 1572.74,-336.434 1569.22,-339.561 1572.72,-339.584 1572.72,-339.584 1572.72,-339.584 1569.22,-339.561 1572.7,-342.734 1565.72,-339.539 1565.72,-339.539\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 21->17 -->\n",
|
|
"<g class=\"edge\" id=\"edge39\"><title>21->17</title>\n",
|
|
"<path d=\"M1611.23,-195.515C1597.71,-195.633 1583.82,-195.652 1570.19,-195.57\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"1563.09,-195.518 1570.11,-192.419 1566.59,-195.544 1570.09,-195.569 1570.09,-195.569 1570.09,-195.569 1566.59,-195.544 1570.07,-198.719 1563.09,-195.518 1563.09,-195.518\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>"
|
|
],
|
|
"text": [
|
|
"<IPython.core.display.SVG object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 12
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a = spot.translate('\"a<1\" U \"b>2\"'); a"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 13,
|
|
"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=\"85pt\"\n",
|
|
" viewBox=\"0.00 0.00 197.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 193,-81 193,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"11.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2"</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<ellipse fill=\"none\" stroke=\"black\" cx=\"167\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"167\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>1->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M74.0312,-22C91.0958,-22 117.659,-22 137.859,-22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"144.984,-22 137.984,-25.1501 141.484,-22 137.984,-22.0001 137.984,-22.0001 137.984,-22.0001 141.484,-22 137.984,-18.8501 144.984,-22 144.984,-22\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">"b>2"</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M156.933,-41.7575C155.223,-52.3499 158.578,-62 167,-62 173.448,-62 176.926,-56.3433 177.435,-48.9379\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"177.067,-41.7575 180.571,-48.5871 177.246,-45.2529 177.425,-48.7483 177.425,-48.7483 177.425,-48.7483 177.246,-45.2529 174.279,-48.9095 177.067,-41.7575 177.067,-41.7575\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"167\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text": [
|
|
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x109eaaab0> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 13
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"spot.otf_product(k, a)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 14,
|
|
"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=\"734pt\" height=\"107pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 106.67\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.467836 0.467836) rotate(0) translate(4 224)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-224 1564.93,-224 1564.93,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"119.893\" cy=\"-179\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"119.893\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.08545,-179C2.21412,-179 14.4049,-179 30.5502,-179\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"37.691,-179 30.6911,-182.15 34.191,-179 30.691,-179 30.691,-179 30.691,-179 34.191,-179 30.691,-175.85 37.691,-179 37.691,-179\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"459.678\" cy=\"-202\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"459.678\" y=\"-198.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M198.388,-184.277C250.861,-187.85 320.179,-192.57 374.087,-196.24\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"381.252,-196.728 374.054,-199.395 377.76,-196.49 374.268,-196.252 374.268,-196.252 374.268,-196.252 377.76,-196.49 374.482,-193.11 381.252,-196.728 381.252,-196.728\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"219.785\" y=\"-198.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"459.678\" cy=\"-148\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"459.678\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M189.462,-169.485C199.619,-168.222 209.967,-167.014 219.785,-166 270.641,-160.746 327.738,-156.387 373.357,-153.275\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"380.577,-152.787 373.806,-156.402 377.085,-153.023 373.593,-153.26 373.593,-153.26 373.593,-153.26 377.085,-153.023 373.381,-150.117 380.577,-152.787 380.577,-152.787\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"219.785\" y=\"-169.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"799.464\" cy=\"-171\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"799.464\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>2->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M538.173,-153.277C590.647,-156.85 659.965,-161.57 713.873,-165.24\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"721.038,-165.728 713.84,-168.395 717.546,-165.49 714.054,-165.252 714.054,-165.252 714.054,-165.252 717.546,-165.49 714.268,-162.11 721.038,-165.728 721.038,-165.728\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"559.571\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\"><title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"799.464\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"799.464\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M529.248,-138.485C539.404,-137.222 549.753,-136.014 559.571,-135 610.427,-129.746 667.524,-125.387 713.143,-122.275\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"720.363,-121.787 713.592,-125.402 716.871,-122.023 713.379,-122.26 713.379,-122.26 713.379,-122.26 716.871,-122.023 713.166,-119.117 720.363,-121.787 720.363,-121.787\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"559.571\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\"><title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-171\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1139.25\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->5 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>4->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M860.791,-129.032C873.509,-131.444 886.859,-133.885 899.356,-136 953.606,-145.181 1015.03,-154.149 1062.01,-160.708\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1069.13,-161.699 1061.76,-163.853 1065.66,-161.216 1062.19,-160.734 1062.19,-160.734 1062.19,-160.734 1065.66,-161.216 1062.63,-157.614 1069.13,-161.699 1069.13,-161.699\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"899.356\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\"><title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1139.25\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->6 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>4->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M881.372,-117C932.168,-117 997.697,-117 1049.86,-117\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1057.12,-117 1050.12,-120.15 1053.62,-117 1050.12,-117 1050.12,-117 1050.12,-117 1053.62,-117 1050.12,-113.85 1057.12,-117 1057.12,-117\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"899.356\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\"><title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1139.25\" cy=\"-63\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1139.25\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\"><title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M860.791,-104.968C873.509,-102.556 886.859,-100.115 899.356,-98 953.606,-88.8191 1015.03,-79.8515 1062.01,-73.292\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1069.13,-72.3012 1062.63,-76.3864 1065.66,-72.7838 1062.19,-73.2664 1062.19,-73.2664 1062.19,-73.2664 1065.66,-72.7838 1061.76,-70.1465 1069.13,-72.3012 1069.13,-72.3012\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"899.356\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\"><title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1479.03\" cy=\"-117\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1479.03\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1 * 0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->8 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\"><title>6->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1221.16,-117C1271.95,-117 1337.48,-117 1389.64,-117\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1396.91,-117 1389.91,-120.15 1393.41,-117 1389.91,-117 1389.91,-117 1389.91,-117 1393.41,-117 1389.91,-113.85 1396.91,-117 1396.91,-117\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1240.64\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- u7 -->\n",
|
|
"<g id=\"node11\" class=\"node\"><title>u7</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1492.03,-77.5 1466.03,-77.5 1466.03,-54.5 1492.03,-54.5 1492.03,-77.5\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1479.03\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->u7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\"><title>7->u7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1221.16,-63.7186C1299.76,-64.4166 1413.63,-65.428 1458.66,-65.8279\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1465.76,-65.891 1458.74,-68.9786 1462.26,-65.8599 1458.76,-65.8288 1458.76,-65.8288 1458.76,-65.8288 1462.26,-65.8599 1458.79,-62.6789 1465.76,-65.891 1465.76,-65.891\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node12\" class=\"node\"><title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1479.03\" cy=\"-18\" rx=\"81.7856\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1479.03\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1 * 1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->9 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\"><title>7->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1201.34,-51.2154C1213.82,-48.995 1226.88,-46.8062 1239.14,-45 1291.38,-37.303 1350.33,-30.6198 1396.6,-25.828\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1403.62,-25.1051 1396.98,-28.9554 1400.14,-25.4636 1396.65,-25.822 1396.65,-25.822 1396.65,-25.822 1400.14,-25.4636 1396.33,-22.6885 1403.62,-25.1051 1403.62,-25.1051\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1239.14\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & !"b>2" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\"><title>8->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1449.26,-134.037C1443.19,-143.858 1453.11,-153 1479.03,-153 1498.48,-153 1508.92,-147.858 1510.36,-141.143\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1508.8,-134.037 1513.38,-140.201 1509.55,-137.456 1510.3,-140.875 1510.3,-140.875 1510.3,-140.875 1509.55,-137.456 1507.23,-141.549 1508.8,-134.037 1508.8,-134.037\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1412.53\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">"a<1" & "b>2" & dead</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1471.03\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text": [
|
|
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x109e19e70> >"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 14
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"!rm -f test1.dve"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 15
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Note that using %%dve does not require any deletion."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": true,
|
|
"input": [],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": null
|
|
}
|
|
],
|
|
"metadata": {}
|
|
}
|
|
]
|
|
} |