alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
6176 commits 6 branches 0 tags 36 MiB
Commit graph

55 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
a31793960f * tests/ltsmin/modelcheck.cc: Typo when printing accepting run. 2016-02-09 14:49:28 +01:00
Alexandre Duret-Lutz
22345d0c67 rename parse_print_test as kripkecat 
Fixes #135.

* tests/core/parse_print_test.cc: Rename as...
* tests/core/kripkecat.cc: ... this.
* tests/Makefile.am, tests/core/.gitignore, tests/core/kripke.test,
tests/ltsmin/kripke.test: Adjust.
 2016-02-03 21:19:30 +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
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
ddc424f5a3 move ltsmin tests to tests/ltsmin/ 
* spot/ltsmin/defs.in: Delete.
* spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve,
spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm,
spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test,
spot/ltsmin/finite2.test, spot/ltsmin/kripke.test,
spot/ltsmin/modelcheck.cc: Move...
* tests/ltsmin/: ... here.
* spot/ltsmin/README: Point to tests/ltsmin/README.
* README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore,
tests/Makefile.am, tests/core/defs.in: Adjust.
 2016-01-05 11:52:24 +01:00