Commit graph

10 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
3034e8fcc3 python: render <svg> via _repr_html_
Work around a recent decision in Jupyter Lab and Notebook to render
<svg> is inline <img>, breaking tooltips or text selection.

(Rerendering all notebooks was painful.)

* NEWS: Mention the change.
* python/spot/__init__.py: Add a _repr_html_ method to all
classes that had a _repr_svg_.  It seems Jupyter will use
_repr_html_ by default.
* python/spot/jupyter.py: SVG replace the _repr_svg_ method
by a _repr_html.
* tests/python/_altscc.ipynb, tests/python/_autparserr.ipynb,
tests/python/_aux.ipynb, tests/python/_mealy.ipynb,
tests/python/_partitioned_relabel.ipynb,
tests/python/_product_susp.ipynb, tests/python/_product_weak.ipynb,
tests/python/_synthesis.ipynb, tests/python/aliases.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb,
tests/python/automata.ipynb, tests/python/cav22-figs.ipynb,
tests/python/contains.ipynb, tests/python/decompose.ipynb,
tests/python/formulas.ipynb, tests/python/games.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/parity.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/satmin.ipynb,
tests/python/stutter-inv.ipynb, tests/python/synthesis.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb, tests/python/zlktree.ipynb: Update all
notebooks.
2024-02-09 15:06:07 +01:00
Alexandre Duret-Lutz
b36cee06a1 adjust to Swig 4.1.0
* python/spot/__init__.py: Add flatnested versions of some static
methods.
* spot/twa/acc.hh: Hide && version of & and |, causing trouble
to swig.
* tests/python/_synthesis.ipynb, tests/python/synthesis.ipynb:
Upgrade expected type names.
* tests/python/ipnbdoctest.py: Adjust for difference between 4.0 and
4.1.
2022-11-10 17:08:30 +01:00
Philipp Schlehuber-Caissier
c63c1796b9 Improve aiger INF encoding
the encoding cna be simplified to produce less gates
when high or low is True.

* spot/twaalgos/aiger.cc: Here
* tests/python/_synthesis.ipynb: Test
2022-09-21 17:28:04 +02:00
Philipp Schlehuber-Caissier
524edea8da Propagate colors in split_2step
Reduce the amount of uncolored transitions
after split_2step by trying to color the env transitions.
This is currently only supported for parity like
acceptance conditions.

* spot/twaalgos/game.cc: Determinizatio of "colored"
game can created trivial self-loops. Fix them
* spot/twaalgos/synthesis.cc: Here
* tests/core/ltlsynt.test,
tests/python/_synthesis.ipynb,
tests/python/games.ipynb,
tests/python/synthesis.ipynb,
tests/python/synthesis.py: New and adjusted tests
2022-04-07 21:21:06 +02:00
Philipp Schlehuber-Caissier
dfb75632ba Update merge_states
Current implementation of merge_states fails
on certain self-loops.
Updated implementation to take them into
account and use a hashbased implementation
to speed up calculations.
Moreover, merge_states() is now aware
of "state-player", just like defrag_states_

* spot/twa/twagraph.cc: Here
* spot/twaalgos/game.cc: Fix odd cycle for sink
* spot/twaalgos/synthesis.cc: Adapt split_det pipeline
* tests/python/_synthesis.ipynb: Tests
2022-04-07 17:42:14 +02:00
Philipp Schlehuber-Caissier
97fc3f6c0b Introduce simplify_mealy
Convenience function dispatching to
minimize_mealy and reduce_mealy.
Change tests accordingly

* spot/twaalgos/mealy_machine.cc,
  spot/twaalgos/mealy_machine.hh: Here
* bin/ltlsynt.cc: Use simplify
* spot/twaalgos/synthesis.cc,
  spot/twaalgos/synthesis.hh: Remove
 minimization, Update options
* tests/core/ltlsynt.test,
  tests/python/synthesis.ipynb,
  tests/python/_synthesis.ipynb: Adapt
2022-03-18 15:35:54 +01:00
Alexandre Duret-Lutz
8c33f959a3 hoa: add support for controllable-AP
* doc/spot.bib (perez.19.hoa): New entry.
* spot/parseaut/public.hh: Mention it.
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Learn to parse
the controllable-AP header.
* spot/twaalgos/hoa.cc: Print it.
* tests/core/ltlsynt.test, tests/core/parseaut.test,
tests/core/readsave.test, tests/python/_synthesis.ipynb,
tests/python/except.py, tests/python/games.ipynb,
tests/python/mealy.py, tests/python/synthesis.py: Adjust or augment
test cases.
2022-01-10 14:51:34 +01:00
philipp
7cefe30d97 Fixes #495
Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.

* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here
* tests/python/_synthesis.ipynb: Testing
2022-01-07 10:44:04 +01:00
philipp
4babe8db75 Fixing state reorder bug for mealy minimization
Isomorph but different machines were created
depending on ARM vs Intel

* spot/twaalgos/mealy_machine.cc: Fix here
* tests/python/_synthesis.ipynb: Test here
2021-12-10 12:48:09 +01:00
Philipp Schlehuber
5b6e2a210a Making solved game to mealy more flexible
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Solved game to mealy
now also supports the other mealy formats
* tests/python/_synthesis.ipynb: Test
* tests/Makefile.am: Test
2021-12-10 12:44:36 +01:00