From 186d2063021aed079d0f2b3986819d6f958e87f2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Nov 2021 23:37:08 +0100 Subject: [PATCH] ltsmin-pml: work around newer jupyter versions Newer Jupyter version are able to capture the system's stdout and stderr to display it in the notebook. This is done asynchronously, with a thread polling those file descriptor. While this will help us debug (finaly we can see the tracing code we put in C++) this causes two issues for testing. One is the asynchronous behaviour, which makes it very hard to reproduce notebooks. The second issue is that older version of Jupyter used to hide some of the prints from the notebook, so it is hard to accommodate both. In the case of the ltsmin-pml notebook, loading the PML file from a filename used to trigger a compilation silently (with output on the console, but not in the notebook). The newer version had the output of that compilation spread into two cells. * python/spot/ltsmin.i: Work around the issue by triggering the compilation from Python, and capturing its output explicitly, so it work with all Jupyter versions. Also adjust to use the more recent and simpler subprocess.run() interface, available since Python 3.5. * tests/python/ltsmin-pml.ipynb: Adjust expected output. * tests/python/ipnbdoctest.py (canonicalize): Adjust patterns. --- python/spot/ltsmin.i | 46 +++---- tests/python/ipnbdoctest.py | 7 +- tests/python/ltsmin-pml.ipynb | 232 +++++++++++----------------------- 3 files changed, 103 insertions(+), 182 deletions(-) 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,