- 10 Dec, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/ltsmin/ltsmin.cc: Add an assert.
-
- 09 Dec, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
Reported by Shufang Zhu. * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion and update the comments. * tests/core/ltlfilt.test: Adjust test cases. * NEWS: Mention the fix. * THANKS: Add Shufang Zhu.
-
- 02 Dec, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
Compilation of each header file alone, as a safety check, was removed when introducing "#pragma once" because we did not have to check for possible double inclusion. However we still need to compile each header to make sure they are self-contained. * tests/sanity/includes.test: Compile each header. * tests/run.in: Export various compiler and directory flags. * spot/twaalgos/emptiness_stats.hh, spot/misc/mspool.hh, spot/misc/fixpool.hh: Include <spot/misc/common.hh>. * spot/misc/common.hh: Include <cassert>. * NEWS: Mention the fixed headers.
-
- 01 Dec, 2016 4 commits
-
-
Alexandre Duret-Lutz authored
* spot/parseaut/parseaut.yy: Add a diagnostic. * tests/core/parseaut.test: Test it. * NEWS: Document it.
-
Alexandre Duret-Lutz authored
* tests/run.in: Here.
-
Maximilien Colange authored
* tests/sanity/style.test: Allow parenthesis after 'operator delete'.
-
Maximilien Colange authored
* tests/core/randtgba.cc: do not time statistics.
-
- 30 Nov, 2016 3 commits
-
-
Alexandre Duret-Lutz authored
* spot/twa/twagraph.hh (state_acc_sets, state_is_accepting): Do not check num_sets()==0 since this would imply prop_state_acc().
-
Alexandre Duret-Lutz authored
* spot/graph/graph.hh: Use only const variants of begin()/end(), since they do not modify the iterator.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/sccinfo.cc: We do not need to care about 0 states anymore.
-
- 29 Nov, 2016 5 commits
-
-
Alexandre Duret-Lutz authored
... by calling valgrind less often. * tests/core/reduc.test, tests/core/reducpsl.test: Call valgrind only on 1 of the 12 calls to randltl, and 2 of the 7 calls to reduc.
-
Alexandre Duret-Lutz authored
* tests/core/readltl.cc: Process many formulas from a file instead of one arg at a time. * tests/core/parse.test, tests/core/parseerr.test, tests/core/utf8.test: Adjust to supply a file as input.
-
Alexandre Duret-Lutz authored
* tests/core/tostring.test: Move all the input formulas into... * tests/core/tostring.cc: ... the code, and do the loop there.
-
Maximilien Colange authored
* NEWS, spot/twa/twa.hh: Document the change. * spot/twa/twagraph.hh, spot/kripke/kripkegraph.hh: Add an exception in get_init_state_number(). get_init_state() now calls get_init_state_number(). * spot/twa/twagraph.cc, spot/twaalgos/simulation.cc, spot/twaalgos/powerset.cc, spot/twaalgos/complete.cc, spot/twaalgos/sccfilter.cc: Remove now useless tests. * spot/twaalgos/hoa.cc: Remove now useless comment. * spot/twaalgos/minimize.cc: Never return an automaton with no state.
-
Alexandre Duret-Lutz authored
* debian/source/lintian-overrides: New file. * Makefile.am: Add it.
-
- 28 Nov, 2016 4 commits
-
-
Alexandre Duret-Lutz authored
This fix some lintian issues. * debian/control: Add dependency. * debian/rules: Fix the generated html page to use the local jquery.
-
Alexandre Duret-Lutz authored
This should solve issue with the Debian package. * spot/ltsmin/Makefile.am: Use the LTDLINC, LTDLDEPS and LIBLTDL as documented. * NEWS: Mention the fix.
-
Alexandre Duret-Lutz authored
Fix #198. Reported by Maximilien Colange. * spot/twaalgos/strength.cc (is_terminal): Test that no accepting transition lead to a rejecting SCC. * tests/core/strength.test: Add test case. * spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org: Adjust documentation. * NEWS: Mention the fix.
-
Maximilien Colange authored
* spot/misc/casts.hh: Add a macro down_pointer_cast.
-
- 25 Nov, 2016 1 commit
-
-
Maximilien Colange authored
* spot/misc/common.hh: Change SPOT_DEPRECATED definition.
-
- 24 Nov, 2016 4 commits
-
-
Alexandre Duret-Lutz authored
Because gal2c generates some C++ sources that do not match our coding convention and should not be checked. * tests/sanity/80columns.test, tests/sanity/style.test: Do not test files in tests' work directories.
-
Alexandre Duret-Lutz authored
Fixes #195. * tests/ltsmin/check.test: Extract the spins and gal checks and move them to... * tests/ltsmin/check2.test, tests/ltsmin/check3.test: ... these files. * tests/Makefile.am: Adjust.
-
Alexandre Duret-Lutz authored
This fixes c9aabcdd. * spot/ltsmin/ltsmin.cc: Update the extension after compiling the model. Do not duplicate the symbol lookups for DVE and gal2C. Also, improve error reporting in case of missing symbol. * tests/ltsmin/check.test: Remove stray character.
-
Alexandre Duret-Lutz authored
Reported by František Blahoudek. * spot/twaalgos/sccfilter.cc: Remove extra print statement. * NEWS: Mention it.
-
- 23 Nov, 2016 4 commits
-
-
Maximilien Colange authored
* spot/ltsmin/ltsmin.cc: Improve error messages.
-
Maximilien Colange authored
* spot/ltsmin/ltsmin.cc: Handle GAL models. * tests/Makefile.am: Test the new feature. * tests/ltsmin/check.test: Also check GAL. * tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests. * tests/ltsmin/finite.gal: A new GAL model for tests. * tests/ltsmin/finite3.test: A new test for GAL.
-
Etienne Renault authored
* spot/misc/bitvect.hh, tests/core/bitvect.cc, tests/core/bitvect.test: here.
-
Etienne Renault authored
* spot/graph/ngraph.hh, spot/ltsmin/ltsmin.cc, spot/misc/bitvect.hh, spot/misc/intvcomp.cc, spot/misc/satsolver.cc, spot/priv/weight.cc, spot/ta/taexplicit.cc, spot/taalgos/minimize.cc, spot/taalgos/reachiter.cc, spot/tl/exclusive.cc, spot/tl/formula.cc, spot/tl/formula.hh, spot/tl/mark.cc, spot/tl/mutation.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc, spot/tl/simplify.cc, spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/taatgba.hh, spot/twa/twa.hh, spot/twa/twagraph.cc, spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc, spot/twaalgos/compsusp.cc, spot/twaalgos/copy.cc, spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc, spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc, spot/twaalgos/powerset.cc, spot/twaalgos/product.cc, spot/twaalgos/randomgraph.cc, spot/twaalgos/reachiter.cc, spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/se05.cc, spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc, spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc, spot/twaalgos/word.cc, tests/core/bitvect.cc: here.
-
- 21 Nov, 2016 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Update.
-
- 19 Nov, 2016 2 commits
-
-
Alexandre Duret-Lutz authored
* tests/core/ltl2tgba.test: Add new test-case, reported by Tomáš Babiak. * NEWS: Mention the bug fixed by previous patch.
-
Alexandre Duret-Lutz authored
* src/kernel.c: Fix error introduced by 5a862295. Report from Tomáš Babiak.
-
- 14 Nov, 2016 3 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* configure.ac, doc/org/setup.org, NEWS: Set version number.
-
- 13 Nov, 2016 4 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* doc/org/oaut.org (Timing): New section. * NEWS: Link to it.
-
Alexandre Duret-Lutz authored
* spot/twa/twa.hh, spot/twa/twa.cc (intersects, intersecting_run, intersecting_word): New functions. * NEWS: Mention them. * doc/org/tut51.org, tests/python/bugdet.py: Use them.
-
Alexandre Duret-Lutz authored
-
- 12 Nov, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
-