diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 3eb051f3f..bd49c5a3f 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2017, 2019 Laboratoire de Recherche et +// Copyright (C) 2016-2017, 2019, 2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -61,8 +61,25 @@ import spot import spot.aux import sys import subprocess +import os.path +import re def load(filename): + # Compile promela model with Spins by end, even if it would be done in model.load, + # so we can capture the output of the compilation regardless of the Jupyter version. + # (Older Jupyter version to not send the output to the notebook, and newer versions + # do it asynchronously in a way that make testing quite hard.) + if filename.endswith('.pm') or filename.endswith('.pml') or filename.endswith('.prom'): + dst = os.path.basename(filename) + '.spins' + if not os.path.exists(dst) or (os.path.getmtime(dst) < os.path.getmtime(filename)): + p = subprocess.run(['spins', filename], stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + universal_newlines=True) + if p.stdout: print(re.sub('^\s*\[\.*\s*\]\n', '', p.stdout, + flags=re.MULTILINE), file=sys.stderr) + if p.stderr: print(p.stderr, file=sys.stderr) + p.check_returncode() + filename = dst return model.load(filename) @spot._extend(model) @@ -155,17 +172,13 @@ try: t.flush() try: - p = subprocess.Popen(['divine', 'compile', + p = subprocess.run(['divine', 'compile', '--ltsmin', t.name], - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, + capture_output=True, 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') + if p.stdout: print(p.stdout) + if p.stderr: print(p.stderr, file=sys.stderr) + p.check_returncode() self.shell.user_ns[line] = load(t.name + '2C') finally: spot.aux.rm_f(t.name + '.cpp') @@ -182,19 +195,8 @@ try: 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') + self.shell.user_ns[line] = load(t.name) finally: spot.aux.rm_f(t.name + '.spins.c') spot.aux.rm_f(t.name + '.spins') diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 5d2c57134..18da81cf8 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -93,7 +93,9 @@ def canonicalize(s, type, ignores): s = re.sub(r'Generated by graphviz version.*', 'VERSION', s) # remove Spins verbose output version - s = re.sub(r'SpinS Promela Compiler.*Compiled C .* to .*pml.spins', + s = re.sub(r'SpinS Promela Compiler.*Written C .* to .*pml.spins.c', + 'SpinS output', s, flags=re.DOTALL) + s = re.sub(r'Compiled C code to PINS .*pml.spins', 'SpinS output', s, flags=re.DOTALL) # %%file writes `Writing`, or `Overwriting` if the file exists. @@ -298,7 +300,8 @@ def test_notebook(ipynb): km = KernelManager() # Do not save the history to disk, as it can yield spurious lock errors. # See https://github.com/ipython/ipython/issues/2845 - km.start_kernel(extra_arguments=['--HistoryManager.hist_file=:memory:']) + km.start_kernel(extra_arguments=['--HistoryManager.hist_file=:memory:', + '--quiet']) kc = km.client() kc.start_channels() diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb index 2975e0938..120ab11f5 100644 --- a/tests/python/ltsmin-pml.ipynb +++ b/tests/python/ltsmin-pml.ipynb @@ -29,7 +29,9 @@ { "cell_type": "code", "execution_count": 2, - "metadata": {}, + "metadata": { + "scrolled": false + }, "outputs": [ { "name": "stderr", @@ -38,8 +40,8 @@ "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n", "(C) University of Twente, Formal Methods and Tools group\n", "\n", - "Parsing tmpfkmh8g4r.pml...\n", - "Parsing tmpfkmh8g4r.pml done (0.0 sec)\n", + "Parsing tmprn9_nun3.pml...\n", + "Parsing tmprn9_nun3.pml done (0.1 sec)\n", "\n", "Optimizing graphs...\n", " StateMerging changed 0 states/transitions.\n", @@ -57,176 +59,33 @@ "Creating state vector\n", "Creating state labels\n", "Generating transitions/state dependency matrices (2 / 3 slots) ... \n", - "\n", - " [.......... ]\n", - " [.................... ]\n", - " [.............................. ]\n", - " [........................................ ]\n", - " [..................................................]\n", " Found 5 / 15 ( 33.3%) Guard/slot reads \n", - "\n", - " [......................... ]\n", - " [..................................................]\n", " Found 6 / 6 (100.0%) Transition/slot tests \n", - "\n", - " [........ ]\n", - " [................ ]\n", - " [......................... ]\n", - " [................................. ]\n", - " [......................................... ]\n", - " [..................................................]\n", " Found 2, 4, 4 / 18 ( 11.1%, 22.2%, 22.2%) Actions/slot r,W,w \n", - "\n", - " [......................... ]\n", - " [..................................................]\n", " Found 2, 4, 4 / 6 ( 33.3%, 66.7%, 66.7%) Atomics/slot r,W,w \n", - "\n", - " [......................... ]\n", - " [..................................................]\n", " Found 6, 4, 4 / 6 (100.0%, 66.7%, 66.7%) Transition/slot r,W,w \n", "Generating transition/state dependency matrices done (0.0 sec)\n", "\n", "Generating guard dependency matrices (5 guards) ...\n", - "\n", - " [.... ]\n", - " [........ ]\n", - " [............ ]\n", - " [................ ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [............................. ]\n", - " [................................. ]\n", - " [..................................... ]\n", - " [......................................... ]\n", " Found 3 / 12 ( 25.0%) Guard/guard dependencies \n", - "\n", - " [..... ]\n", - " [.......... ]\n", - " [............... ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [.............................. ]\n", - " [................................... ]\n", - " [........................................ ]\n", - " [............................................. ]\n", - " [..................................................]\n", " Found 8 / 10 ( 80.0%) Transition/guard writes \n", "\n", " Found 4 / 4 (100.0%) Transition/transition writes \n", - "\n", - " [.... ]\n", - " [........ ]\n", - " [............ ]\n", - " [................ ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [............................. ]\n", - " [................................. ]\n", - " [..................................... ]\n", - " [......................................... ]\n", " Found 2 / 12 ( 16.7%) !MCE guards \n", - "\n", - " [......................... ]\n", " Found 1 / 2 ( 50.0%) !MCE transitions \n", - "\n", - " [.. ]\n", - " [.... ]\n", - " [...... ]\n", - " [........ ]\n", - " [.......... ]\n", - " [............ ]\n", - " [.............. ]\n", - " [................ ]\n", - " [.................. ]\n", - " [.................... ]\n", - " [...................... ]\n", - " [........................ ]\n", - " [.......................... ]\n", - " [............................ ]\n", - " [.............................. ]\n", - " [................................ ]\n", - " [.................................. ]\n", - " [.................................... ]\n", - " [...................................... ]\n", - " [........................................ ]\n", - " [.......................................... ]\n", - " [............................................ ]\n", - " [.............................................. ]\n", - " [................................................ ]\n", - " [..................................................]\n", " Found 7 / 25 ( 28.0%) !ICE guards \n", - "\n", - " [..... ]\n", - " [.......... ]\n", - " [............... ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [.............................. ]\n", - " [................................... ]\n", - " [........................................ ]\n", - " [............................................. ]\n", - " [..................................................]\n", " Found 10 / 10 (100.0%) !NES guards \n", - "\n", - " [............ ]\n", - " [......................... ]\n", - " [..................................... ]\n", - " [..................................................]\n", " Found 4 / 4 (100.0%) !NES transitions \n", - "\n", - " [..... ]\n", - " [.......... ]\n", - " [............... ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [.............................. ]\n", - " [................................... ]\n", - " [........................................ ]\n", - " [............................................. ]\n", - " [..................................................]\n", " Found 8 / 10 ( 80.0%) !NDS guards \n", - "\n", - " [..... ]\n", - " [.......... ]\n", - " [............... ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [.............................. ]\n", - " [................................... ]\n", - " [........................................ ]\n", - " [............................................. ]\n", - " [..................................................]\n", " Found 0 / 10 ( 0.0%) MDS guards \n", - "\n", - " [..... ]\n", - " [.......... ]\n", - " [............... ]\n", - " [.................... ]\n", - " [......................... ]\n", - " [.............................. ]\n", - " [................................... ]\n", - " [........................................ ]\n", - " [............................................. ]\n", - " [..................................................]\n", " Found 4 / 10 ( 40.0%) MES guards \n", - "\n", - " [............ ]\n", - " [......................... ]\n", - " [..................................... ]\n", - " [..................................................]\n", " Found 0 / 4 ( 0.0%) !NDS transitions \n", - "\n", - " [......................... ]\n", " Found 0 / 2 ( 0.0%) !DNA transitions \n", - "\n", - " [......................... ]\n", - " [..................................................]\n", - " [..................................................]\n", " Found 2 / 2 (100.0%) Commuting actions \n", "Generating guard dependency matrices done (0.0 sec)\n", "\n", - "Written C code to /home/adl/git/spot/tests/python/tmpfkmh8g4r.pml.spins.c\n", - "Compiled C code to PINS library tmpfkmh8g4r.pml.spins\n", + "Written C code to /home/adl/git/spot/tests/python/tmprn9_nun3.pml.spins.c\n", + "Compiled C code to PINS library tmprn9_nun3.pml.spins\n", "\n" ] } @@ -294,9 +153,9 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "t\n", "[all]\n", @@ -560,7 +419,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3030ca5150> >" + " *' at 0x7fb7d8049450> >" ] }, "execution_count": 4, @@ -929,9 +788,9 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "t\n", "[all]\n", @@ -1316,7 +1175,64 @@ "cell_type": "code", "execution_count": 9, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stderr", + "output_type": "stream", + "text": [ + "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n", + "(C) University of Twente, Formal Methods and Tools group\n", + "\n", + "Parsing test1.pml...\n", + "Parsing test1.pml done (0.0 sec)\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 (0.0 sec)\n", + "\n", + "Generating next-state function ...\n", + " Instantiating processes\n", + " Statically binding references\n", + " Creating transitions\n", + "Generating next-state function done (0.0 sec)\n", + "\n", + "Creating state vector\n", + "Creating state labels\n", + "Generating transitions/state dependency matrices (2 / 3 slots) ... \n", + " Found 5 / 15 ( 33.3%) Guard/slot reads \n", + " Found 6 / 6 (100.0%) Transition/slot tests \n", + " Found 2, 4, 4 / 18 ( 11.1%, 22.2%, 22.2%) Actions/slot r,W,w \n", + " Found 2, 4, 4 / 6 ( 33.3%, 66.7%, 66.7%) Atomics/slot r,W,w \n", + " Found 6, 4, 4 / 6 (100.0%, 66.7%, 66.7%) Transition/slot r,W,w \n", + "Generating transition/state dependency matrices done (0.0 sec)\n", + "\n", + "Generating guard dependency matrices (5 guards) ...\n", + " Found 3 / 12 ( 25.0%) Guard/guard dependencies \n", + " Found 8 / 10 ( 80.0%) Transition/guard writes \n", + "\n", + " Found 4 / 4 (100.0%) Transition/transition writes \n", + " Found 2 / 12 ( 16.7%) !MCE guards \n", + " Found 1 / 2 ( 50.0%) !MCE transitions \n", + " Found 7 / 25 ( 28.0%) !ICE guards \n", + " Found 10 / 10 (100.0%) !NES guards \n", + " Found 4 / 4 (100.0%) !NES transitions \n", + " Found 8 / 10 ( 80.0%) !NDS guards \n", + " Found 0 / 10 ( 0.0%) MDS guards \n", + " Found 4 / 10 ( 40.0%) MES guards \n", + " Found 0 / 4 ( 0.0%) !NDS transitions \n", + " Found 0 / 2 ( 0.0%) !DNA transitions \n", + " Found 2 / 2 (100.0%) Commuting actions \n", + "Generating guard dependency matrices done (0.0 sec)\n", + "\n", + "Written C code to /home/adl/git/spot/tests/python/test1.pml.spins.c\n", + "Compiled C code to PINS library test1.pml.spins\n", + "\n" + ] + } + ], "source": [ "model2 = spot.ltsmin.load('test1.pml')" ] @@ -1356,7 +1272,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -1370,7 +1286,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.9.2" } }, "nbformat": 4,