Commit 9692d734 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 9b5a7635
......@@ -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
......
......@@ -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
......@@ -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()
# 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:
@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()
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)
......
This diff is collapsed.
......@@ -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:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment