From 9692d734a986e49278f2f9386c860a2a4ef75dfb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 16 Feb 2016 19:08:28 +0100 Subject: [PATCH] cleanup ltsmin bindings * python/spot/aux.py (rm_f): new function. * python/spot/ltsmin.i: Replace the %require magic by a simple function. Rewrite the %%dve magic. * tests/python/otfcrash.py: Simplify using spot.ltsmin.require() * tests/python/ltsmin.ipynb: Likewise, also add more text for the documentation. * NEWS: Adjust. --- NEWS | 8 +- python/spot/aux.py | 14 +- python/spot/ltsmin.i | 103 ++-- tests/python/ltsmin.ipynb | 1036 ++++++++++++++++++------------------- tests/python/otfcrash.py | 9 +- 5 files changed, 559 insertions(+), 611 deletions(-) diff --git a/NEWS b/NEWS index 393b37e32..7b3f7da9a 100644 --- a/NEWS +++ b/NEWS @@ -104,11 +104,9 @@ New in spot 1.99.7a (not yet released) Python: - * The ltsmin interface has been binded in Python. See - https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example. - - * The ltsmin interface support two extra 'magic commands' when ipython - is used: %dve and %%require. + * The ltsmin interface has been binded in Python. It also + comes with a %%dve cell magic to edit DiVinE models in the notebook. + See https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example. * spot.setup() sets de maximum number of states to display in automata to 50 by default, as more states is likely to be diff --git a/python/spot/aux.py b/python/spot/aux.py index a85c26f30..9990df882 100644 --- a/python/spot/aux.py +++ b/python/spot/aux.py @@ -24,7 +24,8 @@ Auxiliary functions for Spot's Python bindings from functools import lru_cache import subprocess import sys - +import os +import errno def extend(*classes): """ @@ -68,3 +69,14 @@ def ostream_to_svg(ostr): Encode an ostringstream as utf-8 and send it to dot for cocnversion to SVG. """ return str_to_svg(ostr.str().encode('utf-8')) + + +def rm_f(filename): + """ + Remove filename if it exists. + """ + try: + os.remove(filename) + except OSError as e: + if e.errno != errno.ENOENT: + raise diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 31c858ecf..03e490de2 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -67,6 +67,9 @@ namespace std { %pythoncode %{ import spot +import spot.aux +import sys +import subprocess def load(filename): return model.load(filename) @@ -107,75 +110,65 @@ class model: res += '\n'; return res +def require(tool): + """ + 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) + + # Load IPython specific support if we can. try: # Load only if we are running IPython. __IPYTHON__ - from IPython.core.magic import (Magics, magics_class, line_cell_magic) - from IPython.core.magic_arguments \ - import (argument, magic_arguments, parse_argstring) + from IPython.core.magic import Magics, magics_class, cell_magic import os import tempfile - import sys - import shutil - try: - import ipywidgets as widgets - except ImportError: - pass - # This class provides support for %%dve model description @magics_class class EditDVE(Magics): - @line_cell_magic - def dve(self, line, cell=None): - try: - # DiViNe prefers when files are in the current directory - # so write cell into local file - t = tempfile.NamedTemporaryFile(dir=os.getcwd()) - filename = t.name + '.dve' - f = open(filename,"w") - f.write(cell) - f.close() + @cell_magic + def dve(self, line, cell): + if not line: + raise ValueError("missing variable name for %%dve") + # DiViNe prefers when files are in the current directory + # so write cell into local file + with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as t: + t.write(cell.encode('utf-8')) + t.flush() - # Then compile and unlink temporary files - import subprocess - out="" - self.shell.user_ns[line] = None - out = subprocess.check_call(['divine', 'compile', - '--ltsmin', filename]) - os.unlink(filename) - os.unlink(filename + '.cpp') - self.shell.user_ns[line] = load(filename + '2C') - os.unlink(filename + '2C') - except Exception as error: try: - os.unlink(filename) - os.unlink(filename + '.cpp') + p = subprocess.Popen(['divine', 'compile', + '--ltsmin', 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, 'divine') + self.shell.user_ns[line] = load(t.name + '2C') finally: - if out != "": - raise RuntimeError(out) from error - raise error - - @line_cell_magic - def require(self, line, cell=None): - if line != "divine": - print ("Unknown" + line, file=sys.stderr) - sys.exit(77) - if cell != None: - print ("No support for Cell magic command") - sys.exit(77) - if shutil.which("divine") == None: - print ("divine not available", file=sys.stderr) - sys.exit(77) - import subprocess - 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) + spot.aux.rm_f(t.name + '.cpp') + spot.aux.rm_f(t.name + '2C') ip = get_ipython() ip.register_magics(EditDVE) diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index 59e73cc9a..2401b5f70 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -17,33 +17,25 @@ "pygments_lexer": "ipython3", "version": "3.5.1" }, - "name": "" + "name": "", + "signature": "sha256:0c10865a9a58374d983e19129ce565c14e590067c1eedf4f12dfe62fa3f58a02" }, "nbformat": 3, "nbformat_minor": 0, "worksheets": [ { "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "This first chunk just makes sure the version of DiVinE installed accepts the `--LTSmin` option. If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that." - ] - }, { "cell_type": "code", "collapsed": false, "input": [ - "import sys\n", - "# Make sure we have divine and that it is patched to accept the --LTSmin option.\n", - "import shutil\n", - "if shutil.which(\"divine\") == None:\n", - " sys.exit(77)\n", - "import subprocess\n", - "out = subprocess.check_output(['divine', 'compile', '--help'], stderr=subprocess.STDOUT)\n", - "if b'LTSmin' not in out:\n", - " sys.exit(77)" + "import spot\n", + "import spot.ltsmin\n", + "# The following line causes the notebook to exit with 77 if the divine is not \n", + "# installed, therefore skipping this test in the test suite.\n", + "spot.ltsmin.require('divine')\n", + "# This is notebook also tests the limitation of the number of states in the GraphViz output\n", + "spot.setup(max_states=10)" ], "language": "python", "metadata": {}, @@ -54,49 +46,12 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The real test case starts here." - ] - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "import spot\n", - "import spot.ltsmin\n", - "# This is notebook also tests the limitation of the number of states in the GraphViz output\n", - "spot.setup(max_states=10)" - ], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": 2 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "The check of DiVinE and the setup of Spot can also be done with only:" - ] - }, - { - "cell_type": "code", - "collapsed": true, - "input": [ - "import spot\n", - "import spot.ltsmin\n", - "%require divine\n", - "spot.setup(max_states=10)" - ], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": 3 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Write an example DiVinE model. " + "There are two ways to load a DiVinE model: from a file or from a cell. \n", + "\n", + "Loading from a file\n", + "-------------------\n", + "\n", + "We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file." ] }, { @@ -108,7 +63,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 4 + "prompt_number": 2 }, { "cell_type": "code", @@ -147,54 +102,61 @@ ] } ], - "prompt_number": 5 + "prompt_number": 3 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Compile the model using the `ltlmin` interface and load it. This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed.\n", - "\n", - "Printing an ltsmin model shows some information about the variables it contains and their types." + "The `spot.ltsmin.load` function compiles the model using the `ltlmin` interface and load it. This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed." ] }, { "cell_type": "code", "collapsed": false, "input": [ - "m = spot.ltsmin.load('test1.dve')\n", - "m" + "m = spot.ltsmin.load('test1.dve')" ], "language": "python", "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "pyout", - "prompt_number": 6, - "text": [ - "ltsmin model with the following variables:\n", - " a: int\n", - " b: int\n", - " P: ['x']\n", - " Q: ['wait', 'work']" - ] - } - ], - "prompt_number": 6 + "outputs": [], + "prompt_number": 4 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "You can also directly load the model into variable m1 by using %dve command" + "Compiling the model creates all several kinds of files. The `test1.dve` file is converted into a C++ source code `test1.dve.cpp` which is then compiled into a shared library `test1.dve2c`. Becauce `spot.ltsmin.load()` has already loaded this shared library, all those files can be erased. If you do not erase the files, `spot.ltsmin.load()` will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.\n", + "\n", + "For editing and loading DVE file from a notebook, it is a better to use the `%%dve` as shown next." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "!rm -f test1.dve test1.dve.cpp test1.dve2C" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Loading from a notebook cell\n", + "----------------------------\n", + "\n", + "The `%%dve` cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files). The variable name that should receive the model (here `m`) should be indicated on the first line, after `%dve`." ] }, { "cell_type": "code", "collapsed": true, "input": [ - "%%dve m1\n", + "%%dve m\n", "int a = 0, b = 0;\n", "\n", "process P {\n", @@ -219,13 +181,23 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 7 + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Working with an ltsmin model\n", + "----------------------------\n", + "\n", + "Printing an ltsmin model shows some information about the variables it contains and their types, however the `info()` methods provide the data in a map that is easier to work with." + ] }, { "cell_type": "code", "collapsed": false, "input": [ - "m1" + "m" ], "language": "python", "metadata": {}, @@ -233,7 +205,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 8, + "prompt_number": 7, "text": [ "ltsmin model with the following variables:\n", " a: int\n", @@ -243,7 +215,7 @@ ] } ], - "prompt_number": 8 + "prompt_number": 7 }, { "cell_type": "code", @@ -257,7 +229,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 9, + "prompt_number": 8, "text": [ "[('state_size', 4),\n", " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n", @@ -265,7 +237,14 @@ ] } ], - "prompt_number": 9 + "prompt_number": 8 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To obtain a Kripke structure, call `kripke` and supply a list of atomic propositions to observe in the model." + ] }, { "cell_type": "code", @@ -280,7 +259,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 10, + "prompt_number": 9, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "a=2, b=1, Q=0\n", - "...\n", + "\n", + "a=2, b=1, Q=0\n", + "...\n", "\n", "\n", "3->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "a=1, b=2, Q=0\n", - "...\n", + "\n", + "a=1, b=2, Q=0\n", + "...\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u5\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "5->u5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=0, b=3, Q=0\n", - "...\n", + "\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", "5->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u7\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "7->u7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u8\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "8->u8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u9\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "9->u9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x109e19ed0> >" + " *' at 0x7fda50a73c90> >" ] } ], - "prompt_number": 10 + "prompt_number": 9 }, { "cell_type": "code", @@ -486,272 +465,272 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 11, + "prompt_number": 10, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "a=2, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "a=1, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=0, b=3, Q=0\n", - "...\n", + "\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", "5->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10\n", - "\n", - "a=0, b=2, Q=1\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11\n", - "\n", - "a=3, b=1, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "12\n", - "\n", - "a=2, b=2, Q=0\n", - "...\n", + "\n", + "a=2, b=2, Q=0\n", + "...\n", "\n", "\n", "7->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "13\n", - "\n", - "a=1, b=3, Q=0\n", - "...\n", + "\n", + "a=1, b=3, Q=0\n", + "...\n", "\n", "\n", "8->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14\n", - "\n", - "a=1, b=2, Q=1\n", - "...\n", + "\n", + "a=1, b=2, Q=1\n", + "...\n", "\n", "\n", "8->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u9\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "9->u9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u10\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "10->u10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u12\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "12->u12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u13\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "13->u13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "u14\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "14->u14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], - "prompt_number": 11 + "prompt_number": 10 }, { "cell_type": "code", @@ -765,349 +744,349 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 12, + "prompt_number": 11, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "a=2, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "a=1, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=0, b=3, Q=0\n", - ""a<1" & "b>2" & !dead\n", + "\n", + "a=0, b=3, Q=0\n", + ""a<1" & "b>2" & !dead\n", "\n", "\n", "5->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10\n", - "\n", - "a=0, b=2, Q=1\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11\n", - "\n", - "a=3, b=1, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "12\n", - "\n", - "a=2, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "7->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "13\n", - "\n", - "a=1, b=3, Q=0\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "a=1, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "8->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14\n", - "\n", - "a=1, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=1, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "8->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "15\n", - "\n", - "a=0, b=3, Q=1\n", - ""a<1" & "b>2" & dead\n", + "\n", + "a=0, b=3, Q=1\n", + ""a<1" & "b>2" & dead\n", "\n", "\n", "9->15\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10->15\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "16\n", - "\n", - "a=3, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=3, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->16\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "17\n", - "\n", - "a=2, b=3, Q=0\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "a=2, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "12->17\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "18\n", - "\n", - "a=2, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=2, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->18\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "19\n", - "\n", - "a=1, b=3, Q=1\n", - "!"a<1" & "b>2" & dead\n", + "\n", + "a=1, b=3, Q=1\n", + "!"a<1" & "b>2" & dead\n", "\n", "\n", "13->19\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14->18\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14->19\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "15->15\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "20\n", - "\n", - "a=3, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "\n", + "a=3, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "16->20\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "21\n", - "\n", - "a=2, b=3, Q=1\n", - "!"a<1" & "b>2" & !dead\n", + "\n", + "a=2, b=3, Q=1\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "17->21\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "18->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "18->20\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "18->21\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "19->19\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "20->16\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "21->17\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], - "prompt_number": 12 + "prompt_number": 11 }, { "cell_type": "code", @@ -1121,7 +1100,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 13, + "prompt_number": 12, "svg": [ "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", @@ -1149,35 +1128,35 @@ "1->1\n", "\n", "\n", - ""a<1" & !"b>2"\n", + ""a<1" & !"b>2"\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", ""b>2"\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x109eaaab0> >" + " *' at 0x7fda58aa2270> >" ] } ], - "prompt_number": 13 + "prompt_number": 12 }, { "cell_type": "code", @@ -1191,7 +1170,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 14, + "prompt_number": 13, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "a=0, b=0, Q=0 * 1\n", + "\n", + "a=0, b=0, Q=0 * 1\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "a=1, b=0, Q=0 * 1\n", + "\n", + "a=1, b=0, Q=0 * 1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2\n", - "\n", - "a=0, b=1, Q=0 * 1\n", + "\n", + "a=0, b=1, Q=0 * 1\n", "\n", "\n", "0->2\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "3\n", - "\n", - "a=1, b=1, Q=0 * 1\n", + "\n", + "a=1, b=1, Q=0 * 1\n", "\n", "\n", "2->3\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "4\n", - "\n", - "a=0, b=2, Q=0 * 1\n", + "\n", + "a=0, b=2, Q=0 * 1\n", "\n", "\n", "2->4\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5\n", - "\n", - "a=1, b=2, Q=0 * 1\n", + "\n", + "a=1, b=2, Q=0 * 1\n", "\n", "\n", "4->5\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "6\n", - "\n", - "a=0, b=3, Q=0 * 1\n", + "\n", + "a=0, b=3, Q=0 * 1\n", "\n", "\n", "4->6\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "7\n", - "\n", - "a=0, b=2, Q=1 * 1\n", + "\n", + "a=0, b=2, Q=1 * 1\n", "\n", "\n", "4->7\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "8\n", - "\n", - "a=0, b=3, Q=1 * 0\n", + "\n", + "a=0, b=3, Q=1 * 0\n", "\n", "\n", "6->8\n", - "\n", - "\n", - ""a<1" & "b>2" & !dead\n", + "\n", + "\n", + ""a<1" & "b>2" & !dead\n", "\n", "\n", "u7\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "7->u7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "a=1, b=2, Q=1 * 1\n", + "\n", + "a=1, b=2, Q=1 * 1\n", "\n", "\n", "7->9\n", - "\n", - "\n", - ""a<1" & !"b>2" & !dead\n", + "\n", + "\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "8->8\n", - "\n", - "\n", - ""a<1" & "b>2" & dead\n", - "\u24ff\n", + "\n", + "\n", + ""a<1" & "b>2" & dead\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x109e19e70> >" + " *' at 0x7fda50a736f0> >" ] } ], - "prompt_number": 14 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "!rm -f test1.dve" - ], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": 15 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Note that using %%dve does not require any deletion." - ] - }, - { - "cell_type": "code", - "collapsed": true, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": null + "prompt_number": 13 } ], "metadata": {} diff --git a/tests/python/otfcrash.py b/tests/python/otfcrash.py index a68e179fd..ce3bc5a29 100644 --- a/tests/python/otfcrash.py +++ b/tests/python/otfcrash.py @@ -4,14 +4,7 @@ import tempfile import shutil import sys -# this test requires divine with --ltsmin support -if shutil.which("divine") == None: - sys.exit(77) -import subprocess -out = subprocess.check_output(['divine', 'compile', - '--help'], stderr=subprocess.STDOUT) -if b'LTSmin' not in out: - sys.exit(77) +spot.ltsmin.require('divine') # the test case actually starts here with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as fp: