diff --git a/NEWS b/NEWS
index 52e43df6e..6a77bc885 100644
--- a/NEWS
+++ b/NEWS
@@ -87,6 +87,9 @@ New in spot 1.99.7a (not yet released)
* 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.
+
* spot.setup() sets de maximum number of states to display in
automata to 50 by default, as more states is likely to be
unreadable (and slow to process by GraphViz). This can be
diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i
index 5b33b525b..31c858ecf 100644
--- a/python/spot/ltsmin.i
+++ b/python/spot/ltsmin.i
@@ -106,4 +106,80 @@ class model:
res += type
res += '\n';
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
%}
diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb
index a149b8134..59e73cc9a 100644
--- a/tests/python/ltsmin.ipynb
+++ b/tests/python/ltsmin.ipynb
@@ -15,7 +15,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
- "version": "3.4.3+"
+ "version": "3.5.1"
},
"name": ""
},
@@ -71,6 +71,27 @@
"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": {},
@@ -87,7 +108,7 @@
"language": "python",
"metadata": {},
"outputs": [],
- "prompt_number": 3
+ "prompt_number": 4
},
{
"cell_type": "code",
@@ -126,7 +147,7 @@
]
}
],
- "prompt_number": 4
+ "prompt_number": 5
},
{
"cell_type": "markdown",
@@ -150,7 +171,7 @@
{
"metadata": {},
"output_type": "pyout",
- "prompt_number": 5,
+ "prompt_number": 6,
"text": [
"ltsmin model with the following variables:\n",
" a: int\n",
@@ -160,7 +181,69 @@
]
}
],
- "prompt_number": 5
+ "prompt_number": 6
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "You can also directly load the model into variable m1 by using %dve command"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "%%dve m1\n",
+ "int a = 0, b = 0;\n",
+ "\n",
+ "process P {\n",
+ " state x;\n",
+ " init x;\n",
+ "\n",
+ " trans\n",
+ " x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
+ " x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
+ "}\n",
+ "\n",
+ "process Q {\n",
+ " state wait, work;\n",
+ " init wait;\n",
+ " trans\n",
+ " wait -> work { guard b > 1; },\n",
+ " work -> wait { guard a > 1; };\n",
+ "}\n",
+ "\n",
+ "system async;"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 7
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "m1"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 8,
+ "text": [
+ "ltsmin model with the following variables:\n",
+ " a: int\n",
+ " b: int\n",
+ " P: ['x']\n",
+ " Q: ['wait', 'work']"
+ ]
+ }
+ ],
+ "prompt_number": 8
},
{
"cell_type": "code",
@@ -174,7 +257,7 @@
{
"metadata": {},
"output_type": "pyout",
- "prompt_number": 6,
+ "prompt_number": 9,
"text": [
"[('state_size', 4),\n",
" ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
@@ -182,855 +265,14 @@
]
}
],
- "prompt_number": 6
- },
- {
- "cell_type": "code",
- "collapsed": false,
- "input": [
- "k = m.kripke([\"a<1\", \"b>2\"])\n",
- "k"
- ],
- "language": "python",
- "metadata": {},
- "outputs": [
- {
- "metadata": {},
- "output_type": "pyout",
- "prompt_number": 7,
- "svg": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text": [
- " *' at 0x7f426c309690> >"
- ]
- }
- ],
- "prompt_number": 7
- },
- {
- "cell_type": "code",
- "collapsed": false,
- "input": [
- "k.show('.<15')"
- ],
- "language": "python",
- "metadata": {},
- "outputs": [
- {
- "metadata": {},
- "output_type": "pyout",
- "prompt_number": 8,
- "svg": [
- ""
- ],
- "text": [
- ""
- ]
- }
- ],
- "prompt_number": 8
- },
- {
- "cell_type": "code",
- "collapsed": false,
- "input": [
- "k.show('.<0') # unlimited output"
- ],
- "language": "python",
- "metadata": {},
- "outputs": [
- {
- "metadata": {},
- "output_type": "pyout",
- "prompt_number": 9,
- "svg": [
- ""
- ],
- "text": [
- ""
- ]
- }
- ],
"prompt_number": 9
},
{
"cell_type": "code",
"collapsed": false,
"input": [
- "a = spot.translate('\"a<1\" U \"b>2\"'); a"
+ "k = m.kripke([\"a<1\", \"b>2\"])\n",
+ "k"
],
"language": "python",
"metadata": {},
@@ -1046,11 +288,852 @@
"\n",
"\n",
- "