From a1260105a44d4bd436614872ffb7103ae6f3f114 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 14:18:48 +0200 Subject: [PATCH] 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. --- doc/org/tut.org | 2 + tests/Makefile.am | 2 + tests/python/atva16-fig2a.ipynb | 261 ++++++++++++++++++++++++ tests/python/atva16-fig2b.ipynb | 340 ++++++++++++++++++++++++++++++++ 4 files changed, 605 insertions(+) create mode 100644 tests/python/atva16-fig2a.ipynb create mode 100644 tests/python/atva16-fig2b.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index 639b8af51..6233324bc 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -68,3 +68,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]]. diff --git a/tests/Makefile.am b/tests/Makefile.am index 3c585789a..858106b57 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -291,6 +291,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 \ diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb new file mode 100644 index 000000000..8e2b789aa --- /dev/null +++ b/tests/python/atva16-fig2a.ipynb @@ -0,0 +1,261 @@ +{ + "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": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' 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": {} + } + ] +} diff --git a/tests/python/atva16-fig2b.ipynb b/tests/python/atva16-fig2b.ipynb new file mode 100644 index 000000000..59023578d --- /dev/null +++ b/tests/python/atva16-fig2b.ipynb @@ -0,0 +1,340 @@ +{ + "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": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "t\n", + "\n", + "\n", + "0\n", + "\n", + "c=1, x1=0, x2=0, a1=0, a2=0\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "c=1, x1=1, x2=0, a1=1, a2=0\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "c=1, x1=0, x2=1, a1=0, a2=1\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "c=1, x1=2, x2=0, a1=2, a2=0\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "c=1, x1=1, x2=1, a1=1, a2=1\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "c=1, x1=0, x2=2, a1=0, a2=2\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "c=2, x1=2, x2=0, a1=0, a2=0\n", + "...\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "c=1, x1=2, x2=1, a1=2, a2=1\n", + "...\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "c=1, x1=1, x2=2, a1=1, a2=2\n", + "...\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "c=2, x1=0, x2=2, a1=0, a2=0\n", + "...\n", + "\n", + "\n", + "5->9\n", + "\n", + "\n", + "\n", + "\n", + "u6\n", + "\n", + "...\n", + "\n", + "\n", + "6->u6\n", + "\n", + "\n", + "\n", + "\n", + "u7\n", + "\n", + "...\n", + "\n", + "\n", + "7->u7\n", + "\n", + "\n", + "\n", + "\n", + "u8\n", + "\n", + "...\n", + "\n", + "\n", + "8->u8\n", + "\n", + "\n", + "\n", + "\n", + "u9\n", + "\n", + "...\n", + "\n", + "\n", + "9->u9\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' 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": {} + } + ] +}