71fef458e1
This is to workaround differences in minidom's pretty-printing that occurred between Python 3.7 and 3.8. * python/spot/jupyter.py (SVG): New class. * python/spot/__init__.py: Use it. * tests/python/_altscc.ipynb, tests/python/alternation.ipynb, tests/python/automata.ipynb, tests/python/formulas.ipynb, tests/python/gen.ipynb, tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb, tests/python/product.ipynb, tests/python/randaut.ipynb, tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb, tests/python/word.ipynb: Adjust.
1378 lines
82 KiB
Text
1378 lines
82 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"import spot\n",
|
|
"import spot.ltsmin\n",
|
|
"# The following line causes the notebook to exit with 77 if spins is not \n",
|
|
"# installed, therefore skipping this test in the test suite.\n",
|
|
"spot.ltsmin.require('spins')\n",
|
|
"spot.setup()"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"There are two ways to load a Promela model: from a file or from a cell. \n",
|
|
"\n",
|
|
"Loading from a cell\n",
|
|
"-------------------\n",
|
|
"\n",
|
|
"Using the `%%pml` magic will save the model in a temporary file, call `spins` to compile it, load the resulting shared library, and store the result into an object whose name is passed as an argument to `%%pml`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stderr",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n",
|
|
"(C) University of Twente, Formal Methods and Tools group\n",
|
|
"\n",
|
|
"Parsing tmpb2gyak36.pml...\n",
|
|
"Parsing tmpb2gyak36.pml done (0.0 sec)\n",
|
|
"\n",
|
|
"Optimizing graphs...\n",
|
|
" StateMerging changed 0 states/transitions.\n",
|
|
" RemoveUselessActions changed 2 states/transitions.\n",
|
|
" RemoveUselessGotos changed 2 states/transitions.\n",
|
|
" RenumberAll changed 1 states/transitions.\n",
|
|
"Optimization done (0.0 sec)\n",
|
|
"\n",
|
|
"Generating next-state function ...\n",
|
|
" Instantiating processes\n",
|
|
" Statically binding references\n",
|
|
" Creating transitions\n",
|
|
"Generating next-state function done (0.0 sec)\n",
|
|
"\n",
|
|
"Creating state vector\n",
|
|
"Creating state labels\n",
|
|
"Generating transitions/state dependency matrices (2 / 3 slots) ... \n",
|
|
"\n",
|
|
" [.......... ]\n",
|
|
" [.................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [........................................ ]\n",
|
|
" [..................................................]\n",
|
|
" Found 5 / 15 ( 33.3%) Guard/slot reads \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 6 / 6 (100.0%) Transition/slot tests \n",
|
|
"\n",
|
|
" [........ ]\n",
|
|
" [................ ]\n",
|
|
" [......................... ]\n",
|
|
" [................................. ]\n",
|
|
" [......................................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 2, 4, 4 / 18 ( 11.1%, 22.2%, 22.2%) Actions/slot r,W,w \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 2, 4, 4 / 6 ( 33.3%, 66.7%, 66.7%) Atomics/slot r,W,w \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 6, 4, 4 / 6 (100.0%, 66.7%, 66.7%) Transition/slot r,W,w \n",
|
|
"Generating transition/state dependency matrices done (0.0 sec)\n",
|
|
"\n",
|
|
"Generating guard dependency matrices (5 guards) ...\n",
|
|
"\n",
|
|
" [.... ]\n",
|
|
" [........ ]\n",
|
|
" [............ ]\n",
|
|
" [................ ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [............................. ]\n",
|
|
" [................................. ]\n",
|
|
" [..................................... ]\n",
|
|
" [......................................... ]\n",
|
|
" Found 3 / 12 ( 25.0%) Guard/guard dependencies \n",
|
|
"\n",
|
|
" [..... ]\n",
|
|
" [.......... ]\n",
|
|
" [............... ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [............................................. ]\n",
|
|
" [..................................................]\n",
|
|
" Found 8 / 10 ( 80.0%) Transition/guard writes \n",
|
|
"\n",
|
|
" Found 4 / 4 (100.0%) Transition/transition writes \n",
|
|
"\n",
|
|
" [.... ]\n",
|
|
" [........ ]\n",
|
|
" [............ ]\n",
|
|
" [................ ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [............................. ]\n",
|
|
" [................................. ]\n",
|
|
" [..................................... ]\n",
|
|
" [......................................... ]\n",
|
|
" Found 2 / 12 ( 16.7%) !MCE guards \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" Found 1 / 2 ( 50.0%) !MCE transitions \n",
|
|
"\n",
|
|
" [.. ]\n",
|
|
" [.... ]\n",
|
|
" [...... ]\n",
|
|
" [........ ]\n",
|
|
" [.......... ]\n",
|
|
" [............ ]\n",
|
|
" [.............. ]\n",
|
|
" [................ ]\n",
|
|
" [.................. ]\n",
|
|
" [.................... ]\n",
|
|
" [...................... ]\n",
|
|
" [........................ ]\n",
|
|
" [.......................... ]\n",
|
|
" [............................ ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................ ]\n",
|
|
" [.................................. ]\n",
|
|
" [.................................... ]\n",
|
|
" [...................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [.......................................... ]\n",
|
|
" [............................................ ]\n",
|
|
" [.............................................. ]\n",
|
|
" [................................................ ]\n",
|
|
" [..................................................]\n",
|
|
" Found 7 / 25 ( 28.0%) !ICE guards \n",
|
|
"\n",
|
|
" [..... ]\n",
|
|
" [.......... ]\n",
|
|
" [............... ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [............................................. ]\n",
|
|
" [..................................................]\n",
|
|
" Found 10 / 10 (100.0%) !NES guards \n",
|
|
"\n",
|
|
" [............ ]\n",
|
|
" [......................... ]\n",
|
|
" [..................................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 4 / 4 (100.0%) !NES transitions \n",
|
|
"\n",
|
|
" [..... ]\n",
|
|
" [.......... ]\n",
|
|
" [............... ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [............................................. ]\n",
|
|
" [..................................................]\n",
|
|
" Found 8 / 10 ( 80.0%) !NDS guards \n",
|
|
"\n",
|
|
" [..... ]\n",
|
|
" [.......... ]\n",
|
|
" [............... ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [............................................. ]\n",
|
|
" [..................................................]\n",
|
|
" Found 0 / 10 ( 0.0%) MDS guards \n",
|
|
"\n",
|
|
" [..... ]\n",
|
|
" [.......... ]\n",
|
|
" [............... ]\n",
|
|
" [.................... ]\n",
|
|
" [......................... ]\n",
|
|
" [.............................. ]\n",
|
|
" [................................... ]\n",
|
|
" [........................................ ]\n",
|
|
" [............................................. ]\n",
|
|
" [..................................................]\n",
|
|
" Found 4 / 10 ( 40.0%) MES guards \n",
|
|
"\n",
|
|
" [............ ]\n",
|
|
" [......................... ]\n",
|
|
" [..................................... ]\n",
|
|
" [..................................................]\n",
|
|
" Found 0 / 4 ( 0.0%) !NDS transitions \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" Found 0 / 2 ( 0.0%) !DNA transitions \n",
|
|
"\n",
|
|
" [......................... ]\n",
|
|
" [..................................................]\n",
|
|
" [..................................................]\n",
|
|
" Found 2 / 2 (100.0%) Commuting actions \n",
|
|
"Generating guard dependency matrices done (0.1 sec)\n",
|
|
"\n",
|
|
"Written C code to /home/adl/git/spot/tests/python/tmpb2gyak36.pml.spins.c\n",
|
|
"Compiled C code to PINS library tmpb2gyak36.pml.spins\n",
|
|
"\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"%%pml model\n",
|
|
"active proctype P() {\n",
|
|
"int a = 0;\n",
|
|
"int b = 0;\n",
|
|
"x: if\n",
|
|
" :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n",
|
|
" :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n",
|
|
"fi;\n",
|
|
"}"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Yes, the `spins` compiler is quite verbose. Printing the resulting `model` object will show information about the variables in that model. "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"text/plain": [
|
|
"ltsmin model with the following variables:\n",
|
|
" P_0._pc: pc\n",
|
|
" P_0.a: int\n",
|
|
" P_0.b: int"
|
|
]
|
|
},
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"model"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"To instantiate a Kripke structure, one should provide a list of atomic proposition to observe."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"120pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 119.62\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.3401360544217687 0.3401360544217687) rotate(0) translate(4 347.74)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-347.74 2154.23,-347.74 2154.23,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1072.11\" y=\"-328.54\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1064.11\" y=\"-313.54\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"197.51\" cy=\"-152.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"108.01\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=0, P_0.b=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"92.01\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.14,-152.87C2.5,-152.87 13.48,-152.87 29.6,-152.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"36.82,-152.87 29.82,-156.02 33.32,-152.87 29.82,-152.87 29.82,-152.87 29.82,-152.87 33.32,-152.87 29.82,-149.72 36.82,-152.87 36.82,-152.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"554.54\" cy=\"-188.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"465.04\" y=\"-192.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=1, P_0.b=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"449.04\" y=\"-177.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M335.27,-166.74C359.62,-169.21 385.06,-171.79 409.61,-174.28\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"416.86,-175.01 409.57,-177.44 413.37,-174.66 409.89,-174.3 409.89,-174.3 409.89,-174.3 413.37,-174.66 410.21,-171.17 416.86,-175.01 416.86,-175.01\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"554.54\" cy=\"-116.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"465.04\" y=\"-120.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=0, P_0.b=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"449.04\" y=\"-105.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M335.27,-139C359.62,-136.53 385.06,-133.95 409.61,-131.46\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"416.86,-130.73 410.21,-134.57 413.37,-131.08 409.89,-131.44 409.89,-131.44 409.89,-131.44 413.37,-131.08 409.57,-128.3 416.86,-130.73 416.86,-130.73\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"914.39\" cy=\"-224.87\" rx=\"163.18\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"824.89\" y=\"-228.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=2, P_0.b=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"806.89\" y=\"-213.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M692.62,-202.66C717.22,-205.14 742.95,-207.72 767.78,-210.22\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"774.76,-210.92 767.48,-213.36 771.28,-210.57 767.8,-210.22 767.8,-210.22 767.8,-210.22 771.28,-210.57 768.11,-207.09 774.76,-210.92 774.76,-210.92\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"914.39\" cy=\"-152.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"824.89\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=1, P_0.b=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"808.89\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M692.62,-175.08C717.76,-172.55 744.08,-169.9 769.42,-167.35\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"776.54,-166.64 769.89,-170.47 773.06,-166.99 769.57,-167.34 769.57,-167.34 769.57,-167.34 773.06,-166.99 769.26,-164.2 776.54,-166.64 776.54,-166.64\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M692.62,-130.66C717.76,-133.19 744.08,-135.84 769.42,-138.39\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"776.54,-139.1 769.26,-141.54 773.06,-138.75 769.57,-138.4 769.57,-138.4 769.57,-138.4 773.06,-138.75 769.89,-135.27 776.54,-139.1 776.54,-139.1\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"914.39\" cy=\"-80.87\" rx=\"158.28\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"824.89\" y=\"-84.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=0, P_0.b=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"810.39\" y=\"-69.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M692.62,-103.08C718.12,-100.51 744.83,-97.83 770.51,-95.24\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"777.72,-94.52 771.07,-98.35 774.24,-94.87 770.76,-95.22 770.76,-95.22 770.76,-95.22 774.24,-94.87 770.44,-92.09 777.72,-94.52 777.72,-94.52\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1277.08\" cy=\"-260.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1187.58\" y=\"-264.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=3, P_0.b=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1171.58\" y=\"-249.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1054.33,-238.74C1079.63,-241.26 1106.09,-243.9 1131.55,-246.44\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1138.7,-247.16 1131.42,-249.6 1135.22,-246.81 1131.74,-246.46 1131.74,-246.46 1131.74,-246.46 1135.22,-246.81 1132.05,-243.33 1138.7,-247.16 1138.7,-247.16\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\">\n",
|
|
"<title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1277.08\" cy=\"-188.87\" rx=\"163.18\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1187.58\" y=\"-192.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=2, P_0.b=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1169.58\" y=\"-177.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1054.33,-211C1079.09,-208.53 1104.95,-205.95 1129.91,-203.46\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1136.92,-202.76 1130.27,-206.59 1133.44,-203.11 1129.95,-203.45 1129.95,-203.45 1129.95,-203.45 1133.44,-203.11 1129.64,-200.32 1136.92,-202.76 1136.92,-202.76\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1052.53,-166.56C1077.83,-169.08 1104.35,-171.73 1129.91,-174.28\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1137.09,-175 1129.81,-177.44 1133.61,-174.65 1130.13,-174.3 1130.13,-174.3 1130.13,-174.3 1133.61,-174.65 1130.44,-171.17 1137.09,-175 1137.09,-175\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\">\n",
|
|
"<title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1277.08\" cy=\"-116.87\" rx=\"158.28\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1187.58\" y=\"-120.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=1, P_0.b=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1173.08\" y=\"-105.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1052.53,-139.18C1078.85,-136.56 1106.49,-133.8 1133,-131.15\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1140.08,-130.44 1133.43,-134.27 1136.6,-130.79 1133.12,-131.14 1133.12,-131.14 1133.12,-131.14 1136.6,-130.79 1132.8,-128 1140.08,-130.44 1140.08,-130.44\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1051.24,-94.43C1077.91,-97.09 1105.97,-99.89 1132.87,-102.58\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1140.06,-103.29 1132.78,-105.73 1136.57,-102.95 1133.09,-102.6 1133.09,-102.6 1133.09,-102.6 1136.57,-102.95 1133.4,-99.46 1140.06,-103.29 1140.06,-103.29\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node11\" class=\"node\">\n",
|
|
"<title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1277.08\" cy=\"-26.87\" rx=\"155.63\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1187.58\" y=\"-30.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=0, P_0.b=3</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1175.08\" y=\"-15.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\">\n",
|
|
"<title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1033.75,-63.15C1071.64,-57.48 1113.7,-51.18 1151.99,-45.45\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1159.1,-44.38 1152.64,-48.54 1155.64,-44.9 1152.17,-45.42 1152.17,-45.42 1152.17,-45.42 1155.64,-44.9 1151.71,-42.31 1159.1,-44.38 1159.1,-44.38\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\">\n",
|
|
"<title>6->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1210.76,-285.79C1205.33,-296.54 1227.43,-305.74 1277.08,-305.74 1315.09,-305.74 1336.95,-300.35 1342.68,-292.99\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1343.4,-285.79 1345.84,-293.07 1343.05,-289.27 1342.7,-292.75 1342.7,-292.75 1342.7,-292.75 1343.05,-289.27 1339.57,-292.44 1343.4,-285.79 1343.4,-285.79\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10 -->\n",
|
|
"<g id=\"node12\" class=\"node\">\n",
|
|
"<title>10</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1636.93\" cy=\"-224.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1547.43\" y=\"-228.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=3, P_0.b=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1531.43\" y=\"-213.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->10 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\">\n",
|
|
"<title>7->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1416.95,-202.84C1441.44,-205.3 1467,-207.88 1491.64,-210.35\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.91,-211.09 1491.63,-213.52 1495.43,-210.74 1491.94,-210.38 1491.94,-210.38 1491.94,-210.38 1495.43,-210.74 1492.26,-207.25 1498.91,-211.09 1498.91,-211.09\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11 -->\n",
|
|
"<g id=\"node13\" class=\"node\">\n",
|
|
"<title>11</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1636.93\" cy=\"-152.87\" rx=\"160.53\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1547.43\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=2, P_0.b=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1531.43\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->11 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\">\n",
|
|
"<title>7->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1416.95,-174.9C1441.44,-172.44 1467,-169.86 1491.64,-167.39\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.91,-166.65 1492.26,-170.49 1495.43,-167 1491.94,-167.36 1491.94,-167.36 1491.94,-167.36 1495.43,-167 1491.63,-164.22 1498.91,-166.65 1498.91,-166.65\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8->11 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\">\n",
|
|
"<title>8->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1413.62,-130.51C1439.12,-133.07 1465.87,-135.76 1491.62,-138.35\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.85,-139.08 1491.57,-141.51 1495.37,-138.73 1491.89,-138.38 1491.89,-138.38 1491.89,-138.38 1495.37,-138.73 1492.2,-135.25 1498.85,-139.08 1498.85,-139.08\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12 -->\n",
|
|
"<g id=\"node14\" class=\"node\">\n",
|
|
"<title>12</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1636.93\" cy=\"-62.87\" rx=\"155.63\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1547.43\" y=\"-66.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=1, P_0.b=3</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1534.93\" y=\"-51.67\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->12 -->\n",
|
|
"<g id=\"edge18\" class=\"edge\">\n",
|
|
"<title>8->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1396.24,-99.04C1433.43,-93.43 1474.58,-87.22 1512.14,-81.55\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1519.11,-80.5 1512.66,-84.66 1515.65,-81.02 1512.19,-81.54 1512.19,-81.54 1512.19,-81.54 1515.65,-81.02 1511.72,-78.43 1519.11,-80.5 1519.11,-80.5\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9->9 -->\n",
|
|
"<g id=\"edge19\" class=\"edge\">\n",
|
|
"<title>9->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1211,-51.33C1204.71,-62.28 1226.73,-71.74 1277.08,-71.74 1315.62,-71.74 1337.57,-66.19 1342.91,-58.68\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1343.15,-51.33 1346.07,-58.43 1343.04,-54.83 1342.92,-58.33 1342.92,-58.33 1342.92,-58.33 1343.04,-54.83 1339.78,-58.22 1343.15,-51.33 1343.15,-51.33\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10->10 -->\n",
|
|
"<g id=\"edge20\" class=\"edge\">\n",
|
|
"<title>10->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1571.35,-249.79C1565.98,-260.54 1587.84,-269.74 1636.93,-269.74 1674.52,-269.74 1696.14,-264.35 1701.8,-256.99\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1702.51,-249.79 1704.96,-257.06 1702.17,-253.27 1701.83,-256.75 1701.83,-256.75 1701.83,-256.75 1702.17,-253.27 1698.69,-256.44 1702.51,-249.79 1702.51,-249.79\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13 -->\n",
|
|
"<g id=\"node15\" class=\"node\">\n",
|
|
"<title>13</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1991.84\" cy=\"-197.87\" rx=\"158.28\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1902.34\" y=\"-201.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=3, P_0.b=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1887.84\" y=\"-186.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 11->13 -->\n",
|
|
"<g id=\"edge21\" class=\"edge\">\n",
|
|
"<title>11->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1765.34,-169.12C1795.32,-172.94 1827.34,-177.02 1857.57,-180.88\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1864.8,-181.8 1857.46,-184.04 1861.33,-181.36 1857.86,-180.91 1857.86,-180.91 1857.86,-180.91 1861.33,-181.36 1858.26,-177.79 1864.8,-181.8 1864.8,-181.8\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14 -->\n",
|
|
"<g id=\"node16\" class=\"node\">\n",
|
|
"<title>14</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1991.84\" cy=\"-107.87\" rx=\"158.28\" ry=\"26.74\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1902.34\" y=\"-111.67\" font-family=\"Lato\" font-size=\"14.00\">P_0._pc=0, P_0.a=2, P_0.b=3</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1887.84\" y=\"-96.67\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 11->14 -->\n",
|
|
"<g id=\"edge22\" class=\"edge\">\n",
|
|
"<title>11->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1765.34,-136.62C1795.32,-132.8 1827.34,-128.72 1857.57,-124.86\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1864.8,-123.94 1858.26,-127.95 1861.33,-124.38 1857.86,-124.83 1857.86,-124.83 1857.86,-124.83 1861.33,-124.38 1857.46,-121.7 1864.8,-123.94 1864.8,-123.94\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12->12 -->\n",
|
|
"<g id=\"edge23\" class=\"edge\">\n",
|
|
"<title>12->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1571.59,-87.33C1565.37,-98.28 1587.15,-107.74 1636.93,-107.74 1675.05,-107.74 1696.75,-102.19 1702.03,-94.68\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1702.27,-87.33 1705.19,-94.43 1702.16,-90.83 1702.04,-94.33 1702.04,-94.33 1702.04,-94.33 1702.16,-90.83 1698.89,-94.23 1702.27,-87.33 1702.27,-87.33\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13->13 -->\n",
|
|
"<g id=\"edge24\" class=\"edge\">\n",
|
|
"<title>13->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1926.26,-222.79C1920.89,-233.54 1942.75,-242.74 1991.84,-242.74 2029.42,-242.74 2051.05,-237.35 2056.71,-229.99\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"2057.42,-222.79 2059.87,-230.06 2057.07,-226.27 2056.73,-229.75 2056.73,-229.75 2056.73,-229.75 2057.07,-226.27 2053.6,-229.44 2057.42,-222.79 2057.42,-222.79\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14->14 -->\n",
|
|
"<g id=\"edge25\" class=\"edge\">\n",
|
|
"<title>14->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1926.26,-132.79C1920.89,-143.54 1942.75,-152.74 1991.84,-152.74 2029.42,-152.74 2051.05,-147.35 2056.71,-139.99\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"2057.42,-132.79 2059.87,-140.06 2057.07,-136.27 2056.73,-139.75 2056.73,-139.75 2056.73,-139.75 2057.07,-136.27 2053.6,-139.44 2057.42,-132.79 2057.42,-132.79\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fb8c8761870> >"
|
|
]
|
|
},
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"And then from this Kripke structure you can do some model checking using the same functions as illustrated in `ltsmin-dve.ipynb`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"For displaying Kripke structures more compactly, it can be useful to use option `1` to move all state labels in tooltips (mouse over the state to see them):"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"455pt\" height=\"280pt\"\n",
|
|
" viewBox=\"0.00 0.00 454.79 280.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 276)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-276 450.79,-276 450.79,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"220.4\" y=\"-256.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
|
"<text text-anchor=\"start\" x=\"212.4\" y=\"-241.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<g id=\"a_node2\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=0 "P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"55\" cy=\"-117\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"55\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-117C2.75,-117 16.68,-117 29.83,-117\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"36.98,-117 29.98,-120.15 33.48,-117 29.98,-117 29.98,-117 29.98,-117 33.48,-117 29.98,-113.85 36.98,-117 36.98,-117\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<g id=\"a_node3\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=0 "P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"127\" cy=\"-144\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"127\" y=\"-140.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M72.24,-123.26C81.42,-126.81 93.06,-131.3 103.16,-135.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"109.85,-137.77 102.19,-138.19 106.59,-136.51 103.32,-135.25 103.32,-135.25 103.32,-135.25 106.59,-136.51 104.46,-132.31 109.85,-137.77 109.85,-137.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<g id=\"a_node4\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=1 "P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"127\" cy=\"-90\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"127\" y=\"-86.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M72.24,-110.74C81.42,-107.19 93.06,-102.7 103.16,-98.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"109.85,-96.23 104.46,-101.69 106.59,-97.49 103.32,-98.75 103.32,-98.75 103.32,-98.75 106.59,-97.49 102.19,-95.81 109.85,-96.23 109.85,-96.23\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<g id=\"a_node5\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=0 !"P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"199\" cy=\"-171\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"199\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.24,-150.26C153.42,-153.81 165.06,-158.3 175.16,-162.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"181.85,-164.77 174.19,-165.19 178.59,-163.51 175.32,-162.25 175.32,-162.25 175.32,-162.25 178.59,-163.51 176.46,-159.31 181.85,-164.77 181.85,-164.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<g id=\"a_node6\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=1 "P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"199\" cy=\"-117\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"199\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.24,-137.74C153.42,-134.19 165.06,-129.7 175.16,-125.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"181.85,-123.23 176.46,-128.69 178.59,-124.49 175.32,-125.75 175.32,-125.75 175.32,-125.75 178.59,-124.49 174.19,-122.81 181.85,-123.23 181.85,-123.23\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.24,-96.26C153.42,-99.81 165.06,-104.3 175.16,-108.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"181.85,-110.77 174.19,-111.19 178.59,-109.51 175.32,-108.25 175.32,-108.25 175.32,-108.25 178.59,-109.51 176.46,-105.31 181.85,-110.77 181.85,-110.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<g id=\"a_node7\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=2 "P_0.a < 2" & "P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"199\" cy=\"-63\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"199\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M144.24,-83.74C153.42,-80.19 165.06,-75.7 175.16,-71.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"181.85,-69.23 176.46,-74.69 178.59,-70.49 175.32,-71.75 175.32,-71.75 175.32,-71.75 178.59,-70.49 174.19,-68.81 181.85,-69.23 181.85,-69.23\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<g id=\"a_node8\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=0 !"P_0.a < 2" & !"P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"271\" cy=\"-198\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"271\" y=\"-194.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M216.24,-177.26C225.42,-180.81 237.06,-185.3 247.16,-189.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"253.85,-191.77 246.19,-192.19 250.59,-190.51 247.32,-189.25 247.32,-189.25 247.32,-189.25 250.59,-190.51 248.46,-186.31 253.85,-191.77 253.85,-191.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\">\n",
|
|
"<title>7</title>\n",
|
|
"<g id=\"a_node9\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=1 !"P_0.a < 2" & !"P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"271\" cy=\"-144\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"271\" y=\"-140.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M216.24,-164.74C225.42,-161.19 237.06,-156.7 247.16,-152.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"253.85,-150.23 248.46,-155.69 250.59,-151.49 247.32,-152.75 247.32,-152.75 247.32,-152.75 250.59,-151.49 246.19,-149.81 253.85,-150.23 253.85,-150.23\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M216.24,-123.26C225.42,-126.81 237.06,-131.3 247.16,-135.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"253.85,-137.77 246.19,-138.19 250.59,-136.51 247.32,-135.25 247.32,-135.25 247.32,-135.25 250.59,-136.51 248.46,-132.31 253.85,-137.77 253.85,-137.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\">\n",
|
|
"<title>8</title>\n",
|
|
"<g id=\"a_node10\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=2 "P_0.a < 2" & "P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"271\" cy=\"-90\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"271\" y=\"-86.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M216.24,-110.74C225.42,-107.19 237.06,-102.7 247.16,-98.81\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"253.85,-96.23 248.46,-101.69 250.59,-97.49 247.32,-98.75 247.32,-98.75 247.32,-98.75 250.59,-97.49 246.19,-95.81 253.85,-96.23 253.85,-96.23\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M216.24,-69.26C225.42,-72.81 237.06,-77.3 247.16,-81.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"253.85,-83.77 246.19,-84.19 250.59,-82.51 247.32,-81.25 247.32,-81.25 247.32,-81.25 250.59,-82.51 248.46,-78.31 253.85,-83.77 253.85,-83.77\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node11\" class=\"node\">\n",
|
|
"<title>9</title>\n",
|
|
"<g id=\"a_node11\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=3 "P_0.a < 2" & "P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"271\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"271\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\">\n",
|
|
"<title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M214.5,-53.68C224.64,-47.16 238.32,-38.37 249.56,-31.14\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"255.51,-27.31 251.33,-33.75 252.57,-29.2 249.63,-31.1 249.63,-31.1 249.63,-31.1 252.57,-29.2 247.92,-28.45 255.51,-27.31 255.51,-27.31\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\">\n",
|
|
"<title>6->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M259.24,-212.04C254.85,-222.91 258.77,-234 271,-234 280.56,-234 285.04,-227.23 284.45,-219.09\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"282.76,-212.04 287.45,-218.11 283.57,-215.45 284.39,-218.85 284.39,-218.85 284.39,-218.85 283.57,-215.45 281.33,-219.58 282.76,-212.04 282.76,-212.04\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10 -->\n",
|
|
"<g id=\"node12\" class=\"node\">\n",
|
|
"<title>10</title>\n",
|
|
"<g id=\"a_node12\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=1 !"P_0.a < 2" & !"P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"346.45\" cy=\"-178\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"346.45\" y=\"-174.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 7->10 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\">\n",
|
|
"<title>7->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M287.58,-151.21C297.06,-155.6 309.4,-161.31 320.25,-166.34\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"326.77,-169.35 319.1,-169.27 323.6,-167.88 320.42,-166.41 320.42,-166.41 320.42,-166.41 323.6,-167.88 321.74,-163.56 326.77,-169.35 326.77,-169.35\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 11 -->\n",
|
|
"<g id=\"node13\" class=\"node\">\n",
|
|
"<title>11</title>\n",
|
|
"<g id=\"a_node13\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=2 !"P_0.a < 2" & "P_0.b > 1" & !dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"346.45\" cy=\"-117\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"346.45\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 7->11 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\">\n",
|
|
"<title>7->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M288.3,-138.01C297.45,-134.64 309.09,-130.37 319.47,-126.55\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"326.07,-124.12 320.58,-129.5 322.78,-125.33 319.5,-126.54 319.5,-126.54 319.5,-126.54 322.78,-125.33 318.41,-123.58 326.07,-124.12 326.07,-124.12\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8->11 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\">\n",
|
|
"<title>8->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M288.3,-95.99C297.45,-99.36 309.09,-103.63 319.47,-107.45\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"326.07,-109.88 318.41,-110.42 322.78,-108.67 319.5,-107.46 319.5,-107.46 319.5,-107.46 322.78,-108.67 320.58,-104.5 326.07,-109.88 326.07,-109.88\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12 -->\n",
|
|
"<g id=\"node14\" class=\"node\">\n",
|
|
"<title>12</title>\n",
|
|
"<g id=\"a_node14\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=3 "P_0.a < 2" & "P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"346.45\" cy=\"-38\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"346.45\" y=\"-34.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 8->12 -->\n",
|
|
"<g id=\"edge18\" class=\"edge\">\n",
|
|
"<title>8->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M286.16,-79.97C296.46,-72.69 310.61,-62.66 322.51,-54.24\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"328.49,-50 324.6,-56.62 325.64,-52.03 322.78,-54.05 322.78,-54.05 322.78,-54.05 325.64,-52.03 320.96,-51.48 328.49,-50 328.49,-50\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9->9 -->\n",
|
|
"<g id=\"edge19\" class=\"edge\">\n",
|
|
"<title>9->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M259.24,-32.04C254.85,-42.91 258.77,-54 271,-54 280.56,-54 285.04,-47.23 284.45,-39.09\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"282.76,-32.04 287.45,-38.11 283.57,-35.45 284.39,-38.85 284.39,-38.85 284.39,-38.85 283.57,-35.45 281.33,-39.58 282.76,-32.04 282.76,-32.04\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 10->10 -->\n",
|
|
"<g id=\"edge20\" class=\"edge\">\n",
|
|
"<title>10->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M333.67,-195.44C330.34,-206.66 334.6,-217.45 346.45,-217.45 355.71,-217.45 360.33,-210.86 360.32,-202.63\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"359.23,-195.44 363.4,-201.89 359.75,-198.9 360.28,-202.36 360.28,-202.36 360.28,-202.36 359.75,-198.9 357.17,-202.84 359.23,-195.44 359.23,-195.44\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13 -->\n",
|
|
"<g id=\"node15\" class=\"node\">\n",
|
|
"<title>13</title>\n",
|
|
"<g id=\"a_node15\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=2 !"P_0.a < 2" & "P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"425.34\" cy=\"-157\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"425.34\" y=\"-153.3\" font-family=\"Lato\" font-size=\"14.00\">13</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 11->13 -->\n",
|
|
"<g id=\"edge21\" class=\"edge\">\n",
|
|
"<title>11->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M366.06,-126.68C376.07,-131.89 388.56,-138.38 399.4,-144.02\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"405.9,-147.41 398.24,-146.97 402.8,-145.79 399.69,-144.18 399.69,-144.18 399.69,-144.18 402.8,-145.79 401.14,-141.38 405.9,-147.41 405.9,-147.41\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14 -->\n",
|
|
"<g id=\"node16\" class=\"node\">\n",
|
|
"<title>14</title>\n",
|
|
"<g id=\"a_node16\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=3 !"P_0.a < 2" & "P_0.b > 1" & dead\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"425.34\" cy=\"-78\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"425.34\" y=\"-74.3\" font-family=\"Lato\" font-size=\"14.00\">14</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 11->14 -->\n",
|
|
"<g id=\"edge22\" class=\"edge\">\n",
|
|
"<title>11->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M366.06,-107.56C376.07,-102.48 388.56,-96.15 399.4,-90.65\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"405.9,-87.35 401.08,-93.33 402.78,-88.94 399.66,-90.52 399.66,-90.52 399.66,-90.52 402.78,-88.94 398.23,-87.71 405.9,-87.35 405.9,-87.35\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 12->12 -->\n",
|
|
"<g id=\"edge23\" class=\"edge\">\n",
|
|
"<title>12->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M333.67,-55.44C330.34,-66.66 334.6,-77.45 346.45,-77.45 355.71,-77.45 360.33,-70.86 360.32,-62.63\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"359.23,-55.44 363.4,-61.89 359.75,-58.9 360.28,-62.36 360.28,-62.36 360.28,-62.36 359.75,-58.9 357.17,-62.84 359.23,-55.44 359.23,-55.44\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 13->13 -->\n",
|
|
"<g id=\"edge24\" class=\"edge\">\n",
|
|
"<title>13->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M412.01,-174.03C408.25,-185.39 412.7,-196.45 425.34,-196.45 435.32,-196.45 440.19,-189.56 439.96,-181.08\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"438.68,-174.03 443.03,-180.35 439.31,-177.47 439.93,-180.92 439.93,-180.92 439.93,-180.92 439.31,-177.47 436.83,-181.48 438.68,-174.03 438.68,-174.03\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 14->14 -->\n",
|
|
"<g id=\"edge25\" class=\"edge\">\n",
|
|
"<title>14->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M412.01,-95.03C408.25,-106.39 412.7,-117.45 425.34,-117.45 435.32,-117.45 440.19,-110.56 439.96,-102.08\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"438.68,-95.03 443.03,-101.35 439.31,-98.47 439.93,-101.92 439.93,-101.92 439.93,-101.92 439.31,-98.47 436.83,-102.48 438.68,-95.03 438.68,-95.03\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.jupyter.SVG object>"
|
|
]
|
|
},
|
|
"execution_count": 5,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"k.show('.1')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Another option is to use option `K` to disable to state-labeling (that is enabled by default for Kripke structure) and use transition-labeling instead. Combining with `1`, this will preserve the state's data as a tooltip."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 6,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"image/svg+xml": [
|
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
|
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
|
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"145pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 144.84\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.4587155963302752 0.4587155963302752) rotate(0) translate(4 312)\">\n",
|
|
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-312 1597.34,-312 1597.34,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"793.67\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
|
"<text text-anchor=\"start\" x=\"785.67\" y=\"-277.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<g id=\"a_node2\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=0\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-124\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"56\" y=\"-120.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-124C2.79,-124 17.15,-124 30.63,-124\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-124 30.94,-127.15 34.44,-124 30.94,-124 30.94,-124 30.94,-124 34.44,-124 30.94,-120.85 37.94,-124 37.94,-124\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<g id=\"a_node3\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=0\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"339\" cy=\"-151\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"339\" y=\"-147.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M74.15,-125.65C122.18,-130.26 258.09,-143.32 313.76,-148.67\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"321.07,-149.37 313.8,-151.84 317.59,-149.04 314.1,-148.7 314.1,-148.7 314.1,-148.7 317.59,-149.04 314.4,-145.57 321.07,-149.37 321.07,-149.37\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-150.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<g id=\"a_node4\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=1\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"339\" cy=\"-97\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"339\" y=\"-93.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M72.28,-116.05C78.27,-113.31 85.3,-110.55 92,-109 171.56,-90.64 269.3,-92.99 313.83,-95.37\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"321.01,-95.78 313.85,-98.53 317.52,-95.58 314.03,-95.39 314.03,-95.39 314.03,-95.39 317.52,-95.58 314.21,-92.24 321.01,-95.78 321.01,-95.78\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"92\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<g id=\"a_node5\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=0\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"622\" cy=\"-181\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"622\" y=\"-177.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M356.65,-155.29C362.42,-156.65 368.97,-158.05 375,-159 455.67,-171.77 552.49,-177.71 596.76,-179.92\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"603.9,-180.27 596.76,-183.08 600.41,-180.1 596.91,-179.93 596.91,-179.93 596.91,-179.93 600.41,-180.1 597.06,-176.78 603.9,-180.27 603.9,-180.27\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"375\" y=\"-182.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<g id=\"a_node6\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=1\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"622\" cy=\"-124\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"622\" y=\"-120.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M356.67,-147.26C362.45,-146.07 368.99,-144.84 375,-144 455.83,-132.67 552.57,-127.13 596.79,-125.03\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"603.93,-124.7 597.08,-128.17 600.43,-124.87 596.93,-125.03 596.93,-125.03 596.93,-125.03 600.43,-124.87 596.79,-121.88 603.93,-124.7 603.93,-124.7\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"375\" y=\"-147.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M357.04,-95.34C397.51,-91.89 502.27,-85.94 586,-107 590.56,-108.15 595.22,-109.92 599.6,-111.91\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"606.19,-115.13 598.51,-114.88 603.04,-113.59 599.9,-112.05 599.9,-112.05 599.9,-112.05 603.04,-113.59 601.28,-109.22 606.19,-115.13 606.19,-115.13\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"375\" y=\"-110.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<g id=\"a_node7\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=2\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"622\" cy=\"-67\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"622\" y=\"-63.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M352.98,-85.42C359.19,-80.63 367.01,-75.58 375,-73 452.97,-47.79 552.21,-56.99 597.07,-63.19\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"604.04,-64.19 596.67,-66.31 600.58,-63.69 597.11,-63.19 597.11,-63.19 597.11,-63.19 600.58,-63.69 597.56,-60.08 604.04,-64.19 604.04,-64.19\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"375\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<g id=\"a_node8\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=0\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"909\" cy=\"-219\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"909\" y=\"-215.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M638.26,-189.35C644.25,-192.25 651.28,-195.23 658,-197 738.81,-218.35 838.88,-220.06 883.98,-219.57\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"890.98,-219.47 884.03,-222.72 887.48,-219.52 883.99,-219.57 883.99,-219.57 883.99,-219.57 887.48,-219.52 883.94,-216.42 890.98,-219.47 890.98,-219.47\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"658\" y=\"-222.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\">\n",
|
|
"<title>7</title>\n",
|
|
"<g id=\"a_node9\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=1\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"909\" cy=\"-162\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"909\" y=\"-158.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M639.97,-179.87C688.37,-176.64 827.19,-167.39 883.66,-163.62\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"890.75,-163.15 883.98,-166.76 887.26,-163.38 883.77,-163.62 883.77,-163.62 883.77,-163.62 887.26,-163.38 883.56,-160.47 890.75,-163.15 890.75,-163.15\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"658\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M640.05,-123.31C681.02,-122.1 787.95,-121.65 873,-145 877.53,-146.24 882.18,-148.07 886.56,-150.06\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"893.14,-153.28 885.47,-153.04 890,-151.75 886.86,-150.21 886.86,-150.21 886.86,-150.21 890,-151.75 888.24,-147.38 893.14,-153.28 893.14,-153.28\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"660\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\">\n",
|
|
"<title>8</title>\n",
|
|
"<g id=\"a_node10\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=2\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"909\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"909\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M637.72,-114.47C643.75,-111.1 650.96,-107.72 658,-106 738.88,-86.25 838.92,-95.54 883.99,-101.43\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"890.99,-102.38 883.64,-104.56 887.53,-101.91 884.06,-101.44 884.06,-101.44 884.06,-101.44 887.53,-101.91 884.48,-98.32 890.99,-102.38 890.99,-102.38\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"660\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M639.81,-64.01C681.15,-57.41 790.41,-44.54 873,-76 879.5,-78.48 885.67,-82.68 890.97,-87.14\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"896.35,-92 889.05,-89.64 893.76,-89.65 891.16,-87.31 891.16,-87.31 891.16,-87.31 893.76,-89.65 893.27,-84.97 896.35,-92 896.35,-92\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"661.5\" y=\"-79.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node11\" class=\"node\">\n",
|
|
"<title>9</title>\n",
|
|
"<g id=\"a_node11\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=3\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"909\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"909\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\">\n",
|
|
"<title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M634.62,-53.7C640.88,-47.49 649.13,-40.67 658,-37 735.54,-4.93 838.06,-10.38 883.97,-15.03\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"891.1,-15.8 883.8,-18.18 887.62,-15.42 884.14,-15.05 884.14,-15.05 884.14,-15.05 887.62,-15.42 884.47,-11.92 891.1,-15.8 891.1,-15.8\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"661.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\">\n",
|
|
"<title>6->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M892.52,-226.96C874.8,-239.31 880.29,-255 909,-255 934.12,-255 941.46,-242.99 931.04,-231.71\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"925.48,-226.96 932.85,-229.11 928.14,-229.23 930.8,-231.51 930.8,-231.51 930.8,-231.51 928.14,-229.23 928.76,-233.9 925.48,-226.96 925.48,-226.96\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"803.5\" y=\"-258.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 10 -->\n",
|
|
"<g id=\"node12\" class=\"node\">\n",
|
|
"<title>10</title>\n",
|
|
"<g id=\"a_node12\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=1\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1199.45\" cy=\"-209\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1199.45\" y=\"-205.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 7->10 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\">\n",
|
|
"<title>7->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M924.89,-170.6C930.95,-173.73 938.13,-176.99 945,-179 1024.72,-202.35 1123.6,-207.59 1170.82,-208.72\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1177.95,-208.87 1170.88,-211.87 1174.45,-208.8 1170.95,-208.72 1170.95,-208.72 1170.95,-208.72 1174.45,-208.8 1171.02,-205.58 1177.95,-208.87 1177.95,-208.87\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"945\" y=\"-211.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 11 -->\n",
|
|
"<g id=\"node13\" class=\"node\">\n",
|
|
"<title>11</title>\n",
|
|
"<g id=\"a_node13\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=2\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1199.45\" cy=\"-148\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1199.45\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 7->11 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\">\n",
|
|
"<title>7->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M927.18,-161.17C975.33,-158.83 1111.92,-152.2 1170.84,-149.34\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1177.96,-148.99 1171.12,-152.48 1174.46,-149.16 1170.96,-149.33 1170.96,-149.33 1170.96,-149.33 1174.46,-149.16 1170.81,-146.19 1177.96,-148.99 1177.96,-148.99\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"945\" y=\"-163.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->11 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\">\n",
|
|
"<title>8->11</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M927,-104.96C967.88,-105.24 1074.6,-108.29 1160,-131 1164.44,-132.18 1169.03,-133.81 1173.42,-135.6\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1180.1,-138.49 1172.42,-138.6 1176.89,-137.1 1173.68,-135.71 1173.68,-135.71 1173.68,-135.71 1176.89,-137.1 1174.93,-132.82 1180.1,-138.49 1180.1,-138.49\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"948.5\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12 -->\n",
|
|
"<g id=\"node14\" class=\"node\">\n",
|
|
"<title>12</title>\n",
|
|
"<g id=\"a_node14\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=3\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1199.45\" cy=\"-54\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1199.45\" y=\"-50.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 8->12 -->\n",
|
|
"<g id=\"edge18\" class=\"edge\">\n",
|
|
"<title>8->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M924.85,-95.92C930.9,-92.61 938.09,-89.16 945,-87 1024.42,-62.24 1123.44,-56.05 1170.76,-54.51\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1177.9,-54.3 1170.99,-57.65 1174.4,-54.4 1170.9,-54.5 1170.9,-54.5 1170.9,-54.5 1174.4,-54.4 1170.81,-51.35 1177.9,-54.3 1177.9,-54.3\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"948.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->9 -->\n",
|
|
"<g id=\"edge19\" class=\"edge\">\n",
|
|
"<title>9->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M892.52,-25.96C874.8,-38.31 880.29,-54 909,-54 934.12,-54 941.46,-41.99 931.04,-30.71\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"925.48,-25.96 932.85,-28.11 928.14,-28.23 930.8,-30.51 930.8,-30.51 930.8,-30.51 928.14,-28.23 928.76,-32.9 925.48,-25.96 925.48,-25.96\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"807\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 10->10 -->\n",
|
|
"<g id=\"edge20\" class=\"edge\">\n",
|
|
"<title>10->10</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1180.52,-219.5C1165.3,-232.72 1171.6,-248.45 1199.45,-248.45 1223.59,-248.45 1231.54,-236.62 1223.3,-224.86\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1218.37,-219.5 1225.43,-222.52 1220.74,-222.08 1223.11,-224.65 1223.11,-224.65 1223.11,-224.65 1220.74,-222.08 1220.8,-226.79 1218.37,-219.5 1218.37,-219.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1093.95\" y=\"-252.25\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & !"P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 13 -->\n",
|
|
"<g id=\"node15\" class=\"node\">\n",
|
|
"<title>13</title>\n",
|
|
"<g id=\"a_node15\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=2\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1489.34\" cy=\"-188\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1489.34\" y=\"-184.3\" font-family=\"Lato\" font-size=\"14.00\">13</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 11->13 -->\n",
|
|
"<g id=\"edge21\" class=\"edge\">\n",
|
|
"<title>11->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1221.15,-150.88C1272.09,-157.95 1403.52,-176.22 1460.89,-184.18\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1467.83,-185.15 1460.46,-187.31 1464.36,-184.67 1460.89,-184.19 1460.89,-184.19 1460.89,-184.19 1464.36,-184.67 1461.33,-181.07 1467.83,-185.15 1467.83,-185.15\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1238.9\" y=\"-185.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 14 -->\n",
|
|
"<g id=\"node16\" class=\"node\">\n",
|
|
"<title>14</title>\n",
|
|
"<g id=\"a_node16\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=3\">\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1489.34\" cy=\"-94\" rx=\"21.4\" ry=\"21.4\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1489.34\" y=\"-90.3\" font-family=\"Lato\" font-size=\"14.00\">14</text>\n",
|
|
"</a>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"<!-- 11->14 -->\n",
|
|
"<g id=\"edge22\" class=\"edge\">\n",
|
|
"<title>11->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1219.78,-140.15C1225.83,-137.91 1232.57,-135.64 1238.9,-134 1318.08,-113.44 1414.3,-101.6 1460.69,-96.7\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1467.7,-95.97 1461.06,-99.82 1464.22,-96.33 1460.74,-96.69 1460.74,-96.69 1460.74,-96.69 1464.22,-96.33 1460.41,-93.56 1467.7,-95.97 1467.7,-95.97\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1238.9\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 12->12 -->\n",
|
|
"<g id=\"edge23\" class=\"edge\">\n",
|
|
"<title>12->12</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1180.52,-64.5C1165.3,-77.72 1171.6,-93.45 1199.45,-93.45 1223.59,-93.45 1231.54,-81.62 1223.3,-69.86\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1218.37,-64.5 1225.43,-67.52 1220.74,-67.08 1223.11,-69.65 1223.11,-69.65 1223.11,-69.65 1220.74,-67.08 1220.8,-71.79 1218.37,-64.5 1218.37,-64.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1097.45\" y=\"-97.25\" font-family=\"Lato\" font-size=\"14.00\">"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 13->13 -->\n",
|
|
"<g id=\"edge24\" class=\"edge\">\n",
|
|
"<title>13->13</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1470.42,-198.5C1455.19,-211.72 1461.5,-227.45 1489.34,-227.45 1513.49,-227.45 1521.44,-215.62 1513.2,-203.86\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1508.27,-198.5 1515.33,-201.52 1510.64,-201.08 1513.01,-203.65 1513.01,-203.65 1513.01,-203.65 1510.64,-201.08 1510.69,-205.79 1508.27,-198.5 1508.27,-198.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1385.34\" y=\"-231.25\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 14->14 -->\n",
|
|
"<g id=\"edge25\" class=\"edge\">\n",
|
|
"<title>14->14</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1470.42,-104.5C1455.19,-117.72 1461.5,-133.45 1489.34,-133.45 1513.49,-133.45 1521.44,-121.62 1513.2,-109.86\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1508.27,-104.5 1515.33,-107.52 1510.64,-107.08 1513.01,-109.65 1513.01,-109.65 1513.01,-109.65 1510.64,-107.08 1510.69,-111.79 1508.27,-104.5 1508.27,-104.5\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1385.34\" y=\"-137.25\" font-family=\"Lato\" font-size=\"14.00\">!"P_0.a < 2" & "P_0.b > 1" & dead</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.jupyter.SVG object>"
|
|
]
|
|
},
|
|
"execution_count": 6,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"k.show('.1K')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Loading from a `*.pml` file\n",
|
|
"---------------------------\n",
|
|
"\n",
|
|
"Another option is to use `ltsmin.load()` to load a Promela file directly. In order for this test-case to be self-contained, we are going to write the Promela file first, but in practice you probably already have your model."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 7,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"!rm -rf test1.pml"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 8,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"Writing test1.pml\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"%%file test1.pml\n",
|
|
"active proctype P() {\n",
|
|
"int a = 0;\n",
|
|
"int b = 0;\n",
|
|
"x: if\n",
|
|
" :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n",
|
|
" :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n",
|
|
"fi;\n",
|
|
"}"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Now load it:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 9,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"model2 = spot.ltsmin.load('test1.pml')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 10,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"text/plain": [
|
|
"ltsmin model with the following variables:\n",
|
|
" P_0._pc: pc\n",
|
|
" P_0.a: int\n",
|
|
" P_0.b: int"
|
|
]
|
|
},
|
|
"execution_count": 10,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"model2"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 11,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"!rm -f test1.pml test1.pml.spins.c test1.pml.spins"
|
|
]
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.7.5"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 2
|
|
}
|