Etienne Renault authored Oct 17, 2019 and Alexandre Duret-Lutz committed Oct 28, 2019

* tests/core/parity.cc: Here.

Reported by Etienne Renault.

* spot/priv/trim.cc: Simplify with a lambda.

This is needed for tcltl.

* python/spot/__init__.py: Alter __path__ to add any spot-extra/
directory we find.
* NEWS: Mention this.

* python/spot/gen.i, python/spot/impl.i, python/spot/ltsmin.i: Here.

* debian/control (spot-doc): Depends on libjs-requirejs.
* debian/rules (fix-js): Replace uses.

* debian/rules: Here.

* NEWS, configure.ac: Here.

* NEWS, configure.ac, doc/org/setup.org: Update version to 2.8.2.

* src/bddx.h (bdd_allsat): Add a version with the old prototype.

* spot/twaalgos/aiger.cc: Simplify some bit operatitions.  Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.

On some architectures (e.g., ARM, or even some -flto setups on Intel)
C++ exceptions to not traverse the C functions.  So even if the C++
main() has a try/catch, it will not catch the exception thrown by C++
code called from the argp module (which is compiled in C).

* bin/common_setup.cc, bin/common_setup.hh: Define some macros
and function to factorize exception handling.
* bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc,
bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc,
bin/common_output.cc, bin/common_post.cc, bin/common_trans.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:
Protect all parse_opt() functions, even those where there is currently
no exception risk.

* spot/misc/bitvect.hh (bitvect_array::at): Fix pointer cast.
* spot/twa/bddprint.cc: Adjust to use signed char* explicitly.
* spot/twaalgos/gtec/gtec.hh: Work around GCC bug #90309.
* .gitlab-ci.yml: Add raspbian build.

* src/bddop.c, src/bddx.h, examples/bddtest/bddtest.cxx: Use signed
char* instead of char*.

Suggested by Victor Khomenko.

* bin/ltl2tgba.cc, bin/ltldo.cc: Implement it.
* doc/org/hierarchy.org: Use it.
* tests/core/ltldo2.test: Test it.
* bin/common_output.cc: Typo.
* NEWS: Mention the new option.

* lib/gettext.h: Remove useless use of NULL.

Otherwise the .gcda files may end into .libs/ and be destroyed by make
clean.

* debian/rules (PRO1SETUP, PRO2SETUP): Here.

* tests/Makefile.am (ltsmin_modelcheck_LDADD): Add -lpthread as it
seems Debian's libtool does not carries this dependency over from
libspotltsmin.la.  Also using $(LTLIBMULTITHREAD) does not work,
because that would add -pthread which is currently ignored when
linking shared libraries (because libtool adds -nostdlib for some
reason).

* configure.ac: Update minimum autoconf version.
* lib/config.charset, lib/ref-add.sin, lib/ref-del.sin,
m4/closeout.m4, m4/close-stream.m4, m4/configmake.m4, m4/glibc21.m4,
m4/hard-locale.m4: Remove.
* lib/alloca.c, lib/alloca.in.h, lib/argmatch.c, lib/argmatch.h,
lib/arg-nonnull.h, lib/argp-ba.c, lib/argp-eexst.c,
lib/argp-fmtstream.c, lib/argp-fmtstream.h, lib/argp-fs-xinl.c,
lib/argp.h, 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/asnprintf.c, lib/basename-lgpl.c, lib/c-ctype.h, lib/c++defs.h,
lib/closeout.c, lib/closeout.h, lib/close-stream.c,
lib/c-strcasecmp.c, lib/c-strcaseeq.h, lib/c-strcase.h,
lib/c-strncasecmp.c, lib/dirname.h, lib/dirname-lgpl.c, 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.c,
lib/float+.h, lib/float.in.h, lib/fpending.c, lib/fpending.h,
lib/getopt1.c, lib/getopt.c, lib/getopt-cdefs.in.h, lib/getopt-core.h,
lib/getopt-ext.h, lib/getopt.in.h, lib/getopt_int.h,
lib/getopt-pfx-core.h, lib/getopt-pfx-ext.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/Makefile.am, lib/malloca.c, lib/malloca.h, lib/malloc.c,
lib/mbrtowc.c, lib/mbsinit.c, lib/memchr.c, lib/memchr.valgrind,
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/_Noreturn.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/quotearg.c, lib/quotearg.h,
lib/quote.h, lib/rawmemchr.c, lib/rawmemchr.valgrind,
lib/secure_getenv.c, lib/size_max.h, lib/sleep.c, lib/stat.c,
lib/stat-time.h, lib/stat-w32.c, lib/stat-w32.h, lib/stdalign.in.h,
lib/stdbool.in.h, lib/stddef.in.h, lib/stdint.in.h, lib/stdio-impl.h,
lib/stdio.in.h, lib/stdlib.in.h, lib/stpcpy.c, lib/strcasecmp.c,
lib/strchrnul.c, lib/strchrnul.valgrind, lib/streq.h, lib/strerror.c,
lib/strerror-override.c, lib/strerror-override.h, lib/string.in.h,
lib/strings.in.h, lib/stripslash.c, lib/strncasecmp.c, lib/strndup.c,
lib/strnlen.c, lib/strverscmp.c, lib/sysexits.in.h, lib/sys_stat.in.h,
lib/sys_time.in.h, lib/sys_types.in.h, lib/sys_wait.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.h, lib/xalloc-oversized.h, lib/xmalloc.c, lib/xsize.h,
m4/00gnulib.m4, m4/absolute-header.m4, m4/alloca.m4, m4/argp.m4,
m4/codeset.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_h.m4, m4/fcntl-o.m4, m4/float_h.m4,
m4/fpending.m4, m4/getopt.m4, m4/getprogname.m4, m4/gettimeofday.m4,
m4/gnulib-cache.m4, m4/gnulib-common.m4, m4/gnulib-comp.m4,
m4/gnulib-tool.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/malloca.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/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/quotearg.m4, m4/quote.m4,
m4/rawmemchr.m4, m4/secure_getenv.m4, m4/size_max.m4, m4/sleep.m4,
m4/ssize_t.m4, m4/stat.m4, m4/stat-time.m4, m4/stdalign.m4,
m4/stdbool.m4, m4/stddef_h.m4, m4/stdint_h.m4, m4/stdint.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/sysexits.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/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/cdefs.h, lib/glthread/lock.c, lib/glthread/lock.h,
lib/glthread/threadlib.c, lib/libc-config.h, lib/mkdir.c,
lib/windows-initguard.h, lib/windows-mutex.c, lib/windows-mutex.h,
lib/windows-once.c, lib/windows-once.h, lib/windows-recmutex.c,
lib/windows-recmutex.h, lib/windows-rwlock.c, lib/windows-rwlock.h,
m4/host-cpu-c-abi.m4, m4/__inline.m4, m4/lib-ld.m4, m4/lib-link.m4,
m4/lib-prefix.m4, m4/lock.m4, m4/mkdir.m4,
m4/pthread_rwlock_rdlock.m4, m4/std-gnu11.m4, m4/threadlib.m4,
tools/config.rpath: New files.

* spot/ltsmin/ltsmin.hh: Here.

Bison 3.0 was released in 2013, and the current Debian stable (buster)
has version 3.3.2.

* m4/bison.m4: Remove -Wno-precedence and -Wno-empty-rule, keep
-Wno-deprecated just to protect from future deprecation warnings that
would be interpreted as errors.
* spot/parseaut/parseaut.yy, spot/parsetl/parsetl.yy: Use %empty
rules, prefer %precedence over %nonassoc, update %error-versbose and
%name-prefix to their more modern equivalent.
* spot/misc/trival.hh (maybe): Mark this function as noexcept to
please the compiler while compiling the parsers.

Fixes #391.

* spot/twa/twagraph.hh: Here.
* tests/core/dualize.test, tests/python/except.py: New tests.
* NEWS: Mention the bug.

* doc/org/concepts.org, doc/org/ltl2tgba.org, doc/org/ltldo.org: Here.

* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.8.1.

* bin/autcross.cc, bin/ltlcross.cc: Implement it.
* doc/org/autcross.org, doc/org/ltlcross.org, NEWS: Document it.
* doc/org/spot.css: Add colors for Makefile snippets.
* tests/core/autcross4.test, tests/core/ltlcross3.test,
tests/core/ltlcrossce.test: Add test cases.

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=91184

* .gitlab-ci.yml (debian-gcc-snapshot): Add allow_failure=true.

* doc/org/init.el.in: Set gnutls-algorithm-priority when needed.
* NEWS: Mention the issue.

std::cerr will flush after each operator<< by default, so it's simpler
to use \n instead of std::endl, especially if we can merge \n into the
previous string.  Ideally we should prefer \n for std::cout as well,
but there are reasonable cases where we want to call std::endl there,
so it's hard to enforce.

* tests/sanity/style.test: Diagnose occurrences of cerr.*<<.*endl.
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, bin/ltlsynt.cc,
spot/tl/formula.cc, spot/twa/bdddict.cc, tests/core/checkpsl.cc,
tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
tests/core/length.cc, tests/core/ltlrel.cc, tests/core/parity.cc,
tests/core/randtgba.cc, tests/core/reduc.cc, tests/core/syntimpl.cc,
tests/ltsmin/modelcheck.cc: Fix them.

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
this.
* NEWS, bin/man/genltl.x, doc/spot.bib: Add documentation.
* tests/core/genltl.test, tests/core/ltlfilt.test: Add some tests.