alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python/atva16-fig2a.ipynb
Alexandre Duret-Lutz 6a808492c1 python: implicit str->formula conversion 
* 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.
2018-05-15 16:16:11 +02:00

246 lines
12 KiB
Text
Raw Blame History

{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This example is the left 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 the current version of Spot."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"spot.setup(show_default='.b')"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$"
],
"text/plain": [
"GFa <-> GFb"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f = spot.formula('GFa <-> GFb'); f"
]
},
{
"cell_type": "code",
"execution_count": 3,
"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=\"198pt\" height=\"355pt\"\n",
" viewBox=\"0.00 0.00 197.50 355.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 1) rotate(0) translate(4 351)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-351 193.5,-351 193.5,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"47.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"69.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"85.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"121.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"137.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"50.75\" y=\"-318.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[gen. Büchi 2]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-68\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-64.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</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=\"#000000\" d=\"M1.1233,-68C4.178,-68 17.9448,-68 30.9241,-68\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-68 30.9808,-71.1501 34.4807,-68 30.9807,-68.0001 30.9807,-68.0001 30.9807,-68.0001 34.4807,-68 30.9807,-64.8501 37.9807,-68 37.9807,-68\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-85.0373C48.3189,-94.8579 50.4453,-104 56,-104 60.166,-104 62.4036,-98.8576 62.7128,-92.1433\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-85.0373 65.8541,-91.8818 62.5434,-88.5335 62.7076,-92.0296 62.7076,-92.0296 62.7076,-92.0296 62.5434,-88.5335 59.561,-92.1774 62.3792,-85.0373 62.3792,-85.0373\"/>\n",
"<text text-anchor=\"start\" x=\"51.5\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"169\" cy=\"-118\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"164.5\" y=\"-114.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M72.6735,-75.3777C91.9517,-83.9078 123.8161,-98.0071 145.5767,-107.6357\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"152.2581,-110.5921 144.5821,-110.6402 149.0574,-109.1758 145.8567,-107.7595 145.8567,-107.7595 145.8567,-107.7595 149.0574,-109.1758 147.1313,-104.8789 152.2581,-110.5921 152.2581,-110.5921\"/>\n",
"<text text-anchor=\"start\" x=\"99\" y=\"-104.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a | b</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"169\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"169\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M72.6735,-60.6223C91.9517,-52.0922 123.8161,-37.9929 145.5767,-28.3643\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"152.2581,-25.4079 147.1313,-31.1211 149.0574,-26.8242 145.8567,-28.2405 145.8567,-28.2405 145.8567,-28.2405 149.0574,-26.8242 144.5821,-25.3598 152.2581,-25.4079 152.2581,-25.4079\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-54.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M166.4673,-136.1527C166.0776,-145.5391 166.9219,-154 169,-154 170.5261,-154 171.3868,-149.437 171.582,-143.2953\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"171.5327,-136.1527 174.7311,-143.1307 171.5569,-139.6526 171.5812,-143.1525 171.5812,-143.1525 171.5812,-143.1525 171.5569,-139.6526 168.4312,-143.1743 171.5327,-136.1527 171.5327,-136.1527\"/>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M164.8279,-135.6991C162.5234,-152.9958 163.9141,-172 169,-172 173.3707,-172 175.0124,-157.965 173.9251,-143.0399\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.1721,-135.6991 177.02,-142.3411 173.5293,-139.1808 173.8865,-142.6626 173.8865,-142.6626 173.8865,-142.6626 173.5293,-139.1808 170.7529,-142.984 173.1721,-135.6991 173.1721,-135.6991\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-175.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M164.0493,-135.4671C158.9005,-163.1487 160.5508,-202 169,-202 176.7561,-202 178.783,-169.2613 175.0805,-142.4773\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.9507,-135.4671 178.1745,-141.8767 174.5077,-138.9225 175.0646,-142.3779 175.0646,-142.3779 175.0646,-142.3779 174.5077,-138.9225 171.9547,-142.8792 173.9507,-135.4671 173.9507,-135.4671\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-220.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M163.5194,-135.2366C155.3333,-171.922 157.1602,-232 169,-232 180.0999,-232 182.3992,-179.1971 175.8981,-142.3689\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"174.4806,-135.2366 178.9348,-141.4882 175.1629,-138.6695 175.8452,-142.1023 175.8452,-142.1023 175.8452,-142.1023 175.1629,-138.6695 172.7556,-142.7164 174.4806,-135.2366 174.4806,-135.2366\"/>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M159.4254,-33.5414C156.7303,-43.9087 159.9219,-54 169,-54 175.9504,-54 179.4503,-48.0847 179.4995,-40.6591\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"178.5746,-33.5414 182.6004,-40.0771 179.0256,-37.0123 179.4767,-40.4831 179.4767,-40.4831 179.4767,-40.4831 179.0256,-37.0123 176.353,-40.889 178.5746,-33.5414 178.5746,-33.5414\"/>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f81a85ea1e0> >"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f.translate()"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"def implies(f, g):\n",
" f = spot.formula(f)\n",
" g = spot.formula.Not(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)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"equiv('a U (b U a)', 'b U a')"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"equiv('!(a U b)', '!a U !b')"
]
}
],
"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
}
Reference in a new issue View git blame Copy permalink