- 13 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
* src/bddio.c, src/bddop.c, src/imatrix.c, src/pairs.c: Here.
-
Alexandre Duret-Lutz authored
Fixes #242. * doc/tl/tl.tex: Remove incorrect claim that {r} does not match the PSL semantics.
-
- 10 Mar, 2017 3 commits
-
-
Alexandre Duret-Lutz authored
* doc/org/g++wrap.in: Save error messages. * doc/Makefile.am: Display them at the end of the compilation.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/emptiness_stats.hh (unsigned_statistics_copy): Remove. * tests/core/randtgba.cc: Remove option -H.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc, spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance condition is not satisfied. * tests/python/misc-ec.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the change.
-
- 09 Mar, 2017 7 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
This also include my patch to lib/argp.hh for C++ compilation. * lib/Makefile.am, lib/alloca.in.h, lib/argmatch.c, lib/argmatch.h, lib/argp-ba.c, lib/argp-eexst.c, lib/argp-fmtstream.c, lib/argp-fmtstream.h, lib/argp-fs-xinl.c, lib/argp-help.c, lib/argp-namefrob.h, lib/argp-parse.c, lib/argp-pin.c, lib/argp-pv.c, lib/argp-pvh.c, lib/argp-xinl.c, lib/argp.h, lib/asnprintf.c, lib/basename-lgpl.c, lib/c-ctype.h, lib/c-strcase.h, lib/c-strcasecmp.c, lib/c-strcaseeq.h, lib/c-strncasecmp.c, lib/config.charset, lib/dirname-lgpl.c, lib/dirname.h, lib/dosname.h, lib/errno.in.h, lib/error.c, lib/error.h, lib/exitfail.c, lib/exitfail.h, lib/fcntl.in.h, lib/float+.h, lib/float.c, lib/float.in.h, lib/getopt.c, lib/getopt.in.h, lib/getopt1.c, lib/getopt_int.h, lib/gettext.h, lib/gettimeofday.c, lib/hard-locale.c, lib/hard-locale.h, lib/intprops.h, lib/isatty.c, lib/itold.c, lib/localcharset.c, lib/localcharset.h, lib/lstat.c, lib/malloc.c, lib/mbrtowc.c, lib/mbsinit.c, lib/memchr.c, lib/mempcpy.c, lib/mkstemp.c, lib/mkstemps.c, lib/msvc-inval.c, lib/msvc-inval.h, lib/msvc-nothrow.c, lib/msvc-nothrow.h, lib/pathmax.h, lib/printf-args.c, lib/printf-args.h, lib/printf-parse.c, lib/printf-parse.h, lib/progname.c, lib/progname.h, lib/quote.h, lib/quotearg.c, lib/quotearg.h, lib/rawmemchr.c, lib/ref-add.sin, lib/ref-del.sin, lib/secure_getenv.c, lib/size_max.h, lib/sleep.c, lib/stat.c, lib/stdalign.in.h, lib/stdbool.in.h, lib/stddef.in.h, lib/stdint.in.h, lib/stdio.in.h, lib/stdlib.in.h, lib/stpcpy.c, lib/strcasecmp.c, lib/strchrnul.c, lib/streq.h, lib/strerror-override.c, lib/strerror-override.h, lib/strerror.c, lib/string.in.h, lib/strings.in.h, lib/stripslash.c, lib/strncasecmp.c, lib/strndup.c, lib/strnlen.c, lib/strverscmp.c, lib/sys_stat.in.h, lib/sys_time.in.h, lib/sys_types.in.h, lib/sys_wait.in.h, lib/sysexits.in.h, lib/tempname.c, lib/tempname.h, lib/time.in.h, lib/unistd.in.h, lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h, lib/vsnprintf.c, lib/wchar.in.h, lib/wctype.in.h, lib/xalloc-die.c, lib/xalloc-oversized.h, lib/xalloc.h, lib/xmalloc.c, lib/xsize.h, m4/00gnulib.m4, m4/absolute-header.m4, m4/alloca.m4, m4/argp.m4, m4/configmake.m4, m4/dirname.m4, m4/double-slash-root.m4, m4/errno_h.m4, m4/error.m4, m4/exponentd.m4, m4/extensions.m4, m4/extern-inline.m4, m4/fcntl-o.m4, m4/fcntl_h.m4, m4/float_h.m4, m4/getopt.m4, m4/gettimeofday.m4, m4/glibc21.m4, m4/gnulib-cache.m4, m4/gnulib-common.m4, m4/gnulib-comp.m4, m4/gnulib-tool.m4, m4/hard-locale.m4, m4/include_next.m4, m4/intmax_t.m4, m4/inttypes_h.m4, m4/isatty.m4, m4/largefile.m4, m4/localcharset.m4, m4/locale-fr.m4, m4/locale-ja.m4, m4/locale-zh.m4, m4/longlong.m4, m4/lstat.m4, m4/malloc.m4, m4/math_h.m4, m4/mbrtowc.m4, m4/mbsinit.m4, m4/mbstate_t.m4, m4/memchr.m4, m4/mempcpy.m4, m4/mkstemp.m4, m4/mkstemps.m4, m4/mmap-anon.m4, m4/msvc-inval.m4, m4/msvc-nothrow.m4, m4/multiarch.m4, m4/nocrash.m4, m4/off_t.m4, m4/pathmax.m4, m4/printf.m4, m4/quote.m4, m4/quotearg.m4, m4/rawmemchr.m4, m4/secure_getenv.m4, m4/size_max.m4, m4/sleep.m4, m4/ssize_t.m4, m4/stat.m4, m4/stdalign.m4, m4/stdbool.m4, m4/stddef_h.m4, m4/stdint.m4, m4/stdint_h.m4, m4/stdio_h.m4, m4/stdlib_h.m4, m4/stpcpy.m4, m4/strcase.m4, m4/strchrnul.m4, m4/strerror.m4, m4/string_h.m4, m4/strings_h.m4, m4/strndup.m4, m4/strnlen.m4, m4/strverscmp.m4, m4/sys_socket_h.m4, m4/sys_stat_h.m4, m4/sys_time_h.m4, m4/sys_types_h.m4, m4/sys_wait_h.m4, m4/sysexits.m4, m4/tempname.m4, m4/time_h.m4, m4/unistd_h.m4, m4/vasnprintf.m4, m4/vsnprintf.m4, m4/warn-on-use.m4, m4/wchar_h.m4, m4/wchar_t.m4, m4/wctype_h.m4, m4/wint_t.m4, m4/xalloc.m4, m4/xsize.m4, tools/snippet/arg-nonnull.h, tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: Update. * lib/getprogname.c, lib/getprogname.h, lib/limits.in.h, lib/minmax.h, m4/getprogname.m4, m4/limits-h.m4, m4/minmax.m4: New files.
-
Alexandre Duret-Lutz authored
From https://github.com/nemtrif/utfcpp/releases/tag/v2.3.5 * utf8/utf8.h, utf8/utf8/checked.h, utf8/utf8/core.h, utf8/utf8/unchecked.h: Update. * utf8/doc/utf8cpp.html, utf8/doc/ReleaseNotes: Delete. * utf8/README.md: New file. * Makefile.am: Adjust.
-
Alexandre Duret-Lutz authored
* python/spot/impl.i: Here. * tests/python/declenv.py: New file. * tests/Makefile.am: Add it.
-
Alexandre Duret-Lutz authored
* spot/parsetl/parsetl.yy (parse_ap, sere_ensure_bool, error_false_block): New functions, replacing several similar blocks.
-
Alexandre Duret-Lutz authored
-
Thomas Medioni authored
Fixes #231. * NEWS: Mention of implementation of sum, sum_and. * bin/autfilt.cc: Add --sum, --sum-or and --sum-and options. * python/spot/impl.i: Add bindings for sum, sum_and. * spot/twaalgos/Makefile.am: Add sum.cc, sum.hh. * spot/twaalgos/sum.cc: Implement sum, sum_and. * spot/twaalgos/sum.hh: Declaration of sum, sum_and. * tests/Makefile.am: Add sum tests. * tests/core/explsum.test: Test the sum of two automatons, false or false, unsatisfied mark propagation, handling of univ. transitions. * tests/python/sum.py: Check that two automatons that does not share their bdd dict are not accepted, then run tests over the sum of randomly generated LTL formulas.
-
- 08 Mar, 2017 5 commits
-
-
Alexandre Duret-Lutz authored
* python/spot/impl.i: Here. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* doc/org/upgrade2.org, tests/python/prodexpt.py, tests/python/product.ipynb, NEWS: Fix typos. * tests/sanity/style.test: Add a check for this.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/degen.cc: Make use_cust_acc_orders as unlikely, as it was never true in the whole test suite before this patch. * tests/core/ltlcross2.test: Play with degen-order and degen-lcache options to test more cases.
-
Alexandre Duret-Lutz authored
Follow-up to an email from Ayrat Khalimov. * python/spot/impl.i: Include twa/formula2bdd.hh. * python/spot/__init__.py: Make the dictionnary optional. * spot/twa/formula2bdd.cc: Throw an exception instead of asserting. * tests/python/bdditer.py: New file. * tests/Makefile.am: Add it. * NEWS: Update.
-
- 07 Mar, 2017 5 commits
-
-
Alexandre Duret-Lutz authored
* spot/twa/twagraph.hh: Here. * NEWS: Mention the change.
-
Alexandre Duret-Lutz authored
The goal is to improve coverage stats, but I discovered two issues while doing so. * tests/python/twagraph.py: New test case. * tests/Makefile.am: Add it. * spot/twa/twagraph.hh: Add fix typos in error messages. * python/spot/impl.i: Fix broken wrappers for state_from_number and state_acc_sets.
-
Alexandre Duret-Lutz authored
This very old test did not do anything useful today. * tests/core/ltlprod.cc, tests/core/ltlprod.test: Delete. * tests/Makefile.am: Adjust.
-
Alexandre Duret-Lutz authored
Fixes #239. * spot/twaalgos/postproc.hh, spot/twaalgos/translate.hh: Here.
-
Alexandre Duret-Lutz authored
Reported by Thomas Medioni. * spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus template parameter. * tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method. * NEWS: Mention the bug.
-
- 03 Mar, 2017 6 commits
-
-
Alexandre Duret-Lutz authored
Fixes #241. * spot/twaalgos/postproc.cc: Use the deterministic monitor if it has as many states as the non-deterministic one. * spot/twaalgos/minimize.cc (minimize_monitor): Quickly check for terminal automata. * spot/twaalgos/stripacc.cc: Set the weak property. * spot/twaalgos/stripacc.hh: Improve documentation. * tests/core/monitor.test, tests/core/sbacc.test: Update. * NEWS: Mention the issue.
-
Alexandre Duret-Lutz authored
* doc/org/tut10.org: Remove a couple of useless includes.
-
Alexandre Duret-Lutz authored
Part of #239. * doc/org/tut11.org: New file. * doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can link to in tut11.org. * doc/org/tut.org, doc/Makefile.am: Add tut11.org. * NEWS: Mention the new page.
-
Alexandre Duret-Lutz authored
Fixes #240. * spot/twaalgos/postproc.cc: Do not call do_simul on the output of minimize_monitor(), and do not skip complete() when PREF_==Any. * tests/core/monitor.test: Add a test case. * NEWS: Mention the bug. * doc/org/ltl2tgba.org: Document complete monitors.
-
Alexandre Duret-Lutz authored
This avoids a few conversion problems, and also made the bug of sbacc (fixed by 37fc948b) obvious. Reported by Thomas Medioni. * spot/twa/acc.hh (mark_t::operator bool): Make it explicit. * spot/twaalgos/remfin.cc: Adjust.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and fix the value of init_acc. * tests/core/sbacc.test: Add a test case. * NEWS: Mention the bug.
-
- 02 Mar, 2017 1 commit
-
-
Alexandre Duret-Lutz authored
Fixes #238. * spot/twa/acc.hh (max_set): Add a version using __builtin_clz(). (min_set): New method. * tests/core/acc.cc, tests/core/acc.test: Add some tests.
-
- 01 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
Fixes #237. * bin/genltl.cc: Fix the numbering of options. * NEWS: Mention the bugs.
-
Alexandre Duret-Lutz authored
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc, bin/common_output.hh: Add options to %x to list atomic propositions with various quoting scheme. Deprecate --format=%a in favor of the new --format=%x for consistency with --stats=%x. * tests/core/format.test, tests/core/remprop.test: Adjust and add more tests. * NEWS: Mention these changes.
-
- 28 Feb, 2017 6 commits
-
-
Alexandre Duret-Lutz authored
Fixes #236. * bin/common_aoutput.cc: Fix it. * tests/core/format.test: Improve test cases. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
Fixes #235, reported by Henrich Lauko. * python/spot/ltsmin.i: Catch CalledProcessError. * NEWS: Mention the bug. * THANKS: Add Henrich.
-
Alexandre Duret-Lutz authored
* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement %x and %X. * tests/core/remprop.test: Test them. * NEWS: Mention them.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* spot/twaalgos/powerset.cc (tgba_powerset): Use twa::ap() to simplify the code. (number_of_variables): Remove.
-
Alexandre Duret-Lutz authored
-
- 21 Feb, 2017 3 commits
-
-
Clément Gillard authored
* tests/python/decompose.ipynb: Add about `decompose_scc`. * doc/org/tut.org: Update description.
-
Clément Gillard authored
Put what is done by `autfilt` in a new function, `decompose_acc_scc`. * bin/autfilt.cc: Move code from here... * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: To here. * tests/python/decompose_scc.py: Test python binding.
-
Clément Gillard authored
See #172. * bin/autfilt.cc: Add option. * tests/core/strength.test: Remove ambiguity with '--decompose-strength'. * NEWS: Mention it. * tests/core/scc.test: Test it.
-