alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python/atva16-fig2b.ipynb
Alexandre Duret-Lutz a7051b32c8 dot: fix #393 
* spot/twaalgos/dot.cc: Add support for option 'E', and default to
rectangle nodes for large labels.
* bin/common_aoutput.cc, NEWS: Document it.
* tests/core/alternating.test, tests/core/dstar.test,
tests/core/readsave.test, tests/core/sccdot.test,
tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/parity.ipynb, tests/python/pdegen.py,
tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
test cases.
2020-04-29 21:14:36 +02:00

380 lines
21 KiB
Text
Raw Blame History

{
"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.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"159pt\"\n",
" viewBox=\"0.00 0.00 734.00 159.14\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.7462686567164178 0.7462686567164178) rotate(0) translate(4 210)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-210 983,-210 983,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M218,-122C218,-122 49,-122 49,-122 43,-122 37,-116 37,-110 37,-110 37,-96 37,-96 37,-90 43,-84 49,-84 49,-84 218,-84 218,-84 224,-84 230,-90 230,-96 230,-96 230,-110 230,-110 230,-116 224,-122 218,-122\"/>\n",
"<text text-anchor=\"start\" x=\"45\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=0, x2=0, a1=0, a2=0</text>\n",
"<text text-anchor=\"start\" x=\"58\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.1,-103C2.25,-103 13.83,-103 29.67,-103\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"36.71,-103 29.71,-106.15 33.21,-103 29.71,-103 29.71,-103 29.71,-103 33.21,-103 29.7,-99.85 36.71,-103 36.71,-103\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M447,-150C447,-150 278,-150 278,-150 272,-150 266,-144 266,-138 266,-138 266,-124 266,-124 266,-118 272,-112 278,-112 278,-112 447,-112 447,-112 453,-112 459,-118 459,-124 459,-124 459,-138 459,-138 459,-144 453,-150 447,-150\"/>\n",
"<text text-anchor=\"start\" x=\"274\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=0, a1=1, a2=0</text>\n",
"<text text-anchor=\"start\" x=\"285\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M230.11,-114.79C239.67,-115.97 249.39,-117.17 259.02,-118.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"266,-119.22 258.67,-121.49 262.53,-118.79 259.05,-118.36 259.05,-118.36 259.05,-118.36 262.53,-118.79 259.44,-115.24 266,-119.22 266,-119.22\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M447,-94C447,-94 278,-94 278,-94 272,-94 266,-88 266,-82 266,-82 266,-68 266,-68 266,-62 272,-56 278,-56 278,-56 447,-56 447,-56 453,-56 459,-62 459,-68 459,-68 459,-82 459,-82 459,-88 453,-94 447,-94\"/>\n",
"<text text-anchor=\"start\" x=\"274\" y=\"-78.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=0, x2=1, a1=0, a2=1</text>\n",
"<text text-anchor=\"start\" x=\"287\" y=\"-63.8\" font-family=\"Lato\" font-size=\"14.00\">a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M230.11,-91.21C239.67,-90.03 249.39,-88.83 259.02,-87.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"266,-86.78 259.44,-90.76 262.53,-87.21 259.05,-87.64 259.05,-87.64 259.05,-87.64 262.53,-87.21 258.67,-84.51 266,-86.78 266,-86.78\"/>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M676,-178C676,-178 507,-178 507,-178 501,-178 495,-172 495,-166 495,-166 495,-152 495,-152 495,-146 501,-140 507,-140 507,-140 676,-140 676,-140 682,-140 688,-146 688,-152 688,-152 688,-166 688,-166 688,-172 682,-178 676,-178\"/>\n",
"<text text-anchor=\"start\" x=\"503\" y=\"-162.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=2, x2=0, a1=2, a2=0</text>\n",
"<text text-anchor=\"start\" x=\"514\" y=\"-147.8\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M459.11,-142.79C468.67,-143.97 478.39,-145.17 488.02,-146.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"495,-147.22 487.67,-149.49 491.53,-146.79 488.05,-146.36 488.05,-146.36 488.05,-146.36 491.53,-146.79 488.44,-143.24 495,-147.22 495,-147.22\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>4</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M676,-122C676,-122 507,-122 507,-122 501,-122 495,-116 495,-110 495,-110 495,-96 495,-96 495,-90 501,-84 507,-84 507,-84 676,-84 676,-84 682,-84 688,-90 688,-96 688,-96 688,-110 688,-110 688,-116 682,-122 676,-122\"/>\n",
"<text text-anchor=\"start\" x=\"503\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=1, a1=1, a2=1</text>\n",
"<text text-anchor=\"start\" x=\"514\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M459.11,-119.21C468.67,-118.03 478.39,-116.83 488.02,-115.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"495,-114.78 488.44,-118.76 491.53,-115.21 488.05,-115.64 488.05,-115.64 488.05,-115.64 491.53,-115.21 487.67,-112.51 495,-114.78 495,-114.78\"/>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M459.11,-86.79C468.67,-87.97 478.39,-89.17 488.02,-90.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"495,-91.22 487.67,-93.49 491.53,-90.79 488.05,-90.36 488.05,-90.36 488.05,-90.36 491.53,-90.79 488.44,-87.24 495,-91.22 495,-91.22\"/>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>5</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M676,-66C676,-66 507,-66 507,-66 501,-66 495,-60 495,-54 495,-54 495,-40 495,-40 495,-34 501,-28 507,-28 507,-28 676,-28 676,-28 682,-28 688,-34 688,-40 688,-40 688,-54 688,-54 688,-60 682,-66 676,-66\"/>\n",
"<text text-anchor=\"start\" x=\"503\" y=\"-50.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=0, x2=2, a1=0, a2=2</text>\n",
"<text text-anchor=\"start\" x=\"516\" y=\"-35.8\" font-family=\"Lato\" font-size=\"14.00\">a1.Q &amp; !&quot;c==17&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M459.11,-63.21C468.67,-62.03 478.39,-60.83 488.02,-59.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"495,-58.78 488.44,-62.76 491.53,-59.21 488.05,-59.64 488.05,-59.64 488.05,-59.64 491.53,-59.21 487.67,-56.51 495,-58.78 495,-58.78\"/>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>6</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M905,-206C905,-206 736,-206 736,-206 730,-206 724,-200 724,-194 724,-194 724,-180 724,-180 724,-174 730,-168 736,-168 736,-168 905,-168 905,-168 911,-168 917,-174 917,-180 917,-180 917,-194 917,-194 917,-200 911,-206 905,-206\"/>\n",
"<text text-anchor=\"start\" x=\"732\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\">c=2, x1=2, x2=0, a1=0, a2=0</text>\n",
"<text text-anchor=\"start\" x=\"815.5\" y=\"-175.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;6 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>3&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-170.79C697.67,-171.97 707.39,-173.17 717.02,-174.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-175.22 716.67,-177.49 720.53,-174.79 717.05,-174.36 717.05,-174.36 717.05,-174.36 720.53,-174.79 717.44,-171.24 724,-175.22 724,-175.22\"/>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>7</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M905,-150C905,-150 736,-150 736,-150 730,-150 724,-144 724,-138 724,-138 724,-124 724,-124 724,-118 730,-112 736,-112 736,-112 905,-112 905,-112 911,-112 917,-118 917,-124 917,-124 917,-138 917,-138 917,-144 911,-150 905,-150\"/>\n",
"<text text-anchor=\"start\" x=\"732\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=2, x2=1, a1=2, a2=1</text>\n",
"<text text-anchor=\"start\" x=\"815.5\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;7 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-147.21C697.67,-146.03 707.39,-144.83 717.02,-143.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-142.78 717.44,-146.76 720.53,-143.21 717.05,-143.64 717.05,-143.64 717.05,-143.64 720.53,-143.21 716.67,-140.51 724,-142.78 724,-142.78\"/>\n",
"</g>\n",
"<!-- 4&#45;&gt;7 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>4&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-114.79C697.67,-115.97 707.39,-117.17 717.02,-118.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-119.22 716.67,-121.49 720.53,-118.79 717.05,-118.36 717.05,-118.36 717.05,-118.36 720.53,-118.79 717.44,-115.24 724,-119.22 724,-119.22\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>8</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M905,-94C905,-94 736,-94 736,-94 730,-94 724,-88 724,-82 724,-82 724,-68 724,-68 724,-62 730,-56 736,-56 736,-56 905,-56 905,-56 911,-56 917,-62 917,-68 917,-68 917,-82 917,-82 917,-88 911,-94 905,-94\"/>\n",
"<text text-anchor=\"start\" x=\"732\" y=\"-78.8\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=2, a1=1, a2=2</text>\n",
"<text text-anchor=\"start\" x=\"815.5\" y=\"-63.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;8 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>4&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-91.21C697.67,-90.03 707.39,-88.83 717.02,-87.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-86.78 717.44,-90.76 720.53,-87.21 717.05,-87.64 717.05,-87.64 717.05,-87.64 720.53,-87.21 716.67,-84.51 724,-86.78 724,-86.78\"/>\n",
"</g>\n",
"<!-- 5&#45;&gt;8 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>5&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-58.79C697.67,-59.97 707.39,-61.17 717.02,-62.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-63.22 716.67,-65.49 720.53,-62.79 717.05,-62.36 717.05,-62.36 717.05,-62.36 720.53,-62.79 717.44,-59.24 724,-63.22 724,-63.22\"/>\n",
"</g>\n",
"<!-- 9 -->\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>9</title>\n",
"<path fill=\"#ffffaa\" stroke=\"black\" d=\"M905,-38C905,-38 736,-38 736,-38 730,-38 724,-32 724,-26 724,-26 724,-12 724,-12 724,-6 730,0 736,0 736,0 905,0 905,0 911,0 917,-6 917,-12 917,-12 917,-26 917,-26 917,-32 911,-38 905,-38\"/>\n",
"<text text-anchor=\"start\" x=\"732\" y=\"-22.8\" font-family=\"Lato\" font-size=\"14.00\">c=2, x1=0, x2=2, a1=0, a2=0</text>\n",
"<text text-anchor=\"start\" x=\"815.5\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;9 -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>5&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M688.11,-35.21C697.67,-34.03 707.39,-32.83 717.02,-31.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"724,-30.78 717.44,-34.76 720.53,-31.21 717.05,-31.64 717.05,-31.64 717.05,-31.64 720.53,-31.21 716.67,-28.51 724,-30.78 724,-30.78\"/>\n",
"</g>\n",
"<!-- u6 -->\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>u6</title>\n",
"<g id=\"a_node12\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M971.33,-198.5C971.33,-198.5 960.67,-198.5 960.67,-198.5 956.83,-198.5 953,-194.67 953,-190.83 953,-190.83 953,-183.17 953,-183.17 953,-179.33 956.83,-175.5 960.67,-175.5 960.67,-175.5 971.33,-175.5 971.33,-175.5 975.17,-175.5 979,-179.33 979,-183.17 979,-183.17 979,-190.83 979,-190.83 979,-194.67 975.17,-198.5 971.33,-198.5\"/>\n",
"<text text-anchor=\"middle\" x=\"966\" y=\"-183.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- 6&#45;&gt;u6 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>6&#45;&gt;u6</title>\n",
"<g id=\"a_edge14\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M917.22,-187C927.86,-187 937.71,-187 945.66,-187\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"952.95,-187 945.95,-190.15 949.45,-187 945.95,-187 945.95,-187 945.95,-187 949.45,-187 945.95,-183.85 952.95,-187 952.95,-187\"/>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- u7 -->\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>u7</title>\n",
"<g id=\"a_node13\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M971.33,-142.5C971.33,-142.5 960.67,-142.5 960.67,-142.5 956.83,-142.5 953,-138.67 953,-134.83 953,-134.83 953,-127.17 953,-127.17 953,-123.33 956.83,-119.5 960.67,-119.5 960.67,-119.5 971.33,-119.5 971.33,-119.5 975.17,-119.5 979,-123.33 979,-127.17 979,-127.17 979,-134.83 979,-134.83 979,-138.67 975.17,-142.5 971.33,-142.5\"/>\n",
"<text text-anchor=\"middle\" x=\"966\" y=\"-127.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- 7&#45;&gt;u7 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>7&#45;&gt;u7</title>\n",
"<g id=\"a_edge15\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M917.22,-131C927.86,-131 937.71,-131 945.66,-131\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"952.95,-131 945.95,-134.15 949.45,-131 945.95,-131 945.95,-131 945.95,-131 949.45,-131 945.95,-127.85 952.95,-131 952.95,-131\"/>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- u8 -->\n",
"<g id=\"node14\" class=\"node\">\n",
"<title>u8</title>\n",
"<g id=\"a_node14\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M971.33,-86.5C971.33,-86.5 960.67,-86.5 960.67,-86.5 956.83,-86.5 953,-82.67 953,-78.83 953,-78.83 953,-71.17 953,-71.17 953,-67.33 956.83,-63.5 960.67,-63.5 960.67,-63.5 971.33,-63.5 971.33,-63.5 975.17,-63.5 979,-67.33 979,-71.17 979,-71.17 979,-78.83 979,-78.83 979,-82.67 975.17,-86.5 971.33,-86.5\"/>\n",
"<text text-anchor=\"middle\" x=\"966\" y=\"-71.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- 8&#45;&gt;u8 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>8&#45;&gt;u8</title>\n",
"<g id=\"a_edge16\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M917.22,-75C927.86,-75 937.71,-75 945.66,-75\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"952.95,-75 945.95,-78.15 949.45,-75 945.95,-75 945.95,-75 945.95,-75 949.45,-75 945.95,-71.85 952.95,-75 952.95,-75\"/>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- u9 -->\n",
"<g id=\"node15\" class=\"node\">\n",
"<title>u9</title>\n",
"<g id=\"a_node15\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"#ffffaa\" stroke=\"transparent\" d=\"M971.33,-30.5C971.33,-30.5 960.67,-30.5 960.67,-30.5 956.83,-30.5 953,-26.67 953,-22.83 953,-22.83 953,-15.17 953,-15.17 953,-11.33 956.83,-7.5 960.67,-7.5 960.67,-7.5 971.33,-7.5 971.33,-7.5 975.17,-7.5 979,-11.33 979,-15.17 979,-15.17 979,-22.83 979,-22.83 979,-26.67 975.17,-30.5 971.33,-30.5\"/>\n",
"<text text-anchor=\"middle\" x=\"966\" y=\"-15.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"<!-- 9&#45;&gt;u9 -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>9&#45;&gt;u9</title>\n",
"<g id=\"a_edge17\"><a xlink:title=\"hidden successors\">\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M917.22,-19C927.86,-19 937.71,-19 945.66,-19\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"952.95,-19 945.95,-22.15 949.45,-19 945.95,-19 945.95,-19 945.95,-19 949.45,-19 945.95,-15.85 952.95,-19 952.95,-19\"/>\n",
"</a>\n",
"</g>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f9a40554b10> >"
]
},
"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.8.2"
}
},
"nbformat": 4,
"nbformat_minor": 2
}
Reference in a new issue View git blame Copy permalink