Commit graph

4859 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
2e165f188d rename SPOT_NB_ACC to SPOT_MAX_ACCSETS
* NEWS, bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc,
configure.ac, spot/parseaut/parseaut.yy, spot/twa/acc.cc,
spot/twa/acc.hh, tests/core/acc.cc, .gitlab-ci.yml: Here.
2018-05-24 22:18:42 +02:00
Alexandre Duret-Lutz
cc2c4615d0 bitset: optimize the code generated by shifts in common cases
* spot/misc/bitset.hh: Here.
* spot/misc/bitset.cc: New file.
* spot/misc/Makefile.am: Add it.
* spot/twa/acc.hh: Conditionally remove the exception checks around
shift operators.
* spot/misc/common.hh (SPOT_ASSUME): New macro.
2018-05-24 19:23:48 +02:00
Alexandre Duret-Lutz
e979791071 common: typo
* spot/misc/common.hh (SPOT_BUILTIN_UNREACHABLE): Typo.
2018-05-24 19:23:48 +02:00
Alexandre Duret-Lutz
b17a9f8578 * tests/sanity/style.test: Allow {{x}} in constructors. 2018-05-24 19:23:48 +02:00
Alexandre Duret-Lutz
c87c13db67 autfilt: better handling of chain of products with -B
Fixes #348, reported by Jeroen Meijer.

* bin/autfilt.cc: If -B is used with many --product,
degeneralize intermediate products as needed.
* NEWS: Mention the change.
* tests/core/prodchain.test: New file.
* tests/Makefile.am: Add it.
* spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of
overflow.
* tests/core/acc.cc: Adjust.
2018-05-24 19:23:48 +02:00
Alexandre Duret-Lutz
a738801edf product: optimize product with weak automata
Fixes #350.

* spot/twaalgos/product.cc: Implement this change.
* NEWS, spot/twaalgos/product.hh: Mention it.
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method.
* tests/python/_product_weak.ipynb: New file.
* tests/Makefile.am: Add it.
* tests/python/automata.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases.
2018-05-23 22:07:50 +02:00
Maximilien Colange
b655038803 ltlsynt: improve coverage
* tests/core/ltlsynt.test: here
2018-05-23 18:40:15 +02:00
Maximilien Colange
61b2b9b140 genltl: improve coverage
* tests/core/genltl.test: here
* spot/gen/formulas.cc: typo
2018-05-23 17:32:54 +02:00
Maximilien Colange
321230f869 ltlfilt: improve coverage
* tests/core/ltlfilt.test: here
2018-05-23 12:01:43 +02:00
Maximilien Colange
1a4117a07f randltl: fix option --allow-dups
* bin/randltl.cc: here
* tests/core/rand.test: test it
* NEWS: document it
2018-05-23 12:01:43 +02:00
Maximilien Colange
cde0977ef8 hide implementation of spot::acc_cond::mark_t
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc,
  spot/parseaut/parseaut.yy: use SPOT_NB_ACC
* spot/twa/acc.hh: make implementation private
2018-05-23 10:27:51 +02:00
Maximilien Colange
c6c085ab22 various fixes to bitset
* spot/misc/bitset.hh: here
* tests/core/acc.cc: test it
2018-05-23 10:02:43 +02:00
Alexandre Duret-Lutz
74651c811d optionmap: fix set()
This longstanding issue caused some emptiness checks options to be
ignored in the test suite, reducing coverage.

* spot/misc/optionmap.cc (set): Insert the other keys without
erasing the existing ones.
2018-05-22 16:14:18 +02:00
Alexandre Duret-Lutz
a3b9469d67 gtec: hide some debugging code behind #if/#endif
* spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/gtec.hh:
Here.
2018-05-22 16:14:18 +02:00
Alexandre Duret-Lutz
75550112a7 bin: remove some dead code
* bin/common_trans.cc, bin/common_trans.hh: Here.
2018-05-22 16:14:18 +02:00
Maximilien Colange
0205ff1394 build with a large spot::acc_cond::mark_t
* .gitlab-ci.yml: here
2018-05-22 13:57:32 +02:00
Maximilien Colange
f4476e78c8 building spot::acc_cond::mark_t from unsigned is deprecated
* spot/twa/acc.hh: here
2018-05-22 13:57:23 +02:00
Maximilien Colange
17532163d2 more portable configure.ac
* configure.ac: do not use bash-ism
2018-05-22 13:54:17 +02:00
Maximilien Colange
65a56f4cef improve coverage
* tests/core/acc.cc: here
* tests/core/acc.test: fix test invokation
2018-05-22 12:16:43 +02:00
Maximilien Colange
6f057941ce better coverage for ltlsynt
* tests/core/ltlsynt.test: here
2018-05-22 11:26:31 +02:00
Maximilien Colange
d7ee23ed2f acc_cond::mark_t now relies on bitset
This allows to represent more than 32 acceptance marks.

* configure.ac: add an option to specify the number of marks
* spot/twa/acc.hh: implement it
* tests/python/acc_cond.ipynb, tests/core/acc.cc,
  tests/core/ltlcross3.test: update tests
* NEWS: document it
* bin/randltl.cc: fix an include
2018-05-22 09:54:19 +02:00
Maximilien Colange
d77d046d26 a new bitset class with static size
* spot/misc/bitset.hh: implement it
* spot/misc/Makefile.am: distribute it
2018-05-22 09:54:19 +02:00
Maximilien Colange
1aaeccf1d3 remove parity_product and parity_product_or
* NEWS: document it
* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh,
  tests/core/parity.cc: here
2018-05-22 09:54:13 +02:00
Alexandre Duret-Lutz
8120587fbf * .gitlab-ci.yml: Remove spot.cc and spot-x.cc from coverage report. 2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
924a642939 * tests/core/randtgba.cc: Remove code related to random formulas. 2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
6e8af75ee9 autcross: exercise %S, %L, and {name{nest}}
* tests/core/autcross.test, tests/core/autcross2.test: More tests.
2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
3334a6a679 bin: remove dead code from ltl2tgta
* bin/ltl2tgta.cc: There is no -B option.
2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
c369f899a3 bin: teach conversion options to report about the options
* bin/common_conv.cc, bin/common_conv.hh: Here.
* bin/autfilt.cc, bin/common_trans.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Pass
the name of the argumennt to the conversion function.
* tests/core/ltlcross3.test, tests/core/ltldo.test,
tests/core/randaut.test: Add test cases.
2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
1f9f3c77ea bin: abort autcross on input parse error
* bin/common_hoaread.hh (hoa_processor): Add a abort_on_error
option.
* bin/autcross.cc: Use it.
* tests/core/autcross4.test: Add many more error cases to improve
coverage.
2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
faca835a5e bin: improve coverage of range-checking code
* tests/core/genaut.test: Here.
2018-05-21 11:00:36 +02:00
Alexandre Duret-Lutz
eca96cdf80 parseaut: accept Alias: before AP:
Fixes #345.

* spot/parseaut/parseaut.yy: Deal with this inconvenient order.
* tests/core/parseaut.test: Test it.
* NEWS: Mention the bug fix.
2018-05-21 10:24:25 +02:00
Alexandre Duret-Lutz
7b580e006a bin: add --usage back
Because it appears in some error messages we cannot remove.  Make
--usage as a synonym for --help.

* bin/common_setup.cc: Here.
2018-05-20 17:36:24 +02:00
Alexandre Duret-Lutz
af3f62c1c8 ltlcross, ltldo, autcross: add support for Rabinizer 4 tools
* bin/common_trans.cc: Here.
* NEWS: Mention that.
2018-05-20 17:24:26 +02:00
Alexandre Duret-Lutz
2e90460b8a tests: exercise --stats='%[v]c %[IW]c' and friends
* tests/core/scc.test: Here.
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
47974cd004 autfilt: support --is-colored
This also improve the coverage of the is_colored() function, because
it was not used in negative cases so far.

* bin/autfilt.cc: Implement it.
* tests/core/satmin2.test: Test it.
* NEWS: Mention it.
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
00c3271c72 python: tests exceptions raised by is_weak_scc() and friends
* tests/python/except.py: Here.
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
2f8ae55f6b bin: diagnose failures to print --help
Fixes #349.

* bin/common_setup.cc (OPT_HELP, OPT_VERSION): Call close_stdout().
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
a80cd361c0 bin: finish removal of --usage
* bin/common_setup.cc: Here.
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
021c0ed0b5 gnulib: add the closeout and secure_getenv modules
* lib/close-stream.c, lib/close-stream.h, lib/closeout.c,
lib/closeout.h, lib/fpending.c, lib/fpending.h, lib/stdio-impl.h,
lib/secure_getenv.c, m4/close-stream.m4, m4/closeout.m4,
m4/fpending.m4, m4/secure_getenv.m4: New file.
* lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
2018-05-18 20:50:48 +02:00
Alexandre Duret-Lutz
2076197e8d update gnulib to b35c22af02271c8dd9844b98db17702b8bf2bd93
* lib/Makefile.am, lib/alloca.in.h, lib/arg-nonnull.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++defs.h, 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/filename.h, lib/float+.h,
lib/float.c, lib/float.in.h, lib/getopt-cdefs.in.h, lib/getopt-core.h,
lib/getopt-ext.h, lib/getopt-pfx-core.h, lib/getopt-pfx-ext.h,
lib/getopt.c, lib/getopt.in.h, lib/getopt1.c, lib/getopt_int.h,
lib/getprogname.c, lib/getprogname.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/limits.in.h,
lib/localcharset.c, lib/localcharset.h, lib/localtime-buffer.c,
lib/localtime-buffer.h, lib/lstat.c, lib/malloc.c, lib/malloca.c,
lib/malloca.h, lib/mbrtowc.c, lib/mbsinit.c, lib/memchr.c,
lib/mempcpy.c, lib/minmax.h, 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/size_max.h, lib/sleep.c, lib/stat-w32.c, lib/stat-w32.h,
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/warn-on-use.h, 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/eealloc.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/getprogname.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/limits-h.m4, m4/localcharset.m4, m4/locale-fr.m4, m4/locale-ja.m4,
m4/locale-zh.m4, m4/localtime-buffer.m4, m4/longlong.m4, m4/lstat.m4,
m4/malloc.m4, m4/malloca.m4, m4/math_h.m4, m4/mbrtowc.m4,
m4/mbsinit.m4, m4/mbstate_t.m4, m4/memchr.m4, m4/mempcpy.m4,
m4/minmax.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/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: Update.
* lib/malloca.valgrind, lib/secure_getenv.c, m4/secure_getenv.m4:
Delete.
* lib/stat-time.c, lib/stat-time.h, m4/stat-time.m4: New files.
2018-05-17 16:05:57 +02:00
Alexandre Duret-Lutz
645bb55622 bin: factor exception-handling code
* bin/common_setup.cc, bin/common_setup.hh: Define a protected_main()
function that deal with exceptions.
* bin/autcross.cc, bin/autfilt.cc, bin/dstar2tgba.cc, bin/genaut.cc,
bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc,
bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc,
bin/randaut.cc, bin/randltl.cc: Use it for all tools.
2018-05-16 20:15:04 +02:00
Alexandre Duret-Lutz
fc0ed01a45 randomltl: avoid #define
As this pollutes the user's namespace.

* spot/tl/randomltl.hh: Use class-level enum and constexpr instead
of #define.
* spot/tl/randomltl.cc, python/spot/__init__.py, bin/randltl.cc,
tests/python/dualize.py, tests/python/sum.py: Adjust usage.
2018-05-16 18:35:36 +02:00
Alexandre Duret-Lutz
565e25502c bin: stop supporting the hidden --usage
It's not used anywhere, not documented, and its output is slightly
broken with options that are too long.

* bin/common_setup.cc: Remove --usage support.
2018-05-16 17:18:48 +02:00
Alexandre Duret-Lutz
f0b57d7264 tests: use ltlcross --color for better code coverage
* tests/core/ltlcross3.test: Here.
2018-05-16 17:05:21 +02:00
Alexandre Duret-Lutz
70b4aa7b7e bin: remove some dead code
* bin/common_output.cc, bin/common_output.hh: Here.
2018-05-16 17:05:21 +02:00
Alexandre Duret-Lutz
589a4035bc tests: cover error handling of ltlfilt -r
* tests/core/ltlfilt.test: Add test cases.
2018-05-16 17:05:21 +02:00
Alexandre Duret-Lutz
a94cc623ad * tests/core/bdd.test: Cover garbage collection hooks. 2018-05-16 16:16:47 +02:00
Alexandre Duret-Lutz
f3a80a58c5 remove useless reachiter.hh includes
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/neverclaim.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/stripacc.cc: Here.
2018-05-16 14:27:49 +02:00
Alexandre Duret-Lutz
4d82758726 autfilt: --complement accepts non-deterministic input
* bin/autfilt.cc: Fix the --help string for --complement, and also
merge edges in the resulting automaton, as suggested by František
Blahoudek.
* tests/core/complement.test: Adjust output and add František's
example.
2018-05-16 14:23:31 +02:00
Alexandre Duret-Lutz
605bcd723d Upgrade to GitLab 10.7
* .gitlab-ci.yml (publish-stable, publish-unstable): Use a single
variable to pass the current branch to the spot-web project.
2018-05-16 10:34:31 +02:00