- 15 Jan, 2016 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 14 Jan, 2016 3 commits
-
-
Alexandre Duret-Lutz authored
* tests/Makefile.am (distclean-local): Erase python/core.
-
Alexandre Duret-Lutz authored
Alexandre Lewkowicz reported a case where complete() would peek an existing state that is accepting, and wrongly use it as a sink. * spot/twaalgos/complete.cc: Fix the function. * tests/core/complete.test: Add two more tests. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
* spot/parseaut/parseaut.yy: Here. * tests/core/parseaut.test: Test it. * NEWS: Mention it.
-
- 13 Jan, 2016 2 commits
-
-
Alexandre Duret-Lutz authored
* spot/twa/twa.hh: Store property bits as trivals. * NEWS: Mention the change. * spot/parseaut/parseaut.yy, spot/twaalgos/are_isomorphic.cc, spot/twaalgos/complete.cc, spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/lbtt.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/postproc.cc, spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc, spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh, spot/twaalgos/totgba.cc, tests/core/ikwiad.cc, tests/python/product.ipynb, tests/python/remfin.py: Adjust. * doc/org/hoa.org, doc/org/tut21.org: Update documentation.
-
Alexandre Duret-Lutz authored
* spot/misc/trival.hh: New file. * spot/misc/Makefile.am: Add it. * python/spot_impl.i: Add Python bindings. * tests/core/trival.cc, tests/core/trival.test, tests/python/trival.py: New files, testing it. * tests/Makefile.am: Add them.
-
- 12 Jan, 2016 1 commit
-
-
Etienne Renault authored
* spot/twa/twagraph.cc, spot/twa/twagraph.hh, tests/core/tgbagraph.test, tests/core/twagraph.cc, NEWS: here.
-
- 10 Jan, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
Fixes #129. * spot/twa/twa.cc (~twa): call unregister_all_my_variables() * spot/twa/twagraph.hh, spot/twa/twaproduct.cc, spot/twaalgos/stutter.cc: Simplify. * NEWS: Mention the change.
-
- 08 Jan, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
* bin/common_aoutput.cc: Make HOA the default output. * NEWS: Mention this. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org, tests/core/dstar.test, tests/core/ltldo2.test, tests/core/monitor.test, tests/python/piperead.ipynb: Adjust.
-
- 06 Jan, 2016 8 commits
-
-
Alexandre Duret-Lutz authored
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_setup.cc: Implement it. * NEWS, bin/man/spot-x.x: Document it. * tests/core/readsave.test: Test it.
-
Alexandre Duret-Lutz authored
* bin/common_aoutput.cc: Here. * NEWS, doc/org/oaut.org: Mention it. * tests/core/readsave.test: Use it once.
-
Alexandre Duret-Lutz authored
This is so that we can have -d as an alias for --dot everywhere. * bin/randaut.cc: Rename -d as -e. * NEWS: Mention the change. * doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org, tests/core/parseaut.test, tests/core/readsave.test: Adjust.
-
Alexandre Duret-Lutz authored
* doc/org/.dir-locals.el.in, doc/org/init.el.in: bin/ is no longer in spot/.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* tests/Makefile.am (TESTS_python): Define conditionally.
-
- 05 Jan, 2016 8 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* tests/Makefile.am (distclean-local): Here.
-
Alexandre Duret-Lutz authored
* spot/sanity/: Move ... * tests/sanity/: ... here. * spot/sanity/Makefile.am: Merge with... * tests/Makefile.am: ... this. * tests/run.in: Learn to run perl tests. * README, configure.ac, spot/Makefile.am: Adjust. * spot/tl/mark.hh: Add missing SPOT_API detected by fixed private.test. * spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Move... * spot/priv/weight.cc, spot/priv/weight.hh: ... here, as suggested by fixed private.test. * spot/twaalgos/tau03opt.cc, spot/twaalgos/Makefile.am, spot/priv/Makefile.am: Adjust.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
-
- 04 Jan, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
* tests/: Rename as... * tests/core/: ... this. * python/tests/: Rename as... * tests/python/: ... this. * python/tests/run.in: Move as... * tests/run.in: This, and adjust. * tests/Makefile.am: Adjust to run both core and python tests. * configure.ac, README, debian/python3-spot.examples, debian/rules, doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am, spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
-
- 28 Dec, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 27 Dec, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* spot/bin/: Move... * bin/: ... here. * spot/tests/: Move... * tests/: ... here. * Makefile.am, README, bench/stutter/Makefile.am, bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am, configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am, spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in: Adjust.
-
- 26 Dec, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* python/tests/ipnbdoctest.py: Simply ignore %timeit blocks.
-
- 25 Dec, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* spot-if/ltsmin/: Rename as... * spot/ltsmin/: ... this. * spot-if/: Delete. * Makefile.am, NEWS, README, configure.ac, debian/libspot-dev.install, doc/Doxyfile.in, spot/Makefile.am, spot/sanity/80columns.test, spot/sanity/style.test: Adjust.
-
Alexandre Duret-Lutz authored
* wrap/python/: Rename to... * python/: ... this. * wrap/: Delete. * Makefile.am, README, configure.ac, debian/python3-spot.examples, debian/rules, doc/org/.dir-locals.el.in, doc/org/init.el.in, spot/sanity/ipynb.test: Adjust.
-
- 24 Dec, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* wrap/python/tests/product.ipynb: New file. * wrap/python/tests/Makefile.am, doc/org/tut.org: Add it. * wrap/python/tests/ipnbdoctest.py: Ignore %timeit results. * wrap/python/spot_impl.i: Add bindings for set_state_names()/get_state_names(). * spot/twaalgos/product.cc: Fix computation of properties. * doc/org/hoa.org: Name. * NEWS: Update.
-
Alexandre Duret-Lutz authored
Calling register_ap() with same atomic proposition several time, for instance via copy_ap() in a product, would create duplicate atomic propositions. This fix will be exercised by the next patch. * spot/twa/twa.hh: Here. * spot/twaalgos/compsusp.cc, spot/twaalgos/ltl2taa.cc: Fix to correctly register atomic propositions. * NEWS: Mention it.
-
- 18 Dec, 2015 5 commits
-
-
Alexandre Duret-Lutz authored
It is already in acc_cond::acc_code::generalized_buchi() along with all other acceptance condition constructors. * spot/twa/acc.hh (acc_cond::generalized_buchi): Remove. * spot/tests/ikwiad.cc, spot/twaalgos/postproc.cc: Adjust.
-
Alexandre Duret-Lutz authored
* spot/twa/acc.hh, spot/twa/acc.cc (parse_acc_code): Rename as... (acc_cond::acc_code): ... this, making it a lot easier to build acceptance conditions from strings. * NEWS: Mention the change. * spot/twaalgos/dtwasat.cc, spot/bin/randaut.cc, spot/tests/acc.cc: Adjust. * wrap/python/tests/acc_cond.ipynb, wrap/python/tests/accparse.ipynb, wrap/python/tests/accparse2.py: Simplify, but not completely to exercise all variants. * wrap/python/spot_impl.i: Make acc_code's constructor implicit.
-
Alexandre Duret-Lutz authored
* spot/twa/acc.hh: Here. * wrap/python/spot_impl.i: Adjust for the strange return type of unsat_mark(). * wrap/python/tests/acc_cond.ipynb: Augment.
-
Alexandre Duret-Lutz authored
* wrap/python/Makefile.am: Use more modern swig flags.
-
Alexandre Duret-Lutz authored
* wrap/python/spot_impl.i: Here. * wrap/python/tests/acc_cond.ipynb: Document it. * spot/twa/acc.cc (is_parity): Always initialize max.
-