Commit graph

8 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
af96cbca83 * tests/python/ltsmin.ipynb: Erase the model file. 2016-02-03 08:51:37 +01:00
Alexandre Duret-Lutz
02b5460b91 dot, hoa: default to "k" for kripke structure
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc: If a Kripke
structure is passed, automatically enable the "k" option.
* tests/core/parse_print_test.cc, tests/ltsmin/modelcheck.cc,
tests/python/ltsmin.ipynb: Remove the explicit use of "k".
* NEWS: Mention the change.
2016-02-01 22:12:13 +01:00
Alexandre Duret-Lutz
a9b4560f3d dot: add option "k"
Fixes #134.

* spot/twaalgos/dot.cc: Implement it.
* bin/common_aoutput.cc, spot/twaalgos/dot.hh, NEWS: Document it.
* tests/core/readsave.test, tests/python/ltsmin.ipynb: Test it.
2016-02-01 08:38:45 +01:00
Alexandre Duret-Lutz
b11c07b351 dot: add a <N option
* spot/twaalgos/dot.cc: Implement it.
* spot/taalgos/dot.cc: Ignore it.
* spot/twaalgos/copy.cc, spot/twaalgos/copy.hh: Add option
to limit the number of states.
* tests/python/ltsmin.ipynb: Improve test case.
* tests/Makefile.am: Cleanup the files generated by ltsmin.ipynb.
* python/spot/__init__.py (setup): Add a max_states argument
that default to 50.
* bin/common_aoutput.cc: Mention the <INT option.
* NEWS: Likewise.
2016-01-29 09:09:05 +01:00
Alexandre Duret-Lutz
4571d6dd3a copy: rewrite as a BFS without using reachiter
* spot/twaalgos/copy.hh: Trim includes.
* spot/twaalgos/copy.cc: Rewrite.
* tests/python/ltsmin.ipynb: Adjust.
2016-01-28 15:37:00 +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