From 272daf62fcabd1745361a62e925f88ea8774a441 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 12 Jun 2016 12:53:55 +0200 Subject: [PATCH] python: add a %%pml magic Fixes #162. * python/spot/ltsmin.i: Implement the magic. * NEWS: Mention it. * tests/python/ltsmin-pml.ipynb: New file. * tests/Makefile.am, doc/org/tut.org: Add it. * tests/python/ipnbdoctest.py: Adjust. --- NEWS | 5 + doc/org/tut.org | 4 +- python/spot/ltsmin.i | 58 +++- tests/Makefile.am | 1 + tests/python/ipnbdoctest.py | 4 + tests/python/ltsmin-pml.ipynb | 506 ++++++++++++++++++++++++++++++++++ 6 files changed, 564 insertions(+), 14 deletions(-) create mode 100644 tests/python/ltsmin-pml.ipynb diff --git a/NEWS b/NEWS index 2e051b415..ed6ef44bf 100644 --- a/NEWS +++ b/NEWS @@ -65,6 +65,11 @@ New in spot 2.0.1a (not yet released) * Bindings for language_containment_checker were added. + * Under IPython the spot.ltsmin modules nows offers a + %%pml magic do define promela models, compile them + with spins, and dynamically load them. This is + akin to the %%dve magic that was already supported. + Documentation: * A new example page shows how to test the equivalence of diff --git a/doc/org/tut.org b/doc/org/tut.org index 3f2742d41..639b8af51 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -63,8 +63,8 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()= function - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing automaton -- [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] minimal test for loading a DiVinE model using - the LTSmin interface. +- [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface. +- [[https://spot.lrde.epita.fr/ipynb/ltsmin-pml.html][=ltsmin-pml.ipynb=]] loading a Promela model using the LTSmin interface. - [[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. diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 1483df950..70f7dbf8b 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -106,25 +106,31 @@ class model: res += '\n'; return res -def require(tool): +def require(*tools): """ Exit with status code 77 if the required tool is not installed. This function is mostly useful in Spot test suite, where 77 is a code used to indicate that some test should be skipped. """ - if tool != "divine": - raise ValueError("unsupported argument for require(): " + tool) import shutil - if shutil.which("divine") == None: - print ("divine not available", file=sys.stderr) - sys.exit(77) - out = subprocess.check_output(['divine', 'compile', - '--help'], stderr=subprocess.STDOUT) - if b'LTSmin' not in out: - print ("divine available but no support for LTSmin", - file=sys.stderr) - sys.exit(77) + for tool in tools: + if tool == "divine": + if shutil.which("divine") == None: + print("divine not available", file=sys.stderr) + sys.exit(77) + out = subprocess.check_output(['divine', 'compile', '--help'], + stderr=subprocess.STDOUT) + if b'LTSmin' not in out: + print("divine available but no support for LTSmin", + file=sys.stderr) + sys.exit(77) + elif tool == "spins": + if shutil.which("spins") == None: + print("spins not available", file=sys.stderr) + sys.exit(77) + else: + raise ValueError("unsupported argument for require(): " + tool) # Load IPython specific support if we can. @@ -166,8 +172,36 @@ try: spot.aux.rm_f(t.name + '.cpp') spot.aux.rm_f(t.name + '2C') + @magics_class + class EditPML(Magics): + + @cell_magic + def pml(self, line, cell): + if not line: + raise ValueError("missing variable name for %%pml") + with tempfile.NamedTemporaryFile(dir='.', suffix='.pml') as t: + t.write(cell.encode('utf-8')) + t.flush() + + try: + p = subprocess.Popen(['spins', t.name], + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + universal_newlines=True) + out = p.communicate() + if out[0]: + print(out[0], file=sys.stderr) + ret = p.wait() + if ret: + raise subprocess.CalledProcessError(ret, 'spins') + self.shell.user_ns[line] = load(t.name + '.spins') + finally: + spot.aux.rm_f(t.name + '.spins.c') + spot.aux.rm_f(t.name + '.spins') + ip = get_ipython() ip.register_magics(EditDVE) + ip.register_magics(EditPML) except (ImportError, NameError): pass diff --git a/tests/Makefile.am b/tests/Makefile.am index 4d0edd4ac..391dda4e7 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -297,6 +297,7 @@ TESTS_ipython = \ python/formulas.ipynb \ python/highlighting.ipynb \ python/ltsmin-dve.ipynb \ + python/ltsmin-pml.ipynb \ python/piperead.ipynb \ python/product.ipynb \ python/randaut.ipynb \ diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index f86ac5b82..4cc65d056 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -71,6 +71,10 @@ def sanitize(s): # normalize graphviz version s = re.sub(r'Generated by graphviz version.*', 'VERSION', s) + # remove Spins verbose output version + s = re.sub(r'SpinS Promela Compiler.*Compiled C model to .*pml.spins', + 'SpinS output', s, flags=re.DOTALL) + # SVG generated by graphviz may put note at different positions # depending on the graphviz build. Let's just strip anything that # look like a position. diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb new file mode 100644 index 000000000..381b6f29e --- /dev/null +++ b/tests/python/ltsmin-pml.ipynb @@ -0,0 +1,506 @@ +{ + "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.1" + }, + "name": "", + "signature": "sha256:bbe178ef6526ace33fca472e0e20c706861b6b033a70d184f5a219c60812d5b7" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "import spot.ltsmin\n", + "# The following line causes the notebook to exit with 77 if spins is not \n", + "# installed, therefore skipping this test in the test suite.\n", + "spot.ltsmin.require('spins')\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "There are two ways to load a Promela model: from a file or from a cell. \n", + "\n", + "Loading from a cell\n", + "-------------------\n", + "\n", + "Using the `%%pml` magic will save the model in a temporary file, call `spins` to compile it, load the resulting shared library, and store the result into an object whose name is passed as an argument to `%%pml`." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%%pml model\n", + "active proctype P() {\n", + "int a = 0;\n", + "int b = 0;\n", + "x: if\n", + " :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n", + " :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n", + "fi;\n", + "}" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stderr", + "text": [ + "SpinS Promela Compiler - version 1.0 (5-Feb-2013)\n", + "(C) University of Twente, Formal Methods and Tools group\n", + "\n", + "Start parsing tmplq2ksakk.pml...done\n", + "\n", + "Optimizing graphs...\n", + " StateMerging changed 0 states/transitions.\n", + " RemoveUselessActions changed 2 states/transitions.\n", + " RemoveUselessGotos changed 2 states/transitions.\n", + " RenumberAll changed 1 states/transitions.\n", + "Optimization done\n", + "\n", + "Generating DM information ...\n", + "Generating DM information done\n", + "\n", + "Generating guard information ...\n", + " Found 0 / 4 ( 0.0%) !MCE guards.\n", + " Found 3 / 8 ( 37.5%) !IMC guards.\n", + " Found 6 / 6 (100.0%) !NES guards.\n", + " Found 6 / 6 (100.0%) !NDS guards.\n", + " Found 6 / 6 (100.0%) !visibilities.\n", + "Generating guard information done\n", + "\n", + "Written C model to /home/adl/git/spot/tests/python/tmplq2ksakk.pml.spins.c\n", + "Compiled C model to tmplq2ksakk.pml.spins\n", + "\n" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Yes, the `spins` compiler is quite verbose. Printing the resulting `model` object will show information about the variables in that model. " + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "model" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "text": [ + "ltsmin model with the following variables:\n", + " _nr_pr: int\n", + " P_0._pc: pc\n", + " P_0._pid: pid\n", + " P_0.a: int\n", + " P_0.b: int" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To instantiate a Kripke structure, one should provide a list of atomic proposition to observe." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "\n", + "5->9\n", + "\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "\n", + "\n", + "7->10\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "\n", + "7->11\n", + "\n", + "\n", + "\n", + "\n", + "8->11\n", + "\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "\n", + "8->12\n", + "\n", + "\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "\n", + "\n", + "10->10\n", + "\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "\n", + "11->13\n", + "\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=3\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "\n", + "11->14\n", + "\n", + "\n", + "\n", + "\n", + "12->12\n", + "\n", + "\n", + "\n", + "\n", + "13->13\n", + "\n", + "\n", + "\n", + "\n", + "14->14\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f87ac090240> >" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "And then from this Kripke structure you can do some model checking using the same functions as illustrated in `ltsmin-dve.ipynb`.\n", + "\n", + "Loading from a `*.pml` file\n", + "---------------------------\n", + "\n", + "Another option is to use `ltsmin.load()` to load a Promela file directly. In order for this test-case to be self-contained, we are going to write the Promela file first, but in practice you probably already have your model." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "!rm -rf test1.pml" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%%file test1.pml\n", + "active proctype P() {\n", + "int a = 0;\n", + "int b = 0;\n", + "x: if\n", + " :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n", + " :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n", + "fi;\n", + "}" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Writing test1.pml\n" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Now load it:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "model2 = spot.ltsmin.load('test1.pml')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 7 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "model2" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 8, + "text": [ + "ltsmin model with the following variables:\n", + " _nr_pr: int\n", + " P_0._pc: pc\n", + " P_0._pid: pid\n", + " P_0.a: int\n", + " P_0.b: int" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "!rm -f test1.pml test1.pml.spins.c test1.pml.spins" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 9 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file