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"
+ ],
+ "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