Skip to content
GitLab
Commit b2a306c8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: add the examples from the ATVA'16 paper 

* tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb: New
files.
* tests/Makefile.am, doc/org/tut.org: Add them.
parent 125ca7df
Hide whitespace changes
Inline Side-by-side
doc/org/tut.org
View file @ b2a306c8
......@@ -67,3 +67,5 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/word.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes.
- [[https://spot.lrde.epita.fr/ipynb/highlighting.html][=highlighting.ipynb=]] shows how to highlight states or edges in
automata.
- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
tests/Makefile.am
View file @ b2a306c8
......@@ -290,6 +290,8 @@ if USE_PYTHON
TESTS_ipython = \
python/acc_cond.ipynb \
python/accparse.ipynb \
python/atva16-fig2a.ipynb \
python/atva16-fig2b.ipynb \
python/automata-io.ipynb \
python/automata.ipynb \
python/decompose.ipynb \
......
tests/python/atva16-fig2a.ipynb 0 → 100644
View file @ b2a306c8
{
"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.2rc1"
},
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"."
]
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"import spot\n",
"spot.setup(show_default='.abr')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('GFa <-> GFb'); f"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"text": [
"GFa <-> GFb"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"svg": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"288pt\" height=\"360pt\"\n",
" viewBox=\"0.00 0.00 288.47 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.947368 0.947368) rotate(0) translate(4 376)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-376 300.5,-376 300.5,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"100.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"124.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"137.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"177.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"<text text-anchor=\"start\" x=\"190.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-105C2.79388,-105 17.1543,-105 30.6317,-105\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-105 30.9419,-108.15 34.4419,-105 30.9419,-105 30.9419,-105 30.9419,-105 34.4419,-105 30.9418,-101.85 37.9419,-105 37.9419,-105\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144.5\" cy=\"-156\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"144.5\" y=\"-152.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M72.0672,-113.884C85.9591,-122.074 106.722,-134.316 122.288,-143.493\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"128.606,-147.218 120.976,-146.376 125.591,-145.441 122.576,-143.663 122.576,-143.663 122.576,-143.663 125.591,-145.441 124.175,-140.95 128.606,-147.218 128.606,-147.218\"/>\n",
"<text text-anchor=\"middle\" x=\"97\" y=\"-133.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"272\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.1508,-102.676C112.123,-97.5301 203.374,-85.1643 246.992,-79.2534\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"254.065,-78.295 247.551,-82.3565 250.596,-78.765 247.128,-79.2351 247.128,-79.2351 247.128,-79.2351 250.596,-78.765 246.705,-76.1136 254.065,-78.295 254.065,-78.295\"/>\n",
"<text text-anchor=\"start\" x=\"120\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"144.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M69.3933,-92.535C84.1669,-77.676 108.963,-52.7363 125.764,-35.8381\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"131.13,-30.4419 128.428,-37.6268 128.662,-32.9239 126.194,-35.4059 126.194,-35.4059 126.194,-35.4059 128.662,-32.9239 123.96,-33.1849 131.13,-30.4419 131.13,-30.4419\"/>\n",
"<text text-anchor=\"middle\" x=\"97\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M142.42,-174.153C142.099,-183.539 142.793,-192 144.5,-192 145.754,-192 146.461,-187.437 146.621,-181.295\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"146.58,-174.153 149.77,-181.135 146.6,-177.653 146.62,-181.153 146.62,-181.153 146.62,-181.153 146.6,-177.653 143.47,-181.171 146.58,-174.153 146.58,-174.153\"/>\n",
"<text text-anchor=\"start\" x=\"123\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"138\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M141.266,-173.906C139.109,-195 140.188,-222 144.5,-222 148.341,-222 149.616,-200.583 148.326,-180.997\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"147.734,-173.906 151.455,-180.62 148.025,-177.394 148.316,-180.882 148.316,-180.882 148.316,-180.882 148.025,-177.394 145.177,-181.144 147.734,-173.906 147.734,-173.906\"/>\n",
"<text text-anchor=\"start\" x=\"120\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M140.372,-173.871C136.217,-201.525 137.593,-240 144.5,-240 150.84,-240 152.52,-207.578 149.539,-180.868\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"148.628,-173.871 152.655,-180.406 149.08,-177.342 149.532,-180.812 149.532,-180.812 149.532,-180.812 149.08,-177.342 146.408,-181.219 148.628,-173.871 148.628,-173.871\"/>\n",
"<text text-anchor=\"start\" x=\"126\" y=\"-257.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"131.5\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"144.5\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M139.905,-173.612C133.288,-209.893 134.819,-268 144.5,-268 153.576,-268 155.489,-216.929 150.24,-180.651\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"149.095,-173.612 153.328,-180.015 149.657,-177.067 150.219,-180.521 150.219,-180.521 150.219,-180.521 149.657,-177.067 147.11,-181.027 149.095,-173.612 149.095,-173.612\"/>\n",
"<text text-anchor=\"start\" x=\"123\" y=\"-286.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"138\" y=\"-271.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M261.849,-91.1666C258.772,-101.664 262.156,-112 272,-112 279.537,-112 283.287,-105.941 283.25,-98.39\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"282.151,-91.1666 286.318,-97.6135 282.678,-94.6269 283.204,-98.0871 283.204,-98.0871 283.204,-98.0871 282.678,-94.6269 280.09,-98.5607 282.151,-91.1666 282.151,-91.1666\"/>\n",
"<text text-anchor=\"start\" x=\"247.5\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"259\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"272\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M161.141,-25.2285C183.217,-35.4311 223.626,-54.1061 248.802,-65.741\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"255.162,-68.6804 247.486,-68.6032 251.985,-67.2121 248.808,-65.7438 248.808,-65.7438 248.808,-65.7438 251.985,-67.2121 250.129,-62.8844 255.162,-68.6804 255.162,-68.6804\"/>\n",
"<text text-anchor=\"start\" x=\"187\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M136.484,-34.2903C134.551,-44.3892 137.223,-54 144.5,-54 149.958,-54 152.826,-48.5939 153.103,-41.6304\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"152.516,-34.2903 156.214,-41.0172 152.795,-37.7792 153.074,-41.268 153.074,-41.268 153.074,-41.268 152.795,-37.7792 149.934,-41.5189 152.516,-34.2903 152.516,-34.2903\"/>\n",
"<text text-anchor=\"middle\" x=\"144.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f87ba300> >"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"def implies(f, g):\n",
" f = spot.formula(f)\n",
" g = spot.formula_Not(spot.formula(g))\n",
" return spot.product(f.translate(), g.translate()).is_empty()\n",
"def equiv(f, g):\n",
" return implies(f, g) and implies(g, f)"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 4
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"equiv('a U (b U a)', 'b U a')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"text": [
"True"
]
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"equiv('!(a U b)', '!a U !b')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 6,
"text": [
"False"
]
}
],
"prompt_number": 6
}
],
"metadata": {}
}
]
}
tests/python/atva16-fig2b.ipynb 0 → 100644
View file @ b2a306c8
{
"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.2rc1"
},
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"."
]
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"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')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"%%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;"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"adding"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"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']"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"adding.kripke(['a1.Q', 'c==17'])"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"svg": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"144pt\"\n",
" viewBox=\"0.00 0.00 734.00 143.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.477539 0.477539) rotate(0) translate(4 296.74)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-296.74 1533.05,-296.74 1533.05,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"761.024\" y=\"-277.54\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"201.756\" cy=\"-134.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"201.756\" 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=\"middle\" x=\"201.756\" y=\"-123.67\" 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\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.14478,-134.87C2.50931,-134.87 13.4162,-134.87 29.4908,-134.87\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"36.6835,-134.87 29.6836,-138.02 33.1835,-134.87 29.6835,-134.87 29.6835,-134.87 29.6835,-134.87 33.1835,-134.87 29.6835,-131.72 36.6835,-134.87 36.6835,-134.87\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"567.268\" cy=\"-170.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"567.268\" 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=\"middle\" x=\"567.268\" y=\"-159.67\" 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\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M343.039,-148.763C367.889,-151.224 393.831,-153.793 418.871,-156.273\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"425.907,-156.97 418.631,-159.414 422.424,-156.625 418.941,-156.28 418.941,-156.28 418.941,-156.28 422.424,-156.625 419.252,-153.145 425.907,-156.97 425.907,-156.97\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"567.268\" cy=\"-98.8701\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"567.268\" 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=\"middle\" x=\"567.268\" y=\"-87.6701\" 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\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M343.039,-120.977C367.889,-118.516 393.831,-115.947 418.871,-113.467\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"425.907,-112.77 419.252,-116.595 422.424,-113.115 418.941,-113.46 418.941,-113.46 418.941,-113.46 422.424,-113.115 418.631,-110.326 425.907,-112.77 425.907,-112.77\"/>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"932.779\" cy=\"-206.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"932.779\" 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=\"middle\" x=\"932.779\" y=\"-195.67\" 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\"><title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M708.551,-184.763C733.401,-187.224 759.343,-189.793 784.382,-192.273\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"791.419,-192.97 784.143,-195.414 787.936,-192.625 784.453,-192.28 784.453,-192.28 784.453,-192.28 787.936,-192.625 784.764,-189.145 791.419,-192.97 791.419,-192.97\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\"><title>4</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"932.779\" cy=\"-134.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"932.779\" 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=\"middle\" x=\"932.779\" y=\"-123.67\" 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\"><title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M708.551,-156.977C733.401,-154.516 759.343,-151.947 784.382,-149.467\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"791.419,-148.77 784.764,-152.595 787.936,-149.115 784.453,-149.46 784.453,-149.46 784.453,-149.46 787.936,-149.115 784.143,-146.326 791.419,-148.77 791.419,-148.77\"/>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M708.551,-112.763C733.401,-115.224 759.343,-117.793 784.382,-120.273\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"791.419,-120.97 784.143,-123.414 787.936,-120.625 784.453,-120.28 784.453,-120.28 784.453,-120.28 787.936,-120.625 784.764,-117.145 791.419,-120.97 791.419,-120.97\"/>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\"><title>5</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"932.779\" cy=\"-62.8701\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"932.779\" 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=\"middle\" x=\"932.779\" y=\"-51.6701\" 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\"><title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M708.551,-84.9773C733.401,-82.5163 759.343,-79.9471 784.382,-77.4674\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"791.419,-76.7705 784.764,-80.5951 787.936,-77.1155 784.453,-77.4604 784.453,-77.4604 784.453,-77.4604 787.936,-77.1155 784.143,-74.3258 791.419,-76.7705 791.419,-76.7705\"/>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node8\" class=\"node\"><title>6</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1298.29\" cy=\"-242.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1298.29\" 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=\"middle\" x=\"1298.29\" y=\"-231.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;6 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-220.763C1098.91,-223.224 1124.85,-225.793 1149.89,-228.273\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-228.97 1149.65,-231.414 1153.45,-228.625 1149.96,-228.28 1149.96,-228.28 1149.96,-228.28 1153.45,-228.625 1150.28,-225.145 1156.93,-228.97 1156.93,-228.97\"/>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g id=\"node9\" class=\"node\"><title>7</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1298.29\" cy=\"-170.87\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1298.29\" 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=\"middle\" x=\"1298.29\" y=\"-159.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;7 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-192.977C1098.91,-190.516 1124.85,-187.947 1149.89,-185.467\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-184.77 1150.28,-188.595 1153.45,-185.115 1149.96,-185.46 1149.96,-185.46 1149.96,-185.46 1153.45,-185.115 1149.65,-182.326 1156.93,-184.77 1156.93,-184.77\"/>\n",
"</g>\n",
"<!-- 4&#45;&gt;7 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-148.763C1098.91,-151.224 1124.85,-153.793 1149.89,-156.273\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-156.97 1149.65,-159.414 1153.45,-156.625 1149.96,-156.28 1149.96,-156.28 1149.96,-156.28 1153.45,-156.625 1150.28,-153.145 1156.93,-156.97 1156.93,-156.97\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g id=\"node10\" class=\"node\"><title>8</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1298.29\" cy=\"-98.8701\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1298.29\" 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=\"middle\" x=\"1298.29\" y=\"-87.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;8 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-120.977C1098.91,-118.516 1124.85,-115.947 1149.89,-113.467\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-112.77 1150.28,-116.595 1153.45,-113.115 1149.96,-113.46 1149.96,-113.46 1149.96,-113.46 1153.45,-113.115 1149.65,-110.326 1156.93,-112.77 1156.93,-112.77\"/>\n",
"</g>\n",
"<!-- 5&#45;&gt;8 -->\n",
"<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-76.7628C1098.91,-79.2238 1124.85,-81.793 1149.89,-84.2727\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-84.9696 1149.65,-87.4143 1153.45,-84.6246 1149.96,-84.2797 1149.96,-84.2797 1149.96,-84.2797 1153.45,-84.6246 1150.28,-81.145 1156.93,-84.9696 1156.93,-84.9696\"/>\n",
"</g>\n",
"<!-- 9 -->\n",
"<g id=\"node11\" class=\"node\"><title>9</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1298.29\" cy=\"-26.8701\" rx=\"164.512\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1298.29\" 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=\"middle\" x=\"1298.29\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;9 -->\n",
"<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1074.06,-48.9773C1098.91,-46.5163 1124.85,-43.9471 1149.89,-41.4674\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1156.93,-40.7705 1150.28,-44.5951 1153.45,-41.1155 1149.96,-41.4604 1149.96,-41.4604 1149.96,-41.4604 1153.45,-41.1155 1149.65,-38.3258 1156.93,-40.7705 1156.93,-40.7705\"/>\n",
"</g>\n",
"<!-- u6 -->\n",
"<g id=\"node12\" class=\"node\"><title>u6</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1529.05,-254.37 1499.05,-254.37 1499.05,-231.37 1529.05,-231.37 1529.05,-254.37\"/>\n",
"<text text-anchor=\"middle\" x=\"1514.05\" y=\"-239.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;u6 -->\n",
"<g id=\"edge14\" class=\"edge\"><title>6&#45;&gt;u6</title>\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1463.2,-242.87C1474.02,-242.87 1483.73,-242.87 1491.65,-242.87\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.94,-242.87 1491.94,-246.02 1495.44,-242.87 1491.94,-242.87 1491.94,-242.87 1491.94,-242.87 1495.44,-242.87 1491.94,-239.72 1498.94,-242.87 1498.94,-242.87\"/>\n",
"</g>\n",
"<!-- u7 -->\n",
"<g id=\"node13\" class=\"node\"><title>u7</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1529.05,-182.37 1499.05,-182.37 1499.05,-159.37 1529.05,-159.37 1529.05,-182.37\"/>\n",
"<text text-anchor=\"middle\" x=\"1514.05\" y=\"-167.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 7&#45;&gt;u7 -->\n",
"<g id=\"edge15\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1463.2,-170.87C1474.02,-170.87 1483.73,-170.87 1491.65,-170.87\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.94,-170.87 1491.94,-174.02 1495.44,-170.87 1491.94,-170.87 1491.94,-170.87 1491.94,-170.87 1495.44,-170.87 1491.94,-167.72 1498.94,-170.87 1498.94,-170.87\"/>\n",
"</g>\n",
"<!-- u8 -->\n",
"<g id=\"node14\" class=\"node\"><title>u8</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1529.05,-110.37 1499.05,-110.37 1499.05,-87.3701 1529.05,-87.3701 1529.05,-110.37\"/>\n",
"<text text-anchor=\"middle\" x=\"1514.05\" y=\"-95.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;u8 -->\n",
"<g id=\"edge16\" class=\"edge\"><title>8&#45;&gt;u8</title>\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1463.2,-98.8701C1474.02,-98.8701 1483.73,-98.8701 1491.65,-98.8701\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.94,-98.8701 1491.94,-102.02 1495.44,-98.8701 1491.94,-98.8702 1491.94,-98.8702 1491.94,-98.8702 1495.44,-98.8701 1491.94,-95.7202 1498.94,-98.8701 1498.94,-98.8701\"/>\n",
"</g>\n",
"<!-- u9 -->\n",
"<g id=\"node15\" class=\"node\"><title>u9</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1529.05,-38.3701 1499.05,-38.3701 1499.05,-15.3701 1529.05,-15.3701 1529.05,-38.3701\"/>\n",
"<text text-anchor=\"middle\" x=\"1514.05\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
"</g>\n",
"<!-- 9&#45;&gt;u9 -->\n",
"<g id=\"edge17\" class=\"edge\"><title>9&#45;&gt;u9</title>\n",
"<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1463.2,-26.8701C1474.02,-26.8701 1483.73,-26.8701 1491.65,-26.8701\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1498.94,-26.8701 1491.94,-30.0202 1495.44,-26.8701 1491.94,-26.8702 1491.94,-26.8702 1491.94,-26.8702 1495.44,-26.8701 1491.94,-23.7202 1498.94,-26.8701 1498.94,-26.8701\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f3406f6f5d0> >"
]
}
],
"prompt_number": 4
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"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()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"model_check(adding, 'F(\"c==2\")')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 6,
"text": [
"True"
]
}
],
"prompt_number": 6
}
],
"metadata": {}
}
]
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment