- 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
-
- 11 Nov, 2016 6 commits
-
-
Alexandre Duret-Lutz authored
* spot/twa/twagraph.hh: Here.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Suggested by Juraj Major. * spot/twaalgos/sccfilter.cc: Here. * tests/python/sccfilter.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the news.
-
Alexandre Duret-Lutz authored
Reported by Juraj Major. * spot/twa/twa.hh: check num_sets() in prop_state_acc() so we do not have to set it in set_acceptance(), causing trouble if set_acceptance() is called multiple times. * tests/python/setacc.py: New test case. * tests/Makefile.am: Add it. * THANKS: Add Juraj. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/remfin.cc: Do not add a sink states to deterministic weak automata, and actually apply the "weak" Fin-removal to any weak automaton. * tests/core/explprod.test: Add a test case for the previous patch, but that used to fail because of this bug. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
* spot/parseaut/public.hh, spot/parseaut/scanaut.ll: When parsing automata read from some given FD, do not close the file descriptor, as the caller is likely to already close it, and closing FDs twice is very bad. This seems to have be the root of some issue we had with recent jupyter versions, were 0MQ would crash with "Bad file descriptor" messages. Also do not close stdin while we are at it. * NEWS: Mention the bug.
-
- 10 Nov, 2016 1 commit
-
-
Alexandre Duret-Lutz authored
* tests/python/ipnbdoctest.py: here.
-