alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

move parts of games.ipynb into synthesis.ipynb

Browse source 
* tests/python/synthesis.ipynb: New file, with bits removed from...
* tests/python/games.ipynb: ... here.
* tests/Makefile.am: Add synthesis.ipynb.
* NEWS, doc/org/tut.org: Mention the new notebook.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-07 10:48:02 +02:00
parent 7bc2c31043
commit 0ec1ee6de3
5 changed files with 3595 additions and 3056 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -289,6 +289,7 @@ New in spot 2.9.8.dev (not yet released)
https://spot.lrde.epita.fr/tut40.html for examples. https://spot.lrde.epita.fr/tut40.html for examples.
- Bindings for functions related to syntethis and aig-circuits. - Bindings for functions related to syntethis and aig-circuits.
See https://spot.lrde.epita.fr/ipynb/synthesis.html
- spot::twa::prop_set was previously abstent from the Python - spot::twa::prop_set was previously abstent from the Python
bindings, making it impossible to call make_twa_graph() for copying bindings, making it impossible to call make_twa_graph() for copying

1
doc/org/tut.org
View file

@ -74,6 +74,7 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata
in Python in Python
- [[https://spot.lrde.epita.fr/ipynb/games.html][=games.ipynb=]] illustrates support for games - [[https://spot.lrde.epita.fr/ipynb/games.html][=games.ipynb=]] illustrates support for games
- [[https://spot.lrde.epita.fr/ipynb/synthesis.html][=synthesis.ipynb=]] illustrates support for game-based LTL reactive synthesis
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
in Python in Python
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]

1
tests/Makefile.am
View file

@ -370,6 +370,7 @@ TESTS_ipython = \
python/randltl.ipynb \ python/randltl.ipynb \
python/satmin.ipynb \ python/satmin.ipynb \
python/stutter-inv.ipynb \ python/stutter-inv.ipynb \
python/synthesis.ipynb \
python/testingaut.ipynb \ python/testingaut.ipynb \
python/twagraph-internals.ipynb \ python/twagraph-internals.ipynb \
python/word.ipynb \ python/word.ipynb \

3075
tests/python/games.ipynb
View file

File diff suppressed because it is too large Load diff

3573
tests/python/synthesis.ipynb Normal file
View file

File diff suppressed because it is too large Load diff