alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: add a %%pml magic

Browse source 
Fixes #162.

* python/spot/ltsmin.i: Implement the magic.
* NEWS: Mention it.
* tests/python/ltsmin-pml.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2016-06-12 12:53:55 +02:00
parent a7e4395f9d
commit 272daf62fc
6 changed files with 564 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -65,6 +65,11 @@ New in spot 2.0.1a (not yet released)
* Bindings for language_containment_checker were added. * 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: Documentation:
* A new example page shows how to test the equivalence of * A new example page shows how to test the equivalence of

4
doc/org/tut.org
View file

@ -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/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 - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing
automaton automaton
- [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] minimal test for loading a DiVinE model using - [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface.
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/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 - [[https://spot.lrde.epita.fr/ipynb/highlighting.html][=highlighting.ipynb=]] shows how to highlight states or edges in
automata. automata.

58
python/spot/ltsmin.i
View file

@ -106,25 +106,31 @@ class model:
res += '\n'; res += '\n';
return res return res
def require(tool): def require(*tools):
""" """
Exit with status code 77 if the required tool is not installed. 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 This function is mostly useful in Spot test suite, where 77 is a
code used to indicate that some test should be skipped. code used to indicate that some test should be skipped.
""" """
if tool != "divine":
raise ValueError("unsupported argument for require(): " + tool)
import shutil import shutil
if shutil.which("divine") == None: for tool in tools:
print ("divine not available", file=sys.stderr) if tool == "divine":
sys.exit(77) if shutil.which("divine") == None:
out = subprocess.check_output(['divine', 'compile', print("divine not available", file=sys.stderr)
'--help'], stderr=subprocess.STDOUT) sys.exit(77)
if b'LTSmin' not in out: out = subprocess.check_output(['divine', 'compile', '--help'],
print ("divine available but no support for LTSmin", stderr=subprocess.STDOUT)
file=sys.stderr) if b'LTSmin' not in out:
sys.exit(77) 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. # 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 + '.cpp')
spot.aux.rm_f(t.name + '2C') 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 = get_ipython()
ip.register_magics(EditDVE) ip.register_magics(EditDVE)
ip.register_magics(EditPML)
except (ImportError, NameError): except (ImportError, NameError):
pass pass

1
tests/Makefile.am
View file

@ -297,6 +297,7 @@ TESTS_ipython = \
python/formulas.ipynb \ python/formulas.ipynb \
python/highlighting.ipynb \ python/highlighting.ipynb \
python/ltsmin-dve.ipynb \ python/ltsmin-dve.ipynb \
python/ltsmin-pml.ipynb \
python/piperead.ipynb \ python/piperead.ipynb \
python/product.ipynb \ python/product.ipynb \
python/randaut.ipynb \ python/randaut.ipynb \

4
tests/python/ipnbdoctest.py
View file

@ -71,6 +71,10 @@ def sanitize(s):
# normalize graphviz version # normalize graphviz version
s = re.sub(r'Generated by graphviz version.*', 'VERSION', s) 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 # SVG generated by graphviz may put note at different positions
# depending on the graphviz build. Let's just strip anything that # depending on the graphviz build. Let's just strip anything that
# look like a position. # look like a position.

506
tests/python/ltsmin-pml.ipynb Normal file
View file

@ -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": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"75pt\"\n",
" viewBox=\"0.00 0.00 734.00 75.07\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.239277 0.239277) rotate(0) translate(4 309.74)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-309.74 3063.57,-309.74 3063.57,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"273.881\" cy=\"-152.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"273.881\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=0</text>\n",
"<text text-anchor=\"middle\" x=\"273.881\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.04952,-152.87C1.86795,-152.87 12.7769,-152.87 29.7957,-152.87\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"36.8867,-152.87 29.8867,-156.02 33.3867,-152.87 29.8867,-152.87 29.8867,-152.87 29.8867,-152.87 33.3867,-152.87 29.8867,-149.72 36.8867,-152.87 36.8867,-152.87\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"783.642\" cy=\"-188.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"783.642\" y=\"-192.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=0</text>\n",
"<text text-anchor=\"middle\" x=\"783.642\" y=\"-177.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M475.197,-167.072C508.083,-169.404 542.225,-171.825 575.278,-174.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"582.314,-174.667 575.109,-177.314 578.823,-174.419 575.331,-174.172 575.331,-174.172 575.331,-174.172 578.823,-174.419 575.554,-171.03 582.314,-174.667 582.314,-174.667\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"783.642\" cy=\"-116.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"783.642\" y=\"-120.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=1</text>\n",
"<text text-anchor=\"middle\" x=\"783.642\" y=\"-105.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M475.197,-138.668C508.083,-136.336 542.225,-133.915 575.278,-131.572\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"582.314,-131.073 575.554,-134.71 578.823,-131.321 575.331,-131.568 575.331,-131.568 575.331,-131.568 578.823,-131.321 575.109,-128.426 582.314,-131.073 582.314,-131.073\"/>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1293.4\" cy=\"-224.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-228.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=0</text>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-213.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M984.959,-203.072C1017.84,-205.404 1051.99,-207.825 1085.04,-210.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1092.08,-210.667 1084.87,-213.314 1088.58,-210.419 1085.09,-210.172 1085.09,-210.172 1085.09,-210.172 1088.58,-210.419 1085.32,-207.03 1092.08,-210.667 1092.08,-210.667\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\"><title>4</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1293.4\" cy=\"-152.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=1</text>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M984.959,-174.668C1017.84,-172.336 1051.99,-169.915 1085.04,-167.572\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1092.08,-167.073 1085.32,-170.71 1088.58,-167.321 1085.09,-167.568 1085.09,-167.568 1085.09,-167.568 1088.58,-167.321 1084.87,-164.426 1092.08,-167.073 1092.08,-167.073\"/>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M984.959,-131.072C1017.84,-133.404 1051.99,-135.825 1085.04,-138.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1092.08,-138.667 1084.87,-141.314 1088.58,-138.419 1085.09,-138.172 1085.09,-138.172 1085.09,-138.172 1088.58,-138.419 1085.32,-135.03 1092.08,-138.667 1092.08,-138.667\"/>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\"><title>5</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1293.4\" cy=\"-80.8701\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-84.6701\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=2</text>\n",
"<text text-anchor=\"middle\" x=\"1293.4\" y=\"-69.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M984.959,-102.668C1017.84,-100.336 1051.99,-97.9155 1085.04,-95.5721\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1092.08,-95.0732 1085.32,-98.7105 1088.58,-95.3208 1085.09,-95.5684 1085.09,-95.5684 1085.09,-95.5684 1088.58,-95.3208 1084.87,-92.4263 1092.08,-95.0732 1092.08,-95.0732\"/>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node8\" class=\"node\"><title>6</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1803.17\" cy=\"-260.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-264.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=0</text>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-249.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;6 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1494.72,-239.072C1527.61,-241.404 1561.75,-243.825 1594.8,-246.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1601.84,-246.667 1594.63,-249.314 1598.35,-246.419 1594.85,-246.172 1594.85,-246.172 1594.85,-246.172 1598.35,-246.419 1595.08,-243.03 1601.84,-246.667 1601.84,-246.667\"/>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g id=\"node9\" class=\"node\"><title>7</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1803.17\" cy=\"-188.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-192.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=1</text>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-177.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;7 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1494.72,-210.668C1527.61,-208.336 1561.75,-205.915 1594.8,-203.572\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1601.84,-203.073 1595.08,-206.71 1598.35,-203.321 1594.85,-203.568 1594.85,-203.568 1594.85,-203.568 1598.35,-203.321 1594.63,-200.426 1601.84,-203.073 1601.84,-203.073\"/>\n",
"</g>\n",
"<!-- 4&#45;&gt;7 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1494.72,-167.072C1527.61,-169.404 1561.75,-171.825 1594.8,-174.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1601.84,-174.667 1594.63,-177.314 1598.35,-174.419 1594.85,-174.172 1594.85,-174.172 1594.85,-174.172 1598.35,-174.419 1595.08,-171.03 1601.84,-174.667 1601.84,-174.667\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g id=\"node10\" class=\"node\"><title>8</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1803.17\" cy=\"-116.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-120.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=2</text>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-105.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;8 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1494.72,-138.668C1527.61,-136.336 1561.75,-133.915 1594.8,-131.572\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1601.84,-131.073 1595.08,-134.71 1598.35,-131.321 1594.85,-131.568 1594.85,-131.568 1594.85,-131.568 1598.35,-131.321 1594.63,-128.426 1601.84,-131.073 1601.84,-131.073\"/>\n",
"</g>\n",
"<!-- 5&#45;&gt;8 -->\n",
"<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1494.72,-95.0724C1527.61,-97.404 1561.75,-99.8246 1594.8,-102.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1601.84,-102.667 1594.63,-105.314 1598.35,-102.419 1594.85,-102.172 1594.85,-102.172 1594.85,-102.172 1598.35,-102.419 1595.08,-99.0296 1601.84,-102.667 1601.84,-102.667\"/>\n",
"</g>\n",
"<!-- 9 -->\n",
"<g id=\"node11\" class=\"node\"><title>9</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1803.17\" cy=\"-26.8701\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=3</text>\n",
"<text text-anchor=\"middle\" x=\"1803.17\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;9 -->\n",
"<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1467.02,-62.5128C1517.13,-57.1834 1571.96,-51.3518 1622.5,-45.9776\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1629.6,-45.2224 1622.97,-49.0951 1626.12,-45.5926 1622.64,-45.9628 1622.64,-45.9628 1622.64,-45.9628 1626.12,-45.5926 1622.3,-42.8304 1629.6,-45.2224 1629.6,-45.2224\"/>\n",
"</g>\n",
"<!-- 6&#45;&gt;6 -->\n",
"<g id=\"edge14\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1709.05,-285.787C1701.35,-296.536 1732.72,-305.74 1803.17,-305.74 1857.1,-305.74 1888.13,-300.345 1896.25,-292.992\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1897.28,-285.787 1899.41,-293.16 1896.78,-289.252 1896.29,-292.717 1896.29,-292.717 1896.29,-292.717 1896.78,-289.252 1893.17,-292.275 1897.28,-285.787 1897.28,-285.787\"/>\n",
"</g>\n",
"<!-- 10 -->\n",
"<g id=\"node12\" class=\"node\"><title>10</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"2312.93\" cy=\"-224.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-228.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=1</text>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-213.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 7&#45;&gt;10 -->\n",
"<g id=\"edge15\" class=\"edge\"><title>7&#45;&gt;10</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2004.48,-203.072C2037.37,-205.404 2071.51,-207.825 2104.56,-210.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2111.6,-210.667 2104.39,-213.314 2108.11,-210.419 2104.62,-210.172 2104.62,-210.172 2104.62,-210.172 2108.11,-210.419 2104.84,-207.03 2111.6,-210.667 2111.6,-210.667\"/>\n",
"</g>\n",
"<!-- 11 -->\n",
"<g id=\"node13\" class=\"node\"><title>11</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"2312.93\" cy=\"-152.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-156.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=2</text>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-141.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
"</g>\n",
"<!-- 7&#45;&gt;11 -->\n",
"<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;11</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2004.48,-174.668C2037.37,-172.336 2071.51,-169.915 2104.56,-167.572\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2111.6,-167.073 2104.84,-170.71 2108.11,-167.321 2104.62,-167.568 2104.62,-167.568 2104.62,-167.568 2108.11,-167.321 2104.39,-164.426 2111.6,-167.073 2111.6,-167.073\"/>\n",
"</g>\n",
"<!-- 8&#45;&gt;11 -->\n",
"<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;11</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2004.48,-131.072C2037.37,-133.404 2071.51,-135.825 2104.56,-138.168\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2111.6,-138.667 2104.39,-141.314 2108.11,-138.419 2104.62,-138.172 2104.62,-138.172 2104.62,-138.172 2108.11,-138.419 2104.84,-135.03 2111.6,-138.667 2111.6,-138.667\"/>\n",
"</g>\n",
"<!-- 12 -->\n",
"<g id=\"node14\" class=\"node\"><title>12</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"2312.93\" cy=\"-62.8701\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-66.6701\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=3</text>\n",
"<text text-anchor=\"middle\" x=\"2312.93\" y=\"-51.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 8&#45;&gt;12 -->\n",
"<g id=\"edge18\" class=\"edge\"><title>8&#45;&gt;12</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1976.78,-98.5128C2026.89,-93.1834 2081.73,-87.3518 2132.26,-81.9776\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2139.36,-81.2224 2132.73,-85.0951 2135.88,-81.5926 2132.4,-81.9628 2132.4,-81.9628 2132.4,-81.9628 2135.88,-81.5926 2132.07,-78.8304 2139.36,-81.2224 2139.36,-81.2224\"/>\n",
"</g>\n",
"<!-- 9&#45;&gt;9 -->\n",
"<g id=\"edge19\" class=\"edge\"><title>9&#45;&gt;9</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1709.05,-51.7868C1701.35,-62.5364 1732.72,-71.7401 1803.17,-71.7401 1857.1,-71.7401 1888.13,-66.3451 1896.25,-58.9918\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"1897.28,-51.7868 1899.41,-59.1598 1896.78,-55.2521 1896.29,-58.7174 1896.29,-58.7174 1896.29,-58.7174 1896.78,-55.2521 1893.17,-58.2751 1897.28,-51.7868 1897.28,-51.7868\"/>\n",
"</g>\n",
"<!-- 10&#45;&gt;10 -->\n",
"<g id=\"edge20\" class=\"edge\"><title>10&#45;&gt;10</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2218.82,-249.787C2211.11,-260.536 2242.48,-269.74 2312.93,-269.74 2366.86,-269.74 2397.89,-264.345 2406.02,-256.992\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2407.04,-249.787 2409.17,-257.16 2406.55,-253.252 2406.05,-256.717 2406.05,-256.717 2406.05,-256.717 2406.55,-253.252 2402.94,-256.275 2407.04,-249.787 2407.04,-249.787\"/>\n",
"</g>\n",
"<!-- 13 -->\n",
"<g id=\"node15\" class=\"node\"><title>13</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"2822.69\" cy=\"-197.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"2822.69\" y=\"-201.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=2</text>\n",
"<text text-anchor=\"middle\" x=\"2822.69\" y=\"-186.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 11&#45;&gt;13 -->\n",
"<g id=\"edge21\" class=\"edge\"><title>11&#45;&gt;13</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2500.12,-169.371C2541.94,-173.078 2586.41,-177.019 2628.51,-180.75\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2635.52,-181.371 2628.27,-183.891 2632.04,-181.062 2628.55,-180.753 2628.55,-180.753 2628.55,-180.753 2632.04,-181.062 2628.83,-177.615 2635.52,-181.371 2635.52,-181.371\"/>\n",
"</g>\n",
"<!-- 14 -->\n",
"<g id=\"node16\" class=\"node\"><title>14</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"2822.69\" cy=\"-107.87\" rx=\"236.762\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"middle\" x=\"2822.69\" y=\"-111.67\" font-family=\"Lato\" font-size=\"14.00\">_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=3</text>\n",
"<text text-anchor=\"middle\" x=\"2822.69\" y=\"-96.6701\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
"</g>\n",
"<!-- 11&#45;&gt;14 -->\n",
"<g id=\"edge22\" class=\"edge\"><title>11&#45;&gt;14</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2500.12,-136.369C2541.94,-132.663 2586.41,-128.721 2628.51,-124.99\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2635.52,-124.369 2628.83,-128.125 2632.04,-124.678 2628.55,-124.987 2628.55,-124.987 2628.55,-124.987 2632.04,-124.678 2628.27,-121.849 2635.52,-124.369 2635.52,-124.369\"/>\n",
"</g>\n",
"<!-- 12&#45;&gt;12 -->\n",
"<g id=\"edge23\" class=\"edge\"><title>12&#45;&gt;12</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2218.82,-87.7868C2211.11,-98.5364 2242.48,-107.74 2312.93,-107.74 2366.86,-107.74 2397.89,-102.345 2406.02,-94.9918\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2407.04,-87.7868 2409.17,-95.1598 2406.55,-91.2521 2406.05,-94.7174 2406.05,-94.7174 2406.05,-94.7174 2406.55,-91.2521 2402.94,-94.2751 2407.04,-87.7868 2407.04,-87.7868\"/>\n",
"</g>\n",
"<!-- 13&#45;&gt;13 -->\n",
"<g id=\"edge24\" class=\"edge\"><title>13&#45;&gt;13</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2728.58,-222.787C2720.87,-233.536 2752.24,-242.74 2822.69,-242.74 2876.62,-242.74 2907.65,-237.345 2915.78,-229.992\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2916.8,-222.787 2918.93,-230.16 2916.31,-226.252 2915.82,-229.717 2915.82,-229.717 2915.82,-229.717 2916.31,-226.252 2912.7,-229.275 2916.8,-222.787 2916.8,-222.787\"/>\n",
"</g>\n",
"<!-- 14&#45;&gt;14 -->\n",
"<g id=\"edge25\" class=\"edge\"><title>14&#45;&gt;14</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2728.58,-132.787C2720.87,-143.536 2752.24,-152.74 2822.69,-152.74 2876.62,-152.74 2907.65,-147.345 2915.78,-139.992\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"2916.8,-132.787 2918.93,-140.16 2916.31,-136.252 2915.82,-139.717 2915.82,-139.717 2915.82,-139.717 2916.31,-136.252 2912.7,-139.275 2916.8,-132.787 2916.8,-132.787\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' 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": {}
}
]
}