6a808492c1
* python/spot/impl.i, python/spot/__init__.py: Implement it. * NEWS: Mention it. * tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb, tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb, tests/python/stutter-inv.ipynb, doc/org/tut02.org: Modernize.
356 lines
20 KiB
Text
356 lines
20 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"This example is the right part of Fig.2 in our ATVA'16 paper titled [\"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"](https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf) slightly updated to benefit from improvements in more recent versions of Spot."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"import spot\n",
|
|
"import spot.ltsmin\n",
|
|
"spot.setup(show_default='.Ab', max_states=10)\n",
|
|
"# This extra line ensures that our test suite skips this test if divine is not installed.\n",
|
|
"spot.ltsmin.require('divine')"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"%%dve adding\n",
|
|
"int c=1, x1, x2;\n",
|
|
"process a1 {\n",
|
|
" state Q, R, S; init Q;\n",
|
|
" trans Q -> R { guard c<20; effect x1 = c; },\n",
|
|
" R -> S { effect x1 = x1 + c; },\n",
|
|
" S -> Q { effect c = x1; };\n",
|
|
"}\n",
|
|
"process a2 {\n",
|
|
" state Q, R, S; init Q;\n",
|
|
" trans Q -> R { guard c<20; effect x2 = c; },\n",
|
|
" R -> S { effect x2 = x2 + c; },\n",
|
|
" S -> Q { effect c = x2; };\n",
|
|
"}\n",
|
|
"system async;"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"text/plain": [
|
|
"ltsmin model with the following variables:\n",
|
|
" c: int\n",
|
|
" x1: int\n",
|
|
" x2: int\n",
|
|
" a1: ['Q', 'R', 'S']\n",
|
|
" a2: ['Q', 'R', 'S']"
|
|
]
|
|
},
|
|
"execution_count": 3,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"adding"
|
|
]
|
|
},
|
|
{
|
|
"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.40.1 (20161225.0304)\n",
|
|
" -->\n",
|
|
"<!-- Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"156pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 156.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(.5617 .5617) rotate(0) translate(4 273.7401)\">\n",
|
|
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-273.7401 1302.7729,-273.7401 1302.7729,4 -4,4\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\">\n",
|
|
"<title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"173.4716\" cy=\"-134.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"84.9716\" y=\"-138.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=0, x2=0, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"96.4716\" y=\"-123.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\">\n",
|
|
"<title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.2712,-134.8701C4.1455,-134.8701 14.8325,-134.8701 29.5805,-134.8701\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"36.6289,-134.8701 29.6289,-138.0202 33.1289,-134.8701 29.6289,-134.8702 29.6289,-134.8702 29.6289,-134.8702 33.1289,-134.8701 29.6288,-131.7202 36.6289,-134.8701 36.6289,-134.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\">\n",
|
|
"<title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"482.4148\" cy=\"-170.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"393.9148\" y=\"-174.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=1, x2=0, a1=1, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"403.4148\" y=\"-159.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\">\n",
|
|
"<title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M291.1511,-148.5828C312.9236,-151.1199 335.7316,-153.7776 357.7045,-156.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"364.8068,-157.1656 357.4892,-159.4842 361.3303,-156.7605 357.8538,-156.3553 357.8538,-156.3553 357.8538,-156.3553 361.3303,-156.7605 358.2185,-153.2265 364.8068,-157.1656 364.8068,-157.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\">\n",
|
|
"<title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"482.4148\" cy=\"-98.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"393.9148\" y=\"-102.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=0, x2=1, a1=0, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"405.4148\" y=\"-87.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\">\n",
|
|
"<title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M291.1511,-121.1573C312.9236,-118.6202 335.7316,-115.9625 357.7045,-113.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"364.8068,-112.5745 358.2185,-116.5136 361.3303,-112.9796 357.8538,-113.3848 357.8538,-113.3848 357.8538,-113.3848 361.3303,-112.9796 357.4892,-110.2559 364.8068,-112.5745 364.8068,-112.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\">\n",
|
|
"<title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"791.358\" cy=\"-206.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-210.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=2, x2=0, a1=2, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"712.358\" y=\"-195.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\">\n",
|
|
"<title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M600.0943,-184.5828C621.8668,-187.1199 644.6748,-189.7776 666.6477,-192.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"673.75,-193.1656 666.4324,-195.4842 670.2735,-192.7605 666.7971,-192.3553 666.7971,-192.3553 666.7971,-192.3553 670.2735,-192.7605 667.1617,-189.2265 673.75,-193.1656 673.75,-193.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\">\n",
|
|
"<title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"791.358\" cy=\"-134.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-138.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=1, x2=1, a1=1, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"712.358\" y=\"-123.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\">\n",
|
|
"<title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M600.0943,-157.1573C621.8668,-154.6202 644.6748,-151.9625 666.6477,-149.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"673.75,-148.5745 667.1617,-152.5136 670.2735,-148.9796 666.7971,-149.3848 666.7971,-149.3848 666.7971,-149.3848 670.2735,-148.9796 666.4324,-146.2559 673.75,-148.5745 673.75,-148.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\">\n",
|
|
"<title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M600.0943,-112.5828C621.8668,-115.1199 644.6748,-117.7776 666.6477,-120.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"673.75,-121.1656 666.4324,-123.4842 670.2735,-120.7605 666.7971,-120.3553 666.7971,-120.3553 666.7971,-120.3553 670.2735,-120.7605 667.1617,-117.2265 673.75,-121.1656 673.75,-121.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\">\n",
|
|
"<title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"791.358\" cy=\"-62.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=0, x2=2, a1=0, a2=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"714.358\" y=\"-51.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\">\n",
|
|
"<title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M600.0943,-85.1573C621.8668,-82.6202 644.6748,-79.9625 666.6477,-77.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"673.75,-76.5745 667.1617,-80.5136 670.2735,-76.9796 666.7971,-77.3848 666.7971,-77.3848 666.7971,-77.3848 670.2735,-76.9796 666.4324,-74.2559 673.75,-76.5745 673.75,-76.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\">\n",
|
|
"<title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1100.3013\" cy=\"-242.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8013\" y=\"-246.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=2, x1=2, x2=0, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3013\" y=\"-231.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\">\n",
|
|
"<title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-220.5828C930.8101,-223.1199 953.618,-225.7776 975.5909,-228.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-229.1656 975.3757,-231.4842 979.2168,-228.7605 975.7403,-228.3553 975.7403,-228.3553 975.7403,-228.3553 979.2168,-228.7605 976.1049,-225.2265 982.6932,-229.1656 982.6932,-229.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\">\n",
|
|
"<title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1100.3013\" cy=\"-170.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8013\" y=\"-174.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=2, x2=1, a1=2, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3013\" y=\"-159.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\">\n",
|
|
"<title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-193.1573C930.8101,-190.6202 953.618,-187.9625 975.5909,-185.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-184.5745 976.1049,-188.5136 979.2168,-184.9796 975.7403,-185.3848 975.7403,-185.3848 975.7403,-185.3848 979.2168,-184.9796 975.3757,-182.2559 982.6932,-184.5745 982.6932,-184.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\">\n",
|
|
"<title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-148.5828C930.8101,-151.1199 953.618,-153.7776 975.5909,-156.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-157.1656 975.3757,-159.4842 979.2168,-156.7605 975.7403,-156.3553 975.7403,-156.3553 975.7403,-156.3553 979.2168,-156.7605 976.1049,-153.2265 982.6932,-157.1656 982.6932,-157.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\">\n",
|
|
"<title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1100.3013\" cy=\"-98.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8013\" y=\"-102.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=1, x1=1, x2=2, a1=1, a2=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3013\" y=\"-87.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\">\n",
|
|
"<title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-121.1573C930.8101,-118.6202 953.618,-115.9625 975.5909,-113.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-112.5745 976.1049,-116.5136 979.2168,-112.9796 975.7403,-113.3848 975.7403,-113.3848 975.7403,-113.3848 979.2168,-112.9796 975.3757,-110.2559 982.6932,-112.5745 982.6932,-112.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\">\n",
|
|
"<title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-76.5828C930.8101,-79.1199 953.618,-81.7776 975.5909,-84.338\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-85.1656 975.3757,-87.4842 979.2168,-84.7605 975.7403,-84.3553 975.7403,-84.3553 975.7403,-84.3553 979.2168,-84.7605 976.1049,-81.2265 982.6932,-85.1656 982.6932,-85.1656\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node11\" class=\"node\">\n",
|
|
"<title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"1100.3013\" cy=\"-26.8701\" rx=\"136.4432\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8013\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">c=2, x1=0, x2=2, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3013\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\">\n",
|
|
"<title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" d=\"M909.0375,-49.1573C930.8101,-46.6202 953.618,-43.9625 975.5909,-41.4021\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"982.6932,-40.5745 976.1049,-44.5136 979.2168,-40.9796 975.7403,-41.3848 975.7403,-41.3848 975.7403,-41.3848 979.2168,-40.9796 975.3757,-38.2559 982.6932,-40.5745 982.6932,-40.5745\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u6 -->\n",
|
|
"<g id=\"node12\" class=\"node\">\n",
|
|
"<title>u6</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1298.7729,-254.3701 1272.7729,-254.3701 1272.7729,-231.3701 1298.7729,-231.3701 1298.7729,-254.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.7729\" y=\"-239.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->u6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\">\n",
|
|
"<title>6->u6</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1237.0424,-242.8701C1247.7929,-242.8701 1257.5163,-242.8701 1265.3992,-242.8701\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1272.6385,-242.8701 1265.6385,-246.0202 1269.1385,-242.8701 1265.6385,-242.8702 1265.6385,-242.8702 1265.6385,-242.8702 1269.1385,-242.8701 1265.6384,-239.7202 1272.6385,-242.8701 1272.6385,-242.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u7 -->\n",
|
|
"<g id=\"node13\" class=\"node\">\n",
|
|
"<title>u7</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1298.7729,-182.3701 1272.7729,-182.3701 1272.7729,-159.3701 1298.7729,-159.3701 1298.7729,-182.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.7729\" y=\"-167.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->u7 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\">\n",
|
|
"<title>7->u7</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1237.0424,-170.8701C1247.7929,-170.8701 1257.5163,-170.8701 1265.3992,-170.8701\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1272.6385,-170.8701 1265.6385,-174.0202 1269.1385,-170.8701 1265.6385,-170.8702 1265.6385,-170.8702 1265.6385,-170.8702 1269.1385,-170.8701 1265.6384,-167.7202 1272.6385,-170.8701 1272.6385,-170.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u8 -->\n",
|
|
"<g id=\"node14\" class=\"node\">\n",
|
|
"<title>u8</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1298.7729,-110.3701 1272.7729,-110.3701 1272.7729,-87.3701 1298.7729,-87.3701 1298.7729,-110.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.7729\" y=\"-95.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->u8 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\">\n",
|
|
"<title>8->u8</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1237.0424,-98.8701C1247.7929,-98.8701 1257.5163,-98.8701 1265.3992,-98.8701\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1272.6385,-98.8701 1265.6385,-102.0202 1269.1385,-98.8701 1265.6385,-98.8702 1265.6385,-98.8702 1265.6385,-98.8702 1269.1385,-98.8701 1265.6384,-95.7202 1272.6385,-98.8701 1272.6385,-98.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u9 -->\n",
|
|
"<g id=\"node15\" class=\"node\">\n",
|
|
"<title>u9</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"transparent\" points=\"1298.7729,-38.3701 1272.7729,-38.3701 1272.7729,-15.3701 1298.7729,-15.3701 1298.7729,-38.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.7729\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->u9 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\">\n",
|
|
"<title>9->u9</title>\n",
|
|
"<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"5,2\" d=\"M1237.0424,-26.8701C1247.7929,-26.8701 1257.5163,-26.8701 1265.3992,-26.8701\"/>\n",
|
|
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"1272.6385,-26.8701 1265.6385,-30.0202 1269.1385,-26.8701 1265.6385,-26.8702 1265.6385,-26.8702 1265.6385,-26.8702 1269.1385,-26.8701 1265.6384,-23.7202 1272.6385,-26.8701 1272.6385,-26.8701\"/>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>\n"
|
|
],
|
|
"text/plain": [
|
|
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f4dc45626f0> >"
|
|
]
|
|
},
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"adding.kripke(['a1.Q', 'c==17'])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"def model_check(model, f):\n",
|
|
" nf = spot.formula.Not(f)\n",
|
|
" ss = model.kripke(spot.atomic_prop_collect(nf))\n",
|
|
" return not ss.intersects(nf.translate())"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 6,
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"data": {
|
|
"text/plain": [
|
|
"True"
|
|
]
|
|
},
|
|
"execution_count": 6,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"model_check(adding, 'F(\"c==2\")')"
|
|
]
|
|
}
|
|
],
|
|
"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.6.5"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 2
|
|
}
|