Commit graph

12 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
186d206302 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.
2021-11-15 23:37:08 +01:00
Alexandre Duret-Lutz
f8695e91f9 python: remove workaround for swig 2.0.2
* python/spot/gen.i, python/spot/impl.i, python/spot/ltsmin.i: Here.
2019-10-02 09:34:18 +02:00
Alexandre Duret-Lutz
d2e9515c10 skip divine tests when divine does not understand compile --help
Fixes #235, reported by Henrich Lauko.

* python/spot/ltsmin.i: Catch CalledProcessError.
* NEWS: Mention the bug.
* THANKS: Add Henrich.
2017-02-28 17:02:06 +01:00
Etienne Renault
8a8fcf2ac1 spot.ltsmin: fix errors on Darwin
* NEWS, python/spot/ltsmin.i: here.
2016-10-10 20:11:40 +02:00
Alexandre Duret-Lutz
e37f62dc75 python: have %%dve and %%pml honor SPOT_TMPDIR and TMPDIR
* python/spot/aux.py (tmpdir): New context manager.
* python/spot/ltsmin.i: Use it for the two magics.
* NEWS: Mention this.
2016-07-19 14:23:27 +02:00
Alexandre Duret-Lutz
272daf62fc python: add a %%pml magic
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.
2016-06-12 12:53:55 +02:00
Alexandre Duret-Lutz
901f287032 python: add prints for atomic_prop_set
Fixes #159.

* python/spot/ltsmin.i: Here.
* python/spot/impl.i: Disable duplicate instantiation.
* tests/python/ltsmin.ipynb: Test it.
2016-04-08 23:01:07 +02:00
Alexandre Duret-Lutz
9692d734a9 cleanup ltsmin bindings
* python/spot/aux.py (rm_f): new function.
* python/spot/ltsmin.i: Replace the %require magic by a simple function.
Rewrite the %%dve magic.
* tests/python/otfcrash.py: Simplify using spot.ltsmin.require()
* tests/python/ltsmin.ipynb: Likewise, also add more text for the
documentation.
* NEWS: Adjust.
2016-02-16 19:08:28 +01:00
Etienne Renault
091251b5b7 Provide support for %dve and %require
* NEWS, python/spot/ltsmin.i,
tests/python/ltsmin.ipynb: Here.
2016-02-15 09:08:37 +01:00
Alexandre Duret-Lutz
db1e842a67 ltsmin: add accessors for variable names and types
* spot/ltsmin/ltsmin.hh, spot/ltsmin/ltsmin.cc: Expose more of the
ltsmin interface.
* python/spot/ltsmin.i: Add some helper functions on top of this
new interface.
* tests/python/ltsmin.ipynb: Test them.
* NEWS: Mention it.
2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
907b72fbfb ltsmin: implement a two-step loading
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: Split load_ltsmin() into
ltsmin_model::load() and ltsmin_model::kripke().  Report errors using
exceptions instead of on std::cerr.
* python/spot/ltsmin.i: Deal with exceptions.
* tests/ltsmin/modelcheck.cc, tests/python/ltsmin.ipynb: Adjust.
2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
5a9b0aa1c1 python: add bindings for ltsmin
* python/spot/ltsmin.i: New file.
* python/Makefile.am: Add it.
* python/spot/impl.i: Add bindings for kripke and fair_kripke.
* tests/python/ltsmin.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Make it possible for notebook
to exit(77).
* debian/control: Make the Python package dependent
on libspotltsmin0.
* python/spot/__init__.py: Typo.
2016-01-26 19:20:53 +01:00