Commit graph

4936 commits

Author SHA1 Message Date
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
Alexandre Duret-Lutz
36b5b76ca5 python: improve formating of double-quoted AP in MathJax
* python/spot/impl.i: Move the rendering code...
* python/spot/__init__.py: ... here, and ajust it for MathJax.
* tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb: Adjust
expected results.
2018-05-15 17:27:21 +02:00
Alexandre Duret-Lutz
965d0ed6b7 * doc/org/tut04.org: Show are_equivalent(). 2018-05-15 16:17:00 +02:00
Alexandre Duret-Lutz
6a808492c1 python: implicit str->formula conversion
* python/spot/impl.i, python/spot/__init__.py: Implement it.
* NEWS: Mention it.
* tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/ltsmin-pml.ipynb, tests/python/stutter-inv.ipynb,
doc/org/tut02.org: Modernize.
2018-05-15 16:16:11 +02:00
Alexandre Duret-Lutz
5c1d9c492c dot: add option K
* spot/twaalgos/dot.cc: Here.
* NEWS, bin/common_aoutput.cc: Mention it.
* tests/python/ltsmin-pml.ipynb: Use it.
* tests/python/ipnbdoctest.py: Work around some graphviz
version differences.
2018-05-14 18:07:58 +02:00
Alexandre Duret-Lutz
75b5449ac3 org: fix and improve hoa.org
* doc/org/hoa.org: Here.
2018-05-14 16:33:28 +02:00
Alexandre Duret-Lutz
9361bd9401 python: add a show= keyword to display_inline()
* python/spot/jupyter.py: Here.
* tests/python/alternation.ipynb: Use it.
* NEWS: Mention the above notebook as usage example.
2018-05-12 09:23:05 +02:00
Alexandre Duret-Lutz
60898b6d22 dot: support 'u'
* spot/twaalgos/dot.cc: Implement it.
* bin/common_aoutput.cc, NEWS: Mention it.
* tests/python/alternation.ipynb: Test it.
2018-05-12 09:23:05 +02:00
Maximilien Colange
13c227a099 remove a useless exception
* spot/twaalgos/split.cc: split_2step does work with any acceptance
  condition
* spot/twaalgos/split.hh: typo
2018-05-04 20:06:33 +02:00
Alexandre Duret-Lutz
26f5e93e90 * tests/python/stutter-inv.ipynb: Remove debug print. 2018-05-04 17:44:09 +02:00
Alexandre Duret-Lutz
9f30b9244f org: add link to stutter checks and autcross on main page
* doc/org/index.org: Here.
2018-05-04 17:28:27 +02:00
Alexandre Duret-Lutz
d6f9618172 introduce containement checks functions
* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc: New files.
* spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
* python/spot/__init__.py: Also attach these functions as methods,
and support string arguments.
* tests/python/contains.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* bin/autfilt.cc, tests/python/streett_totgba.py, tests/python/sum.py,
tests/python/toweak.py: Use the new function.
2018-05-04 17:18:49 +02:00
Alexandre Duret-Lutz
58d9a12495 python: introduce spot.jupyter.display_inline()
* python/spot/jupyter.py: New file.
* python/Makefile.am: Add it.
* tests/python/product.ipynb: Use it.
* NEWS: Mention it.
2018-05-04 15:27:51 +02:00
Alexandre Duret-Lutz
b0b431a5a4 improve gf_guarantee_to_ba
* spot/twaalgos/gfguarantee.cc: Combine the last letter read
with the first one of the next pass when doing transition-based
acceptance.  Also move the initial states to the source of any
accepting transition if the input is deterministic.
* tests/core/ltl2tgba2.test, tests/core/satmin.test,
tests/python/stutter-inv.ipynb: Reduce expected sizes of a few
automata.
2018-05-03 20:05:50 +02:00
Maximilien Colange
1fdc32f9bb ltlsynt: improve construction of turn-based games
Improve the way transitions are duplicated when preparing the turn-based
game for synthesis. The resulting arena should now be deterministic on
nodes owned by the environment. Also move the code to another file, so
that it is easier to test (e.g. in Python).

* bin/ltlsynt.cc: move the code
* spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
  implement the improvements
* tests/Makefile.am, tests/python/split.py: test it
* tests/core/ltlsynt.test: update existing tests to reflect the changes
2018-04-30 14:41:52 +02:00
Alexandre Duret-Lutz
4fbcdaca91 print_dot: correctly escape \n in html output
* spot/misc/escape.cc (escape_html): Handle \n.
* tests/core/readsave.test: Test it.
* NEWS: Mention the fix.
2018-04-27 15:46:56 +02:00
Maximilien Colange
9d34c1f500 fix parity game printing
* spot/misc/game.cc: a state could be printed several times
* tests/core/ltlsynt.test: update tests
2018-04-23 14:38:45 +02:00
Maximilien Colange
9698363ef5 parity game: various improvements
Zielonka algorithm has been fixed and optimized.
It also now computes the strategy for both players.

* bin/ltlsynt.cc: Update calls to parity_game::solve()
* spot/misc/game.cc, spot/misc/game.hh: Implement the changes
2018-04-23 11:51:12 +02:00
Maximilien Colange
0e29d30d1b ltlsynt: fix the construction of the arena
* bin/ltlsynt.cc: implement it
* tests/core/ltlsynt.test: update tests
2018-04-23 11:51:12 +02:00
Maximilien Colange
5d80cc556c Add a verbose option to ltlsynt
* bin/ltlsynt.cc: implement it
2018-04-23 11:51:02 +02:00
Alexandre Duret-Lutz
bc2fa1a2a3 * tests/python/satmin.ipynb: Remove a debug statement. 2018-04-20 16:55:20 +02:00
Alexandre Duret-Lutz
c2e177ee09 Merge branch 'master' into next 2018-04-20 08:06:33 +02:00
Alexandre Duret-Lutz
fea122f7ba Bump version to 2.5.3.dev
* NEWS, configure.ac: Here.
2018-04-20 07:59:33 +02:00
Alexandre Duret-Lutz
8de9f6aa26 Release Spot 2.5.3
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2018-04-20 07:57:01 +02:00