- 16 Jul, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
Reported by Joachim Klein. * doc/org/ltl2tgba.org: Broken link. * doc/org/ltlcross.org: Two typos.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc: Here.
-
Alexandre Duret-Lutz authored
* src/twaalgos/remfin.cc: Here.
-
- 10 Jul, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* src/twaalgos/totgba.hh, src/twaalgos/totgba.cc: Implement the new function. * NEWS: Mention this new function. * src/bin/man/spot-x.x: Document SPOT_STREETT_CONV_MIN. * src/tests/ltl2dstar4.test: Add tests. * src/tests/Makefile.am: Add it. * src/bin/autfilt.cc: Do do call remove_fin explicitely when --tgba is used, let the postprocessor do it. * src/twa/acc.hh: Add shift operators for acceptance marks. * src/twaalgos/remfin.cc: Use the new algorithm. * src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Add a new method to supply the acceptance sets visited by an SCC.
-
- 09 Jul, 2015 5 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/twaalgos/sccinfo.cc: Here.
-
Alexandre Duret-Lutz authored
The command in #96 now takes 1min 16s. * src/twaalgos/sccinfo.cc: Only gather successor SCCs when popping an SCC. * wrap/python/tests/automata.ipynb: Adjust.
-
Alexandre Duret-Lutz authored
Suggested by Etienne. The command in #96 now takes 9min 35s. * src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Here.
-
Alexandre Duret-Lutz authored
They are unused. * src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Do not keep track of conditions between two SCCs. * src/twaalgos/minimize.cc, src/twaalgos/ltl2tgba_fm.cc: Adjust.
-
- 07 Jul, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* NEWS, doc/org/install.org: Here.
-
- 06 Jul, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
Fixes #94. * iface/ltsmin/Makefile.am: Install libspotltsmin. * debian/libspotltlsmin0.install: New file. * debian/control (libspotltlsmin0): New package. * debian/libspot-dev.install: Add the linspotltlsmin0.so symlink.
-
Alexandre Duret-Lutz authored
* debian/control (libbddx-dev, libbddx0, libspot0): New packages. (libspot-dev): Make it "Architecture: any". * debian/libspot-dev.install: Include the .so symlink. * debian/spot.install: Remove the libraries. * debian/libbddx-dev.install, debian/libbddx0.install, debian/libspot0.install: New files. * Makefile.am: Distribute them.
-
- 01 Jul, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 30 Jun, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
This helps diagnosing #96. * src/bin/ltlcross.cc (process_formula): Print product sizes if --verbose.
-
Alexandre Duret-Lutz authored
Fixes #95, reported by Vitus Lam. * m4/pypath.m4: Check for Python.h and print some advice if missing. * NEWS: Mention this. * THANKS: Add Vitus.
-
Alexandre Duret-Lutz authored
* src/twaalgos/sccfilter.cc (acc_filter_some, acc_filter_all): Merge into... (acc_filter_mask): ... this single parametrized class, and only remove sets that are only used as Inf. * src/twa/acc.hh: Add missing operator~. * src/tests/sccsimpl.test: Add test case. * src/tests/sccdot.test: Adjust. * NEWS: Mention the bug.
-
- 23 Jun, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
* src/ltlast/bunop.cc: Fix detection of f[:*2] as siPSL if f is siPSL * src/tests/kind.test: Test it. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
-
- 22 Jun, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* doc/org/spot.css: Improve TOC. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Specify viewport.
-
- 21 Jun, 2015 4 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/misc/bareword.hh, src/misc/bitvect.hh, src/misc/escape.hh, src/misc/hashfunc.hh, src/misc/intvcmp2.hh, src/misc/intvcomp.hh, src/misc/random.hh, src/misc/timer.hh, src/misc/tmpfile.hh: Use ingroup rather than addtogroup.
-
- 20 Jun, 2015 5 commits
-
-
Alexandre Duret-Lutz authored
Fixes #53. * wrap/python/ajax/spotcgi.in: Do that. * wrap/python/ajax/trans.html: Fixup jquery code to avoid looping over tabs. * wrap/python/spot_impl.i: Wrap the automaton relabeling code. * NEWS: Update.
-
Alexandre Duret-Lutz authored
* wrap/python/ajax/spotcgi.in: Here.
-
Alexandre Duret-Lutz authored
* doc/tl/tl.tex, src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Remove is_eltl_formula(). * src/tests/kind.test: Adjust.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 19 Jun, 2015 6 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* doc/org/satmin.org: Fix export. We need both 'results: silent' and 'exports: both' for the code to be run and shown.
-
Alexandre Duret-Lutz authored
Report from Joachim Klein. * doc/tl/Makefile.am (mostlyclean-local): Rename as... (maintainer-clean-local): ... this.
-
Alexandre Duret-Lutz authored
* doc/org/satmin.org: Do not use ":export code" on code that must be run on export.
-
Alexandre Duret-Lutz authored
* doc/Makefile.am (org): Remove the useless temporary directory.
-
- 18 Jun, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* doc/Makefile.am (org): Use $(MAKE), not make. (org-deploy): Remove this obsolete rule.
-
Alexandre Duret-Lutz authored
* wrap/python/ajax/spotcgi.in: Here.
-
- 17 Jun, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
* wrap/python/ajax/css/ui-lightness/: Delete. * wrap/python/ajax/Makefile.am: Adjust. * wrap/python/ajax/trans.html: Fetch the UI theme from Google's CDN. * wrap/python/ajax/css/trans.css: Add the tweaks locally.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
This is the version currently in Debian. * wrap/python/ajax/trans.html: Adjust to the newer version.
-