- 25 Aug, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* src/tests/bitvect.cc: Fix it, it was failing an assert() on 32bit architectures because the subset test was done in the wrong order. Reported by Christopher Ziegler. * NEWS: Mention it.
-
- 24 Aug, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
Fixes #96, reported by Vitus Lam & Christopher Ziegler. * src/bin/ltlcross.cc: Catch std::bad_alloc, skip those products and the related tests. Display a count of those skipped tests at the end. * NEWS: Mention it. * src/tests/ltlcross3.test: Adjust expected error message.
-
- 23 Aug, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
Reported by Christopher Ziegler. * src/tests/uniq.test: For LC_ALL=C before sort.
-
- 21 Aug, 2015 7 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
This implies learning alternative rules for G, and W as well, since those would use R. Fixes #103. Suggested by Joachim Klein. * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: Implement the new rules. * doc/tl/tl.tex: Document the rules. * src/tests/unabbrevwm.test: Test them. * src/bin/ltlfilt.cc, NEWS: Mention that --unabbreviate accepts R.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 20 Aug, 2015 7 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Fixes #8. * src/bin/dstar2tgba.cc: Here.
-
Alexandre Duret-Lutz authored
* src/dstarparse/dstarparse.yy, src/dstarparse/dstarscan.ll src/dstarparse/parsedecl.hh, src/dstarparse/public.hh: Adjust to return the same return types as parse_aut. * src/dstarparse/fmterror.cc: Delete, we can use the one of parse_aut. * src/dstarparse/Makefile.am: Adjust. * src/tests/ikwiad.cc, src/bin/dstar2tgba.cc, src/bin/ltldo.cc: Adjust usage. * src/bin/ltlcross.cc: The the result of dstar_parse() as-is, now that it is a TωA like those produced by parse_aut(). As a consequence, get rid of all the code storing statistics about the input automaton. * src/tests/ltlcross3.test, src/tests/ltl2dstar.test: Adjust expected CSV output. * doc/org/ltlcross.org, src/bin/man/ltlcross.x: Adjust to not mention that %D performs a tranformation to Büchi.
-
Alexandre Duret-Lutz authored
Since we just removed that conversion, those can go as well. Yay! * src/tests/kv.test, src/twa/twamask.cc, src/twa/twamask.hh, src/twa/twaproxy.cc, src/twa/twaproxy.hh, src/twaalgos/scc.cc, src/twaalgos/scc.hh: Delete. * src/twaalgos/Makefile.am, src/twa/Makefile.am, src/tests/Makefile.am, src/tests/ikwiad.cc: adjust.
-
Alexandre Duret-Lutz authored
* src/dstarparse/dstarparse.yy: Use the twa_graph_ptr to store the acceptance condition. * src/dstarparse/dra2ba.cc, src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc: Delete all these conversion routines. * src/dstarparse/public.hh, src/dstarparse/Makefile.am: Adjust. * src/bin/dstar2tgba.cc: Adjust to call to_generalized_buchi() instead. * src/bin/ltlcross.cc: Adjust to call remove_fin() instead. * src/bin/ltldo.cc: Use the parsed automaton as-is. * src/tests/degenid.test, src/tests/dstar.test, src/tests/ikwiad.cc: Adjust test cases.
-
Alexandre Duret-Lutz authored
I.e., automata that could be Rabin if we add some empty Fin(x) or full Inf(y) sets. This way it does not matter when remove_fin() is called after cleanup_acceptance(). * src/twaalgos/remfin.cc: Implement that. * src/tests/remfin.test: More tests.
-
Alexandre Duret-Lutz authored
Because using multiple acceptance condition is pointless in this case. * src/twaalgos/remfin.cc (ra_to_ba): Extract most of the RA->BA code into this new function for clarity. * src/tests/remfin.test: Adjust.
-
- 19 Aug, 2015 4 commits
-
-
Alexandre Duret-Lutz authored
* src/twaalgos/remfin.cc: Here. * src/tests/remfin.test: Add a single test. * src/twa/acc.hh (mark_t::lowest): New function.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 18 Aug, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
* src/ltlparse/ltlscan.ll: Adjust parser. * src/ltlvisit/print.cc: Adjust printer. * src/tests/ltlfilt.test: Add some tests. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* doc/tl/tl.tex: Here.
-
Alexandre Duret-Lutz authored
* src/ltlvisit/mutation.cc, src/ltlvisit/relabel.cc, src/ltlvisit/remove_x.cc: Add final keyword to final classes.
-
- 17 Aug, 2015 4 commits
-
-
Alexandre Duret-Lutz authored
(Upcoming GCC 6.) * src/misc/intvcmp2.cc: Here. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* src/bin/ltlfilt.cc: Add option --unabbreviate. * src/tests/ltlfilt.test: Add a test case. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh, src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh: Delete. * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: New files. * src/ltlvisit/Makefile.am: Adjust. * src/ltlvisit/print.cc, src/tests/equalsf.cc, src/tests/Makefile.am, src/twaalgos/ltl2taa.cc, wrap/python/spot_impl.i, src/bin/ltlfilt.cc: Adjust callers. * src/ltlvisit/contain.cc, src/tests/syntimpl.cc: Remove useless include. * wrap/python/tests/formulas.ipynb: New test cases. * doc/tl/tl.tex: Group all rules in a single section. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
- 14 Aug, 2015 5 commits
-
-
Alexandre Duret-Lutz authored
Fixes #39, reported by Joachim Klein. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Take an option to specify which of xor/equiv/implies should be rewritten. * src/ltlvisit/print.cc (print_spin): Rewrite only xor. * src/tests/ltlfilt.test: Add a test case. * NEWS: Mention this.
-
Alexandre Duret-Lutz authored
* src/twa/twagraph.hh (namer): Use a template alias instead of a trait. * src/twa/twagraph.cc, src/parseaut/parseaut.yy, src/twaalgos/ltl2tgba_fm.cc: Adjust.
-
Alexandre Duret-Lutz authored
* src/twa/bdddict.cc, src/twa/bdddict.hh: Here.
-
Alexandre Duret-Lutz authored
* src/twaalgos/totgba.cc: Here. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
We do not remove them in rejecting SCCs (as it might make the SCC accepting), but we can remove them between SCCs. Fixes #101. * src/twaalgos/sccfilter.cc: Here. * src/tests/sccsimpl.test: Add test case. * NEWS: Mention this.
-
- 13 Aug, 2015 7 commits
-
-
Alexandre Duret-Lutz authored
* src/ltlvisit/print.cc: Property output the double quotes in latex mode, not only sclatex. * src/misc/escape.cc: Fix LaTeX escape to work in math mode. * src/tests/latex.test: Add a test. * wrap/python/tests/formulas.ipynb: Adjust expected output * NEWS: Mention the fix.
-
Alexandre Duret-Lutz authored
Fixes #100. * doc/org/tut.org: Link to the notebook. * src/sanity/ipynb.test: New test, to make sure we do not forget to document ipython notebook when we add some. * src/sanity/Makefile.am: Add it and run it. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-