Commit graph

3894 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
ed254ea19f man: fix an apostrophe
* bin/man/ltl2tgba.x: Fix apostrophe.  It was appearing incorrectly in
the generated html pages.
2016-09-05 14:01:44 +02:00
Alexandre Duret-Lutz
cc761870c2 kripkegraph: fix g++ warning
Test the output of down_cast before using it.  This
used to generate a warning when crosscompiling
for mingw with g+++ 6.1.1

* spot/kripke/kripkegraph.hh: Here.
2016-09-04 17:25:24 +02:00
Alexandre Duret-Lutz
ca6435d847 help2man: update to 1.47.4
Also disable i18n because that seems to be causing many problem to Mac
users building Spot for git and not knowing how to install
Locale::gettext.

* tools/help2man: Update from upstream, plus the two changes from
2b4cf8e7cb and
f7b65001e9.
* bin/man/Makefile.am: Remove the -L flag.
2016-09-03 19:54:08 +02:00
Alexandre Duret-Lutz
2dfe429447 org: fix an example input
* doc/org/autfilt.org: Remove incorrect acc-name.
2016-08-19 14:30:05 +02:00
Alexandre Duret-Lutz
571f0112ab bin: add options for --stats=%c
* spot/twaalgos/stats.cc: Implement options.
* bin/common_aoutput.cc, NEWS: Document them.
* tests/core/format.test: Add some quick tests.
2016-08-17 16:35:00 +02:00
Alexandre Duret-Lutz
4f0a630dbc stats: preparatory change of the implementation of %c
This now holds the scc_info while processing the %c sequence, so that
using options we will soon be able to specify which SCC to count.

* spot/twaalgos/stats.hh, spot/twaalgos/stats.cc (printable_scc_info):
New class.
(state_printer): Use it for %c.
* spot/misc/formater.hh: Add move assignment.
* bin/common_aoutput.hh, bin/common_aoutput.cc: Use printable_scc_info
for %C.
* tests/core/format.test: Add a quick test case to make sure nothing
changed.
2016-08-17 14:49:28 +02:00
Alexandre Duret-Lutz
70de1328d8 bin: hide the hoa_state_printer code
* bin/common_aoutput.hh (hoa_state_printer::hoa_state_printer,
hoa_state_printer::print): Move the definition...
* bin/common_aoutput.cc: ... here.
2016-08-17 13:42:13 +02:00
Alexandre Duret-Lutz
825332029c autfilt: implement %D, %N, %P, %W
* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement.
* tests/core/format.test: Test.
* NEWS: Mention.
2016-08-16 19:20:12 +02:00
Alexandre Duret-Lutz
926ffbf965 bin: %a,%b,%s format specs for LTL output
* NEWS: Mention those.
* bin/common_output.cc, bin/common_output.hh: Implement them.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update
--help.
* tests/core/format.test: New file.
* tests/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation.
2016-08-15 16:09:53 +02:00
Alexandre Duret-Lutz
0210080152 * spot/tl/length.hh: Fix comment. 2016-08-15 14:57:30 +02:00
Alexandre Duret-Lutz
e97ea5fa74 bin: diagnose more write errors
* tests/core/full.test: New file.
* tests/Makefile.am: Add it.
* bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
bin/common_file.cc, bin/common_file.hh, bin/genltl.cc, bin/ltlcross.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Add diagnostics.
* NEWS: Mention the fix.
2016-08-14 18:18:20 +02:00
Alexandre Duret-Lutz
53e6640034 Bump version to 2.1.0a
* configure.ac, NEWS: Here.
2016-08-08 16:30:56 +02:00
Alexandre Duret-Lutz
78232df3bf Release Spot 2.1
* configure.ac, NEWS, doc/org/setup.org: Update version.
2016-08-08 13:23:18 +02:00
Alexandre Duret-Lutz
ca0d81b5d7 autfilt, dstar2tgba: add CSV input
Fixes #91.

* bin/autfilt.cc, bin/dstar2tgba.cc: Implement reading CSV files.
* bin/common_finput.cc: Fix comments.
* bin/common_aoutput.cc: Show %<, %> in help text.
* NEWS, doc/org/csv.org: Document it.
* tests/core/readsave.test: Add a short test case.
2016-08-08 13:18:50 +02:00
Alexandre Duret-Lutz
f423c424eb bin: --stats=%H --stats=%h
Part of #91.

* bin/common_aoutput.cc, bin/common_aoutput.hh: implement %H and %h.
* tests/core/readsave.test: Test them.
* NEWS: Mention it.
2016-08-08 12:41:36 +02:00
Alexandre Duret-Lutz
0d753048ce formater: add support for double-quoted fields
Part of #91.

* spot/misc/formater.cc, spot/misc/formater.hh: Here.
* bin/common_output.cc: Adjust automatic output format.
* doc/org/csv.org: Adjust.
* tests/core/lbt.test, tests/core/ltlfilt.test: More tests.
* NEWS: Mention the changes.
2016-08-08 10:53:33 +02:00
Alexandre Duret-Lutz
6ed0830f87 fix two minor issues reported by clang-analyzer
These are actually two events that should never happen, but let's just
make sure they do not.

* spot/tl/formula.cc: Add an assert.
* spot/twaalgos/emptiness.cc: Add an exception.
2016-08-07 19:45:01 +02:00
Alexandre Duret-Lutz
2b4cf8e7cb org: more typos and small fixups
* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/ltl2tgba.org, doc/org/oaut.org: Here.
* tools/help2man: Adjust regex for optional arguments.
2016-08-06 11:49:53 +02:00
Alexandre Duret-Lutz
ce7b9c5161 org: fix some automata rendering
The new ob-dot.el installed by 15ea2e66e8
makes all the sed escaping useless (and actually harmful).

* doc/org/ltl2tgta.org, doc/org/oaut.org: Fix those.
2016-08-05 20:47:33 +02:00
Alexandre Duret-Lutz
06d5aa5ea2 org: several typos
* doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut04.org, doc/org/tut10.org, doc/org/tut20.org,
doc/org/tut21.org, doc/org/tut50.org: Fix some typos and reword some
sentences.
2016-08-05 11:13:15 +02:00
Alexandre Duret-Lutz
14bee1ae7f implement conversion to GRA and GSA
Fixes #174.

* spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
(to_generalized_streett, to_generalized_rabin): New functions.
* spot/twa/acc.hh: Declare more methods as static.
* bin/autfilt.cc: Implement --generalized-rabin and
--generalized-streett options.
* NEWS: Mention these.
* tests/core/gragsa.test: New file.
* tests/Makefile.am: Add it.
2016-08-04 22:24:30 +02:00
Alexandre Duret-Lutz
736003057c * NEWS: Minor typos and reorganization. 2016-08-03 12:23:46 +02:00
Alexandre Duret-Lutz
51afd4adfe ltlcross: prefer execl("/bin/sh", ...) to execlp("sh", ...)
Fixes #98.

* bin/common_trans.cc: Here.
2016-08-02 14:24:08 +02:00
Alexandre Duret-Lutz
7524e05128 ltlcross: bypass the shell for simple command
For #98.

* bin/common_trans.cc: Here.
* NEWS: Mention it.
2016-08-02 14:24:05 +02:00
Alexandre Duret-Lutz
d2068bb1a0 sbacc: improve using SCCs and common marks
* spot/twaalgos/sbacc.cc: Here.
* tests/core/parseaut.test, tests/python/automata.ipynb: Adjust.
* tests/core/sbacc.test: Likewise + more tests.
* NEWS: Mention it.
2016-07-31 22:57:50 +02:00
Alexandre Duret-Lutz
d271dfd592 python: make it possible to modify edges during iteration
Reported by Laurent Xu.

* python/spot/impl.i: Fix the iterator to return pointers instead of
references.  Because references are ultimately copied.
* tests/python/automata.ipynb: Add test cases.
* NEWS: Mention it.
2016-07-29 16:09:54 +02:00
Alexandre Duret-Lutz
09c6393942 * NEWS: Typo. 2016-07-29 11:59:31 +02:00
Alexandre Duret-Lutz
59efe470ca ltlcross: show cross-comparison checks counterexamples
Part of #38.

* bin/ltlcross.cc: Implement it.
* NEWS: Mention it.
* doc/org/ltlcross.org: Adjust example.
* tests/core/ltlcrossce2.test: New test case.
2016-07-29 11:58:12 +02:00
Alexandre Duret-Lutz
f6c7ed54c7 update gnulib
This comes from gnulib 348402f2aac342bc925b7aaea9ee3cc353f427a9 plus
a custom patch to support compilation of arpg in C++11.

* lib/hard-locale.c, lib/hard-locale.h, m4/hard-locale.m4, m4/ltargz.m4:
New files.
* 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.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/codeset.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/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,
tests/core/randtgba.cc, tools/snippet/arg-nonnull.h,
tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: Update.
2016-07-29 10:59:21 +02:00
Alexandre Duret-Lutz
561672d3d7 lbtt: fix a memory leak detected by asan.
* spot/twaalgos/lbtt.cc: Here.
* NEWS: Mention it.
2016-07-27 20:10:51 +02:00
Alexandre Duret-Lutz
a9fc5d49d8 misc: fix some signed shifts
* spot/misc/intvcmp2.cc, spot/misc/intvcomp.cc: Here.
2016-07-27 19:47:34 +02:00
Alexandre Duret-Lutz
a7842ac47f tests: disable ltsmin tests if --disable-shared
* configure.ac (USE_LTSMIN): New.
* tests/Makefile.am: Use it.
2016-07-27 19:47:34 +02:00
Alexandre Duret-Lutz
8e69530023 [buddy] fix an undefined behavior
* src/prime.c (BitIsSet): Do not shift signed
int by 31 places; shift unsigned int instead.
2016-07-27 19:47:30 +02:00
Alexandre Duret-Lutz
fcd6783157 * doc/org/tut50.org: Simplify UML diagrams. 2016-07-27 16:21:37 +02:00
Alexandre Duret-Lutz
15ea2e66e8 org: show how to implement Kripke structures
* doc/org/tut51.org: New file.
* doc/org/tut.org, doc/Makefile.am, NEWS: Add it.
* elisp/ob-dot.el: New file, to work around old org-mode versions.
* elisp/README, elisp/Makefile.am: Add it.
2016-07-27 16:21:03 +02:00
Alexandre Duret-Lutz
6617538156 kripke: rename state_acceptance_conditions
* spot/kripke/kripke.cc, spot/kripke/kripke.hh,
spot/kripke/fairkripke.hh (state_acceptance_conditions): Rename as...
(state_acceptance_mark): ... this.
* NEWS: Mention it.
2016-07-27 11:13:06 +02:00
Alexandre Duret-Lutz
096edf227d * NEWS: Reword some entries. 2016-07-27 10:35:59 +02:00
Alexandre Duret-Lutz
64c7036660 active -Wsuggest-override where supported
* m4/gccwarn.m4: Add the option.
* bin/autfilt.cc, bin/common_output.hh, bin/dstar2tgba.cc,
bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, spot/kripke/kripke.hh,
spot/ltsmin/ltsmin.cc, spot/ta/ta.hh, spot/ta/tgtaproduct.hh,
spot/taalgos/dot.cc, spot/taalgos/reachiter.hh,
spot/taalgos/statessetbuilder.cc, spot/taalgos/stats.cc,
spot/twa/twaproduct.cc, spot/twaalgos/emptiness.cc,
spot/twaalgos/gtec/ce.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ndfs_result.hxx, spot/twaalgos/stats.hh,
spot/twaalgos/tau03opt.cc, tests/core/ngraph.cc: Add suggested override
qualifiers.
2016-07-27 10:30:10 +02:00
Alexandre Duret-Lutz
da464d8199 org: document explicit vs. on-the-fly
* doc/org/tut50.org: New file.
* doc/org/tut.org: Add it.
* NEWS: Mention it.
* doc/Makefile.am: Add tut50.org, and download plantuml.jar when needed.
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Activate plantum.
* HACKING: Mention the Java dependency.
2016-07-26 11:26:16 +02:00
Alexandre Duret-Lutz
d7d6b40926 minimize_wdba: fix nondeterministic execution
Fixes core/readsave.test and python/automata.ipython
with gcc-snapshot (future gcc 7).

* spot/twaalgos/minimize.cc: Here.
* NEWS: Mention the change.
* tests/core/acc_word.test: Adjust test case.
2016-07-25 14:02:40 +02:00
Alexandre Duret-Lutz
20cf43b3ea use SPOT_ASSERT instead of assert
For #184.

* spot/graph/graph.hh, spot/kripke/kripkegraph.hh,
spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/fixpool.hh,
spot/misc/mspool.hh, spot/misc/timer.hh, spot/tl/formula.hh,
spot/twa/acc.hh, spot/twa/taatgba.hh, spot/twa/twa.hh,
spot/twa/twagraph.hh, spot/twaalgos/emptiness_stats.hh,
spot/twaalgos/mask.hh, spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.hh: Replace
assert() by SPOT_ASSERT(), or an exception, or nothing, depending
on the case.
* tests/sanity/style.test: Flag all asserts in headers.
* HACKING: Discuss assertions.
2016-07-24 23:26:59 +02:00
Alexandre Duret-Lutz
9f7bf5ab2d configure: support --enable-glibgxx-debug
Part of #184.

* m4/devel.m4 (adl_ENABLE_GLIBCXX_DEBUG): New macro.
* configure.ac: Use it.
* README: Mention it.
* spot/twa/acc.cc: Fix a small issue found with this
option.
2016-07-24 00:07:04 +02:00
Alexandre Duret-Lutz
1a5de86c1e * spot/tl/formula.hh: Fix some comments. 2016-07-24 00:02:34 +02:00
Alexandre Duret-Lutz
71e2490643 twa: rename twa::succ_iterable into internal::twa_succ_iterable
* spot/twa/twa.hh: Here.
* NEWS: Mention the change.
2016-07-22 14:14:23 +02:00
Alexandre Duret-Lutz
7534f62dba org: add autfilt decoration examples
* doc/org/autfilt.org: Here.
* doc/org/hoa.org: Add a link to it.
* bin/autfilt.cc: Typo.
2016-07-20 11:22:20 +02:00
Alexandre Duret-Lutz
dd6875d5fe bin: overhaul default input selection
If no input have been specified, and the standard input is not a tty all
tools now default to reading it.  If standard input is a tty, all tools
display an error message.  Additionally, - is now a shorthand for -F- in
all tools.

* NEWS: Summarize this.
* bin/common_finput.cc, bin/common_finput.hh (check_no_formulas,
check_no_automaton): New functions that implement the above istty()
logic.
* bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc,
bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function,
and recognize '-' if it was not the case.
* tests/core/acc_word.test, tests/core/ltldo.test,
tests/core/minusx.test, tests/core/readsave.test,
tests/core/unambig.test: Adjust some tests to exercise this.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/oaut.org: Adjust the documentation and simplify some
examples.
2016-07-19 21:55:12 +02:00
Alexandre Duret-Lutz
abff7eba8e simplifier: new PSL simplifications
{e[*0..j]}<>->f = {e[*1..j]}<>->f
{e[*0..j]}[]->f = {e[*1..j]}[]->f

Fixes #81.

This required a small change to the bounded-star-normal-form to prevent
infinite recursion.

* spot/tl/simplify.cc: Implement these rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test: Add tests, and adjust others.
* tests/core/unambig.test: Replace formula that used to generated an
ambiguous automaton, but now generates a deterministic one.
2016-07-19 17:57:16 +02:00
Alexandre Duret-Lutz
d5b2de7fa8 simplifier: new LTL simplifications
if e is pure eventuality and g => e, then e U g = Fg
if u is purely universal and u => g, then u R g = Gg

Fixes #93.

* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test: Adjust.
2016-07-19 16:02:19 +02:00
Alexandre Duret-Lutz
e37f62dc75 python: have %%dve and %%pml honor SPOT_TMPDIR and TMPDIR
* python/spot/aux.py (tmpdir): New context manager.
* python/spot/ltsmin.i: Use it for the two magics.
* NEWS: Mention this.
2016-07-19 14:23:27 +02:00
Alexandre Duret-Lutz
b136b81c6d new test case to improve coverage stats
The streett_to_generalized_buchi() function was not tested unless
ltl2dstar is installed.

* tests/core/streett.test: New file.
* tests/Makefile.am: Add it.
2016-07-19 13:35:47 +02:00