Provide support for %dve and %require
* NEWS, python/spot/ltsmin.i, tests/python/ltsmin.ipynb: Here.
This commit is contained in:
parent
369c2c537d
commit
091251b5b7
3 changed files with 1106 additions and 928 deletions
3
NEWS
3
NEWS
|
|
@ -87,6 +87,9 @@ New in spot 1.99.7a (not yet released)
|
||||||
* The ltsmin interface has been binded in Python. See
|
* The ltsmin interface has been binded in Python. See
|
||||||
https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example.
|
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.
|
||||||
|
|
||||||
* spot.setup() sets de maximum number of states to display in
|
* spot.setup() sets de maximum number of states to display in
|
||||||
automata to 50 by default, as more states is likely to be
|
automata to 50 by default, as more states is likely to be
|
||||||
unreadable (and slow to process by GraphViz). This can be
|
unreadable (and slow to process by GraphViz). This can be
|
||||||
|
|
|
||||||
|
|
@ -106,4 +106,80 @@ class model:
|
||||||
res += type
|
res += type
|
||||||
res += '\n';
|
res += '\n';
|
||||||
return res
|
return res
|
||||||
|
|
||||||
|
# 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)
|
||||||
|
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:
|
||||||
|
try:
|
||||||
|
os.unlink(filename)
|
||||||
|
os.unlink(filename + '.cpp')
|
||||||
|
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)
|
||||||
|
|
||||||
|
ip = get_ipython()
|
||||||
|
ip.register_magics(EditDVE)
|
||||||
|
|
||||||
|
except (ImportError, NameError):
|
||||||
|
pass
|
||||||
%}
|
%}
|
||||||
|
|
|
||||||
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue