alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python/atva16-fig2a.ipynb
Alexandre Duret-Lutz ae0e84ac9e simulation: do not depend on bdd numbers for ordering classes 
Fixes #262 again.  Reported by Maximilien Colange.

* spot/twaalgos/simulation.cc: Use state numbers to order classes, not
their signatures.  The problem was that even if two simulation of the
same automaton assign the same signature, the BDD identifier used for
that signature might be different, and therefore the ordering obtained
by using BDDs as keys in a map can be different.  A side-effect of
this change is that the order of states in automata produced by
simulation-based reduction may change; many tests had to be updated.
* tests/core/ltl2tgba.test: Add a new test case based on Maximilien's
report.
* tests/core/complement.test, tests/core/det.test,
tests/core/parseaut.test, tests/core/prodor.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/highlighting.ipynb,
tests/python/piperead.ipynb, tests/python/testingaut.ipynb,
tests/python/word.ipynb: Update test cases for new order of states.
2017-06-03 10:03:59 +02:00

244 lines
12 KiB
Text
Raw Blame History

{
"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.3"
},
"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=\"198pt\" height=\"342pt\"\n",
" viewBox=\"0.00 0.00 197.50 342.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 338)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-338 193.5,-338 193.5,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"47.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"69.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"85.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"121.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"<text text-anchor=\"start\" x=\"137.75\" y=\"-319.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=\"-75\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-71.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,-75C2.79388,-75 17.1543,-75 30.6317,-75\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-75 30.9419,-78.1501 34.4419,-75 30.9419,-75.0001 30.9419,-75.0001 30.9419,-75.0001 34.4419,-75 30.9418,-71.8501 37.9419,-75 37.9419,-75\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-92.0373C48.3189,-101.858 50.4453,-111 56,-111 60.166,-111 62.4036,-105.858 62.7128,-99.1433\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-92.0373 65.8541,-98.8818 62.5434,-95.5335 62.7076,-99.0296 62.7076,-99.0296 62.7076,-99.0296 62.5434,-95.5335 59.561,-99.1774 62.3792,-92.0373 62.3792,-92.0373\"/>\n",
"<text text-anchor=\"start\" x=\"51.5\" y=\"-114.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" 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\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M73.3784,-81.3448C92.4242,-88.7229 123.976,-100.946 145.359,-109.229\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"151.915,-111.769 144.25,-112.178 148.652,-110.505 145.388,-109.24 145.388,-109.24 145.388,-109.24 148.652,-110.505 146.526,-106.303 151.915,-111.769 151.915,-111.769\"/>\n",
"<text text-anchor=\"start\" x=\"99\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" 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\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M72.4341,-67.0744C91.6528,-57.2053 124.596,-40.2883 146.337,-29.1242\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"152.697,-25.8583 147.909,-31.8581 149.584,-27.4571 146.47,-29.056 146.47,-29.056 146.47,-29.056 149.584,-27.4571 145.031,-26.2538 152.697,-25.8583 152.697,-25.8583\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-59.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</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=\"M166.467,-136.153C166.078,-145.539 166.922,-154 169,-154 170.526,-154 171.387,-149.437 171.582,-143.295\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"171.533,-136.153 174.731,-143.131 171.557,-139.653 171.581,-143.153 171.581,-143.153 171.581,-143.153 171.557,-139.653 168.431,-143.174 171.533,-136.153 171.533,-136.153\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-157.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=\"M165.104,-135.577C162.424,-156.718 163.723,-184 169,-184 173.7,-184 175.244,-162.36 173.633,-142.691\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"172.896,-135.577 176.75,-142.215 173.257,-139.059 173.617,-142.54 173.617,-142.54 173.617,-142.54 173.257,-139.059 170.484,-142.864 172.896,-135.577 172.896,-135.577\"/>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-187.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=\"M164.049,-135.467C158.901,-163.149 160.551,-202 169,-202 176.756,-202 178.783,-169.261 175.081,-142.477\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"173.951,-135.467 178.174,-141.877 174.508,-138.923 175.065,-142.378 175.065,-142.378 175.065,-142.378 174.508,-138.923 171.955,-142.879 173.951,-135.467 173.951,-135.467\"/>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-219.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-205.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=\"M163.463,-135.36C155.342,-171.623 157.188,-230 169,-230 180.074,-230 182.389,-178.692 175.943,-142.399\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"174.537,-135.36 178.997,-141.607 175.223,-138.792 175.908,-142.224 175.908,-142.224 175.908,-142.224 175.223,-138.792 172.819,-142.841 174.537,-135.36 174.537,-135.36\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-248.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-233.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=\"M159.425,-33.5414C156.73,-43.9087 159.922,-54 169,-54 175.95,-54 179.45,-48.0847 179.499,-40.6591\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"178.575,-33.5414 182.6,-40.0771 179.026,-37.0123 179.477,-40.4831 179.477,-40.4831 179.477,-40.4831 179.026,-37.0123 176.353,-40.889 178.575,-33.5414 178.575,-33.5414\"/>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</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 0x7f6b2060be40> >"
]
}
],
"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": {}
}
]
}
Reference in a new issue View git blame Copy permalink