Commit 186d2063 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent aeb05f0f
Pipeline #31251 passed with stages
in 115 minutes and 12 seconds
// -*- 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')
......
......@@ -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()
......
%% Cell type:code id: tags:
``` python
import spot
import spot.ltsmin
# The following line causes the notebook to exit with 77 if spins is not
# installed, therefore skipping this test in the test suite.
spot.ltsmin.require('spins')
spot.setup()
```
%% Cell type:markdown id: tags:
There are two ways to load a Promela model: from a file or from a cell.
Loading from a cell
-------------------
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 id: tags:
``` python
%%pml model
active proctype P() {
int a = 0;
int b = 0;
x: if
:: d_step {a < 3 && b < 3; a = a + 1; } goto x;
:: d_step {a < 3 && b < 3; b = b + 1; } goto x;
fi;
}
```
%% Output
SpinS Promela Compiler - version 1.1 (3-Feb-2015)
(C) University of Twente, Formal Methods and Tools group
Parsing tmpfkmh8g4r.pml...
Parsing tmpfkmh8g4r.pml done (0.0 sec)
Parsing tmprn9_nun3.pml...
Parsing tmprn9_nun3.pml done (0.1 sec)
Optimizing graphs...
StateMerging changed 0 states/transitions.
RemoveUselessActions changed 2 states/transitions.
RemoveUselessGotos changed 2 states/transitions.
RenumberAll changed 1 states/transitions.
Optimization done (0.0 sec)
Generating next-state function ...
Instantiating processes
Statically binding references
Creating transitions
Generating next-state function done (0.0 sec)
Creating state vector
Creating state labels
Generating transitions/state dependency matrices (2 / 3 slots) ...
[.......... ]
[.................... ]
[.............................. ]
[........................................ ]
[..................................................]
Found 5 / 15 ( 33.3%) Guard/slot reads
[......................... ]
[..................................................]
Found 6 / 6 (100.0%) Transition/slot tests
[........ ]
[................ ]
[......................... ]
[................................. ]
[......................................... ]
[..................................................]
Found 2, 4, 4 / 18 ( 11.1%, 22.2%, 22.2%) Actions/slot r,W,w
[......................... ]
[..................................................]
Found 2, 4, 4 / 6 ( 33.3%, 66.7%, 66.7%) Atomics/slot r,W,w
[......................... ]
[..................................................]
Found 6, 4, 4 / 6 (100.0%, 66.7%, 66.7%) Transition/slot r,W,w
Generating transition/state dependency matrices done (0.0 sec)
Generating guard dependency matrices (5 guards) ...
[.... ]
[........ ]
[............ ]
[................ ]
[.................... ]
[......................... ]
[............................. ]
[................................. ]
[..................................... ]
[......................................... ]
Found 3 / 12 ( 25.0%) Guard/guard dependencies
[..... ]
[.......... ]
[............... ]
[.................... ]
[......................... ]
[.............................. ]
[................................... ]
[........................................ ]
[............................................. ]
[..................................................]
Found 8 / 10 ( 80.0%) Transition/guard writes
Found 4 / 4 (100.0%) Transition/transition writes
[.... ]
[........ ]
[............ ]
[................ ]
[.................... ]
[......................... ]
[............................. ]
[................................. ]
[..................................... ]
[......................................... ]
Found 2 / 12 ( 16.7%) !MCE guards
[......................... ]
Found 1 / 2 ( 50.0%) !MCE transitions
[.. ]
[.... ]
[...... ]
[........ ]
[.......... ]
[............ ]
[.............. ]
[................ ]
[.................. ]
[.................... ]
[...................... ]
[........................ ]
[.......................... ]
[............................ ]
[.............................. ]
[................................ ]
[.................................. ]
[.................................... ]
[...................................... ]
[........................................ ]
[.......................................... ]
[............................................ ]
[.............................................. ]
[................................................ ]
[..................................................]
Found 7 / 25 ( 28.0%) !ICE guards
[..... ]
[.......... ]
[............... ]
[.................... ]
[......................... ]
[.............................. ]
[................................... ]
[........................................ ]
[............................................. ]
[..................................................]
Found 10 / 10 (100.0%) !NES guards
[............ ]
[......................... ]
[..................................... ]
[..................................................]
Found 4 / 4 (100.0%) !NES transitions
[..... ]
[.......... ]
[............... ]
[.................... ]
[......................... ]
[.............................. ]
[................................... ]
[........................................ ]
[............................................. ]
[..................................................]
Found 8 / 10 ( 80.0%) !NDS guards
[..... ]
[.......... ]
[............... ]
[.................... ]
[......................... ]
[.............................. ]
[................................... ]
[........................................ ]
[............................................. ]
[..................................................]
Found 0 / 10 ( 0.0%) MDS guards
[..... ]
[.......... ]
[............... ]
[.................... ]
[......................... ]
[.............................. ]
[................................... ]
[........................................ ]
[............................................. ]
[..................................................]
Found 4 / 10 ( 40.0%) MES guards
[............ ]
[......................... ]
[..................................... ]
[..................................................]
Found 0 / 4 ( 0.0%) !NDS transitions
[......................... ]
Found 0 / 2 ( 0.0%) !DNA transitions
[......................... ]
[..................................................]
[..................................................]
Found 2 / 2 (100.0%) Commuting actions
Generating guard dependency matrices done (0.0 sec)
Written C code to /home/adl/git/spot/tests/python/tmpfkmh8g4r.pml.spins.c
Compiled C code to PINS library tmpfkmh8g4r.pml.spins
Written C code to /home/adl/git/spot/tests/python/tmprn9_nun3.pml.spins.c
Compiled C code to PINS library tmprn9_nun3.pml.spins
%% Cell type:markdown id: tags:
Yes, the `spins` compiler is quite verbose. Printing the resulting `model` object will show information about the variables in that model.
%% Cell type:code id: tags:
``` python
model
```
%% Output
ltsmin model with the following variables:
P_0._pc: pc
P_0.a: int
P_0.b: int
%% Cell type:markdown id: tags:
To instantiate a Kripke structure, one should provide a list of atomic proposition to observe.
%% Cell type:code id: tags:
``` python
k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k
```
%% Output