58e64e752c
Fixes #311. * tests/python/ipnbdoctest.py: Adjust to process the new format, with a lot of inspiration from Vcsn's copy of this file. * tests/python/_altscc.ipynb, tests/python/_aux.ipynb, tests/python/acc_cond.ipynb, tests/python/accparse.ipynb, tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb, tests/python/automata.ipynb, tests/python/decompose.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/parity.ipynb, tests/python/piperead.ipynb, tests/python/product.ipynb, tests/python/randaut.ipynb, tests/python/randltl.ipynb, tests/python/stutter-inv.ipynb, tests/python/testingaut.ipynb, tests/python/word.ipynb: Upgrade to the new format. * NEWS: Mention the change.
341 lines
19 KiB
Text
341 lines
19 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*\"."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"metadata": {
|
|
"collapsed": true
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
"import spot\n",
|
|
"import spot.ltsmin\n",
|
|
"spot.setup(show_default='.abr', 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": {
|
|
"collapsed": true
|
|
},
|
|
"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": {
|
|
"collapsed": false
|
|
},
|
|
"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": {
|
|
"collapsed": false
|
|
},
|
|
"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.38.0 (20140413.2041)\n",
|
|
" -->\n",
|
|
"<!-- Title: G Pages: 1 -->\n",
|
|
"<svg width=\"734pt\" height=\"177pt\"\n",
|
|
" viewBox=\"0.00 0.00 734.00 177.35\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.561689 0.561689) rotate(0) translate(4 311.74)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-311.74 1302.77,-311.74 1302.77,4 -4,4\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"646.386\" y=\"-292.54\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
|
"<text text-anchor=\"start\" x=\"638.386\" y=\"-277.54\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173.472\" cy=\"-134.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"84.9716\" y=\"-138.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=0, x2=0, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"96.4716\" y=\"-123.67\" font-family=\"Lato\" font-size=\"14.00\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g id=\"edge1\" class=\"edge\"><title>I->0</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M1.12428,-134.87C2.41096,-134.87 13.5817,-134.87 29.659,-134.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"36.8351,-134.87 29.8352,-138.02 33.3351,-134.87 29.8351,-134.87 29.8351,-134.87 29.8351,-134.87 33.3351,-134.87 29.8351,-131.72 36.8351,-134.87 36.8351,-134.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"482.415\" cy=\"-170.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"393.915\" y=\"-174.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=0, a1=1, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"403.415\" y=\"-159.67\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M291.389,-148.583C313.097,-151.129 335.841,-153.796 357.743,-156.365\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"364.822,-157.195 357.503,-159.508 361.346,-156.788 357.87,-156.38 357.87,-156.38 357.87,-156.38 361.346,-156.788 358.237,-153.251 364.822,-157.195 364.822,-157.195\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"482.415\" cy=\"-98.8701\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"393.915\" y=\"-102.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=0, x2=1, a1=0, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"405.415\" y=\"-87.6701\" font-family=\"Lato\" font-size=\"14.00\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g id=\"edge3\" class=\"edge\"><title>0->2</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M291.389,-121.157C313.097,-118.611 335.841,-115.944 357.743,-113.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"364.822,-112.545 358.237,-116.489 361.346,-112.952 357.87,-113.36 357.87,-113.36 357.87,-113.36 361.346,-112.952 357.503,-110.232 364.822,-112.545 364.822,-112.545\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"791.358\" cy=\"-206.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-210.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=2, x2=0, a1=2, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"712.358\" y=\"-195.67\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g id=\"edge4\" class=\"edge\"><title>1->3</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M600.333,-184.583C622.041,-187.129 644.785,-189.796 666.686,-192.365\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"673.765,-193.195 666.446,-195.508 670.289,-192.788 666.813,-192.38 666.813,-192.38 666.813,-192.38 670.289,-192.788 667.18,-189.251 673.765,-193.195 673.765,-193.195\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g id=\"node6\" class=\"node\"><title>4</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"791.358\" cy=\"-134.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-138.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=1, a1=1, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"712.358\" y=\"-123.67\" font-family=\"Lato\" font-size=\"14.00\">!a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->4 -->\n",
|
|
"<g id=\"edge5\" class=\"edge\"><title>1->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M600.333,-157.157C622.041,-154.611 644.785,-151.944 666.686,-149.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"673.765,-148.545 667.18,-152.489 670.289,-148.952 666.813,-149.36 666.813,-149.36 666.813,-149.36 670.289,-148.952 666.446,-146.232 673.765,-148.545 673.765,-148.545\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g id=\"edge6\" class=\"edge\"><title>2->4</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M600.333,-112.583C622.041,-115.129 644.785,-117.796 666.686,-120.365\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"673.765,-121.195 666.446,-123.508 670.289,-120.788 666.813,-120.38 666.813,-120.38 666.813,-120.38 670.289,-120.788 667.18,-117.251 673.765,-121.195 673.765,-121.195\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g id=\"node7\" class=\"node\"><title>5</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"791.358\" cy=\"-62.8701\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"702.858\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">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\">a1.Q & !"c==17" & !dead</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->5 -->\n",
|
|
"<g id=\"edge7\" class=\"edge\"><title>2->5</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M600.333,-85.1573C622.041,-82.6113 644.785,-79.9437 666.686,-77.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"673.765,-76.5447 667.18,-80.4887 670.289,-76.9524 666.813,-77.3602 666.813,-77.3602 666.813,-77.3602 670.289,-76.9524 666.446,-74.2316 673.765,-76.5447 673.765,-76.5447\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g id=\"node8\" class=\"node\"><title>6</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1100.3\" cy=\"-242.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8\" y=\"-246.67\" font-family=\"Lato\" font-size=\"14.00\">c=2, x1=2, x2=0, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3\" y=\"-231.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->6 -->\n",
|
|
"<g id=\"edge8\" class=\"edge\"><title>3->6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-220.583C930.984,-223.129 953.728,-225.796 975.63,-228.365\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-229.195 975.389,-231.508 979.232,-228.788 975.756,-228.38 975.756,-228.38 975.756,-228.38 979.232,-228.788 976.123,-225.251 982.709,-229.195 982.709,-229.195\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 7 -->\n",
|
|
"<g id=\"node9\" class=\"node\"><title>7</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1100.3\" cy=\"-170.87\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8\" y=\"-174.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=2, x2=1, a1=2, a2=1</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3\" y=\"-159.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->7 -->\n",
|
|
"<g id=\"edge9\" class=\"edge\"><title>3->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-193.157C930.984,-190.611 953.728,-187.944 975.63,-185.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-184.545 976.123,-188.489 979.232,-184.952 975.756,-185.36 975.756,-185.36 975.756,-185.36 979.232,-184.952 975.389,-182.232 982.709,-184.545 982.709,-184.545\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 4->7 -->\n",
|
|
"<g id=\"edge10\" class=\"edge\"><title>4->7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-148.583C930.984,-151.129 953.728,-153.796 975.63,-156.365\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-157.195 975.389,-159.508 979.232,-156.788 975.756,-156.38 975.756,-156.38 975.756,-156.38 979.232,-156.788 976.123,-153.251 982.709,-157.195 982.709,-157.195\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 8 -->\n",
|
|
"<g id=\"node10\" class=\"node\"><title>8</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1100.3\" cy=\"-98.8701\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8\" y=\"-102.67\" font-family=\"Lato\" font-size=\"14.00\">c=1, x1=1, x2=2, a1=1, a2=2</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3\" y=\"-87.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->8 -->\n",
|
|
"<g id=\"edge11\" class=\"edge\"><title>4->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-121.157C930.984,-118.611 953.728,-115.944 975.63,-113.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-112.545 976.123,-116.489 979.232,-112.952 975.756,-113.36 975.756,-113.36 975.756,-113.36 979.232,-112.952 975.389,-110.232 982.709,-112.545 982.709,-112.545\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 5->8 -->\n",
|
|
"<g id=\"edge12\" class=\"edge\"><title>5->8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-76.5828C930.984,-79.1288 953.728,-81.7964 975.63,-84.3652\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-85.1954 975.389,-87.5085 979.232,-84.7877 975.756,-84.3799 975.756,-84.3799 975.756,-84.3799 979.232,-84.7877 976.123,-81.2514 982.709,-85.1954 982.709,-85.1954\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 9 -->\n",
|
|
"<g id=\"node11\" class=\"node\"><title>9</title>\n",
|
|
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1100.3\" cy=\"-26.8701\" rx=\"136.443\" ry=\"26.7407\"/>\n",
|
|
"<text text-anchor=\"start\" x=\"1011.8\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">c=2, x1=0, x2=2, a1=0, a2=0</text>\n",
|
|
"<text text-anchor=\"start\" x=\"1095.3\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->9 -->\n",
|
|
"<g id=\"edge13\" class=\"edge\"><title>5->9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" d=\"M909.276,-49.1573C930.984,-46.6113 953.728,-43.9437 975.63,-41.375\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"982.709,-40.5447 976.123,-44.4887 979.232,-40.9524 975.756,-41.3602 975.756,-41.3602 975.756,-41.3602 979.232,-40.9524 975.389,-38.2316 982.709,-40.5447 982.709,-40.5447\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u6 -->\n",
|
|
"<g id=\"node12\" class=\"node\"><title>u6</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1298.77,-254.37 1272.77,-254.37 1272.77,-231.37 1298.77,-231.37 1298.77,-254.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.77\" y=\"-239.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->u6 -->\n",
|
|
"<g id=\"edge14\" class=\"edge\"><title>6->u6</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1237.05,-242.87C1247.91,-242.87 1257.69,-242.87 1265.53,-242.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1272.69,-242.87 1265.69,-246.02 1269.19,-242.87 1265.69,-242.87 1265.69,-242.87 1265.69,-242.87 1269.19,-242.87 1265.69,-239.72 1272.69,-242.87 1272.69,-242.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u7 -->\n",
|
|
"<g id=\"node13\" class=\"node\"><title>u7</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1298.77,-182.37 1272.77,-182.37 1272.77,-159.37 1298.77,-159.37 1298.77,-182.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.77\" y=\"-167.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 7->u7 -->\n",
|
|
"<g id=\"edge15\" class=\"edge\"><title>7->u7</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1237.05,-170.87C1247.91,-170.87 1257.69,-170.87 1265.53,-170.87\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1272.69,-170.87 1265.69,-174.02 1269.19,-170.87 1265.69,-170.87 1265.69,-170.87 1265.69,-170.87 1269.19,-170.87 1265.69,-167.72 1272.69,-170.87 1272.69,-170.87\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u8 -->\n",
|
|
"<g id=\"node14\" class=\"node\"><title>u8</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1298.77,-110.37 1272.77,-110.37 1272.77,-87.3701 1298.77,-87.3701 1298.77,-110.37\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.77\" y=\"-95.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 8->u8 -->\n",
|
|
"<g id=\"edge16\" class=\"edge\"><title>8->u8</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1237.05,-98.8701C1247.91,-98.8701 1257.69,-98.8701 1265.53,-98.8701\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1272.69,-98.8701 1265.69,-102.02 1269.19,-98.8701 1265.69,-98.8702 1265.69,-98.8702 1265.69,-98.8702 1269.19,-98.8701 1265.69,-95.7202 1272.69,-98.8701 1272.69,-98.8701\"/>\n",
|
|
"</g>\n",
|
|
"<!-- u9 -->\n",
|
|
"<g id=\"node15\" class=\"node\"><title>u9</title>\n",
|
|
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1298.77,-38.3701 1272.77,-38.3701 1272.77,-15.3701 1298.77,-15.3701 1298.77,-38.3701\"/>\n",
|
|
"<text text-anchor=\"middle\" x=\"1285.77\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
|
|
"</g>\n",
|
|
"<!-- 9->u9 -->\n",
|
|
"<g id=\"edge17\" class=\"edge\"><title>9->u9</title>\n",
|
|
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1237.05,-26.8701C1247.91,-26.8701 1257.69,-26.8701 1265.53,-26.8701\"/>\n",
|
|
"<polygon fill=\"black\" stroke=\"black\" points=\"1272.69,-26.8701 1265.69,-30.0202 1269.19,-26.8701 1265.69,-26.8702 1265.69,-26.8702 1265.69,-26.8702 1269.19,-26.8701 1265.69,-23.7202 1272.69,-26.8701 1272.69,-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 0x7fb770097600> >"
|
|
]
|
|
},
|
|
"execution_count": 4,
|
|
"metadata": {},
|
|
"output_type": "execute_result"
|
|
}
|
|
],
|
|
"source": [
|
|
"adding.kripke(['a1.Q', 'c==17'])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"metadata": {
|
|
"collapsed": true
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
"def model_check(model, f):\n",
|
|
" f = spot.formula(f)\n",
|
|
" ss = model.kripke(spot.atomic_prop_collect(f))\n",
|
|
" nf = spot.formula_Not(f).translate()\n",
|
|
" return spot.otf_product(ss, nf).is_empty()"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 6,
|
|
"metadata": {
|
|
"collapsed": false
|
|
},
|
|
"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.5.4"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 2
|
|
}
|