alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
4624 commits 6 branches 0 tags 36 MiB
Commit graph

4624 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
80621557b2 Release Spot 2.4 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2017-09-05 21:08:48 +02:00
Alexandre Duret-Lutz
f3ef225334 * NEWS: Add a missing entry. 2017-09-05 19:15:50 +02:00
Clément Gillard
ad3588420c fix typos and indentation 
* bin/autfilt.cc, python/spot/__init__.py, spot/twa/twa.hh,
spot/twa/twaproduct.cc, spot/twaalgos/couvreurnew.cc,
tests/python/bugdet.py: Here.
 2017-09-05 13:23:01 +02:00
Alexandre Duret-Lutz
552afb9d55 * NEWS: Some typos en cleanup. 2017-09-05 11:23:23 +02:00
Alexandre Duret-Lutz
bc626788af dot: make 'x' compatible with 'b'/'r'/'R' 
* spot/twaalgos/dot.cc: Implement.
* doc/org/oaut.org: Illustrate.
* tests/core/dot2tex.test: Add some limited tests.
 2017-09-05 07:45:11 +02:00
Alexandre Duret-Lutz
290d7b56fb * doc/org/oaut.org: Missing word. 2017-09-04 19:57:40 +02:00
Alexandre Duret-Lutz
e452e09ff7 bin: make --stats and --format synonyms 
* bin/common_output.cc: Make --stats an alias of --format.
* bin/common_aoutput.cc: Make --format an alias of --stats.
* tests/core/acc2.test, tests/core/format.test: Test these aliases.
* NEWS: Mention this.
 2017-09-04 17:42:13 +02:00
Alexandre Duret-Lutz
f726152ebd org: fix one example 
* doc/org/genaut.org: Output the result for the last example.
 2017-09-04 17:23:07 +02:00
Alexandre Duret-Lutz
e7df182a30 gen: rename KS_COBUCHI to KS_NCA for consistency 
* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.
 2017-09-03 15:47:27 +02:00
Alexandre Duret-Lutz
6cd6802ace simplify: rewrite GF(a & Fb) as G(Fa & Fb) 
This addresses part of #35, and is just a generalization of the rules
from 646c5170 for #263 (hence, no new documentation).

* spot/tl/simplify.cc: Implement this.
* tests/core/reduccmp.test: Add test cases.
* tests/core/stutter-tgba.test: Adjust to expect smaller automata.
 2017-09-02 20:02:20 +02:00
Alexandre Duret-Lutz
e8527d5ae9 Improve simplification of expr[*0..1] 
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
 2017-09-02 16:35:18 +02:00
Alexandre Duret-Lutz
190d4cfaf1 ltl2tgba_fm: implement a small optimization 
Fixes #277.

* spot/twaalgos/ltl2tgba_fm.cc: Improve the translation of f U g
when f is universal.  Suggested by Maximilien Colange.
* tests/core/ltl2tgba.test: Test it.
 2017-09-02 14:48:52 +02:00
Alexandre Duret-Lutz
42abcf8559 genltl: add --gxf-and and --fxg-or 
As suggested in #263.

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
these options.
* tests/core/genltl.test: Use them.
* NEWS: Mention them.
 2017-09-02 11:51:54 +02:00
Alexandre Duret-Lutz
646c5170ed simplify: some new simplification rules 
For #263, reported by Mikuláš Klokočka.

G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
* tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
smaller automata.
* THANKS: Add Mikuláš.
 2017-09-02 11:27:04 +02:00
Alexandre Duret-Lutz
cd6f1c2c3e get rid of some unnecessary code 
* spot/priv/enumflags.hh: Delete.
* spot/priv/Makefile.am, debian/copyright: Adjust.
* spot/twaalgos/remfin.cc: Replace the complex enum
definition by a plain enum that is almost not used.
 2017-09-01 22:09:52 +02:00
Alexandre Duret-Lutz
15cc7301cc remove_fin: apply Rabin conversion before Streett 
* spot/twaalgos/remfin.cc (remove_fin_impl): Apply the Rabin strategy
before the Streett one.
 2017-09-01 22:09:52 +02:00
Alexandre Duret-Lutz
f7ba490898 streett_to_generalize_buchi: fix handling of SCCs without Fin 
The generalization to Streett-like of 7b5b8f34 was incomplete for this
case.  Thanks to František Blahoudek for reporting the bug.
Fixes #279.

* spot/twaalgos/totgba.cc (streett_to_generalized_buchi): Here.
* tests/core/remfin.test: Add more tests.
 2017-09-01 22:09:49 +02:00
Alexandre Duret-Lutz
7b9cedc697 common_trans: leave the shell handle commands containing = in arg0 
This is probably an environment variable definition.

* bin/common_trans.cc: Here.  A use-case appears in the test of the
next patch.
 2017-09-01 20:20:36 +02:00
Alexandre Duret-Lutz
fbb9e4374e dot: add x option for dot2tex 
* spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
conditions.
* spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
a bit to limit duplication.
* tests/core/dot2tex.test: New test case (requires dot2tex).
* tests/Makefile.am: Add dot2tex.test.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/automata-io.ipynb: Adjust expected output.
* NEWS, doc/org/oaut.org: Mention the new option.
 2017-08-31 19:50:08 +02:00
Alexandre Duret-Lutz
b242122ce8 dot: add option 'A' to disable 'a' 
This way in 2.5 we can make 'a' the default, and tell people to use
SPOT_DOTDEFAULT=A if they want the old behavior in both 2.4 and 2.5.

* spot/twaalgos/dot.cc: Implement the option.
* NEWS, bin/common_aoutput.cc: Mention it.
* tests/core/readsave.test: Test it.
 2017-08-30 16:15:53 +02:00
Alexandre Duret-Lutz
205294c2c2 dot: display Rabin-like and Streett-like acceptances 
* spot/twaalgos/dot.cc (print_acceptance_for_human): Add Rabin-like
and Streett-like checks.
* tests/core/sccdot.test, tests/python/decompose.ipynb,
tests/python/randaut.ipynb, tests/core/alternating.test: Adjust.
 2017-08-30 16:15:48 +02:00
Alexandre Duret-Lutz
ed361bb0a9 org: add remark about "%h" 
* doc/org/csv.org: Mention that %h must be double-quoted in CSV output.
 2017-08-29 14:02:28 +02:00
Maximilien Colange
f58f61b302 Improve tests of spot.dualize() 
* tests/python/dualize.py: test that an automaton and its dual have
  complementary languages.
 2017-08-29 11:57:06 +02:00
Maximilien Colange
1b2f2a79c1 Fix a bug in spot.complete() 
spot.complete() could complete an empty co-Büchi automaton into an
automaton accepting everything.

* NEWS: Document it
* spot/twaalgos/complete.cc: Fix it
* tests/core/complete.test, tests/core/prodor.test: Test it
 2017-08-28 17:55:32 +02:00
Maximilien Colange
eb91ecf66f Typos 
* NEWS, doc/org/concepts.org, doc/org/hierarchy.org,
  spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh,
  spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos
 2017-08-28 17:54:21 +02:00
Alexandre Duret-Lutz
f5dce597c6 switch to C++14 compilation 
* configure.ac: Compile in C++14 by default and rename
--enable-c++14 as c++17.
* doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
NEWS, README: Adjust all mentions of C++11.
* spot/twaalgos/stats.hh: Use std::make_unique.
 2017-08-22 18:21:49 +02:00
Alexandre Duret-Lutz
7f42782701 [buddy] switch to C++14 compilation 
* configure.ac: Here.  Rename --enable-c++14 into --enable-c++17.
 2017-08-22 18:21:46 +02:00
Alexandre Duret-Lutz
b7d54c8b90 mention autcross in arch.tex 
* doc/org/arch.tex: Add autcross.
* tests/sanity/bin.test: Make sure all binaries appear in arch.tex.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
1cc45b2413 dot: display acceptance names 
* spot/twaalgos/dot.cc: Display common acceptance names.
* NEWS: Mention the change.
* doc/org/oaut.org: Adjust text.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
f8ef06acc6 acc: fix operator| and operator& 
Bug introduced in abe2c08b, visible in tests/python/product.ipynb,
and tests/python/acc_cond.ipynb.

* spot/twa/acc.hh: fix operator| and operator&.
* tests/python/acc_cond.ipynb: Adjust test case.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
2e8a67027f hierarchy: avoid sbacc() 
* spot/tl/hierarchy.cc (is_recurrence): Do not request state-based
acceptance, now that the Rabin->DBA conversionn works on
transition-based acceptance as well.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
a3f5834249 org: update hierarchy 
* doc/org/hierarchy.org: Update with small typos, and
notes about tra2tba.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
e3b30e6d8e remfin: remove some unnecessary copies 
* spot/twaalgos/remfin.cc (tra_to_tba, is_scc_tba_type): Here.
 2017-08-17 15:21:59 +02:00
Thomas Medioni
4b5606e742 to_weak_alternating(): fixes a bug on generalized co-Büchi automata 
Fixes #278. Also adds a test ensuring non-regression.

* spot/twaalgos/toweak.cc: Fixes the bug.
* tests/python/toweak.py: Add a test case.
 2017-08-17 13:07:20 +02:00
Alexandre Duret-Lutz
df04c715cf remove_fin: fix incorrect state-based output 
* spot/twaalgos/remfin.cc: If no Inf set is used, set sbacc early so
that it is used in the algorithm.
* tests/core/remfin.test: Add more tests.
* NEWS: Mention the bug.
 2017-08-09 18:25:36 +02:00
Thomas Medioni
30a68d288b Fix typo automatons -> automata 
* NEWS, spot/twaalgos/dualize.cc, spot/twaalgos/dualize.hh,
  spot/twaalgos/langmap.cc, spot/twaalgos/sum.hh,
  tests/python/streett_totgba.py: Fixes typo.
 2017-08-09 15:51:23 +02:00
Alexandre Duret-Lutz
f0161618ca * spot/twaalgos/simulation.cc (print_partition): Improve. 2017-08-08 15:00:33 +02:00
Alexandre Duret-Lutz
59c0f08278 * tests/core/optba.test: Use set -x. 2017-08-08 15:00:33 +02:00
Alexandre Duret-Lutz
80d50c5665 gnulib: upgrade to today's version 
* tools/snippet/_Noreturn.h, tools/snippet/c++defs.h,
tools/snippet/arg-nonnull.h, tools/snippet/warn-on-use.h: Rename to...
* lib/_Noreturn.h, lib/c++defs.h, lib/arg-nonnull.h,
lib/warn-on-use.h: ... these.
* lib/filename.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/localtime-buffer.c, lib/localtime-buffer.h, lib/malloca.c,
lib/malloca.h, lib/malloca.valgrind, lib/stat-w32.c, lib/stat-w32.h,
m4/eealloc.m4, m4/localtime-buffer.m4, m4/malloca.m4: New files.
* lib/argp-help.c, lib/argp-parse.c, lib/error.c, lib/float.in.h,
lib/getopt1.c, lib/getopt.c, lib/getopt.in.h, lib/getopt_int.h,
lib/gettext.h, lib/gettimeofday.c, lib/intprops.h, lib/isatty.c,
lib/limits.in.h, lib/localcharset.c, lib/Makefile.am, lib/mbrtowc.c,
lib/mbsinit.c, lib/msvc-nothrow.c, lib/quotearg.c, lib/stat.c,
lib/stdalign.in.h, lib/stdint.in.h, lib/string.in.h,
lib/sys_stat.in.h, lib/sys_types.in.h, lib/tempname.c, lib/time.in.h,
lib/unistd.in.h, lib/vasnprintf.c, lib/wchar.in.h, lib/wctype.in.h,
lib/xalloc.h, lib/xalloc-oversized.h, m4/fcntl-o.m4, m4/float_h.m4,
m4/getopt.m4, m4/gettimeofday.m4, m4/gnulib-common.m4,
m4/gnulib-comp.m4, m4/include_next.m4, m4/largefile.m4, m4/lstat.m4,
m4/mbrtowc.m4, m4/memchr.m4, m4/mkstemp.m4, m4/printf.m4, m4/sleep.m4,
m4/stat.m4, m4/stdalign.m4, m4/stdint.m4, m4/strerror.m4,
m4/string_h.m4, m4/sys_stat_h.m4, m4/sys_time_h.m4, m4/sys_types_h.m4,
m4/time_h.m4, m4/unistd_h.m4, m4/wchar_h.m4, m4/wctype_h.m4,
m4/wint_t.m4: Update.
 2017-08-08 15:00:11 +02:00
Alexandre Duret-Lutz
aa8cf6ac92 typos in NEWS 
* NEWS: Fix them.
 2017-08-04 17:01:03 +02:00
Alexandre Duret-Lutz
55113ed1d0 fix error message in exception 
* spot/twaalgos/alternation.cc: Here.
 2017-08-04 17:01:03 +02:00
Alexandre Duret-Lutz
1cf5778faa stats: allow counting complete SCCs 
* bin/common_aoutput.cc, NEWS: Update documentation.
* spot/twaalgos/stats.cc: Honor c and C.
* tests/core/alternating.test: Test it.
 2017-08-04 17:01:03 +02:00
Alexandre Duret-Lutz
223b0c6a9e is_weak_scc and friend: make them work for alternating automata 
* spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh,
spot/twaalgos/mask.cc, spot/twaalgos/mask.hh: Adjust to
work with alternating automata.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh
(determine_unknown_acceptance): Do not complain about
not supporting alternating automata if there is not
indeterminate acceptance.
* spot/twaalgos/stats.cc: Fix a bug were %[iw]c was
read as %[iww]c.
* tests/core/alternating.test: Test is_inherently_weak_scc() and
is_weak_scc().
* python/spot/impl.i: Add missing python bindings
for isweakscc.hh.
 2017-08-04 15:12:27 +02:00
Alexandre Duret-Lutz
e041db6101 dot: extend the palette from 9 to 16 colors 
Let's close #212 even if this does not cover the 32 sets.

* spot/twaalgos/dot.cc: Change the palette.
* doc/org/autfilt.org, NEWS: Adjust documentation.
* tests/core/alternating.test, tests/core/readsave.test,
tests/core/tgbagraph.test, tests/python/_altscc.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/gen.ipynb,
tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/piperead.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/word.ipynb: Adjust
test cases.
 2017-08-03 14:32:11 +02:00
Alexandre Duret-Lutz
85c23202b7 g++wrap: make it work with --enable-glibcxx-debug 
* doc/org/g++wrap.in: Honor CPPFLAGS.
 2017-08-02 15:26:35 +02:00
Alexandre Duret-Lutz
ab42075dce formula: hide throw statements from inline methods 
* spot/tl/formula.hh: Move all throw statements behind
some [[noreturn]] report...() methods...
* spot/tl/formula.cc: ... defined here.  This makes the methods
shorter and helps their inlining.  Incidentally, this also removes the
uninitialized read that weirdly occurs when _GLIBCXX_DEBUG is on, as
observed with #184, but I do not know why.
 2017-08-02 11:31:47 +02:00
Alexandre Duret-Lutz
6b96aa4f27 is_unabiguous: fix incorrect vector usage 
* spot/twaalgos/isunamb.cc: Actually set the size of the vector
instead of just reserving the size.
 2017-08-01 18:04:07 +02:00
Alexandre Duret-Lutz
eb8df6d72c parseaut: allow the univ-branch diagnostics to be ignored 
* spot/parseaut/parseaut.yy: Check the SPOT_HOA_TOLERANT variable.
* tests/core/ltl3ba.test, tests/core/parseaut.test: Adjust test cases.
* NEWS, bin/man/spot-x.x: Mention SPOT_HOA_TOLERANT.
 2017-08-01 18:03:06 +02:00
Alexandre Duret-Lutz
d3607a7ce3 hoa: fix I/O of determinism 
Fixes #212.

* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
exist-branch, and adjust printer to the 1.1 semantics.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/det.test, tests/core/explsum.test,
tests/core/parseaut.test, tests/core/readsave.test,
tests/core/sbacc.test, tests/core/tgbagraph.test,
tests/python/alternating.py, tests/python/dualize.py: Adjust test
cases.
* NEWS: Mention the change.
 2017-07-31 22:33:56 +02:00
Alexandre Duret-Lutz
0cf250d839 bin: introduce autcross 
Fixes #252.

* NEWS: Mention it.
* bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
files.
* bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
doc/Makefile.am: Add them.
* bin/autfilt.cc: Use is_universal() instead of is_deterministic().
* bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
ltlcross, ltldo and autcross.
* tests/core/autcross.test, tests/core/autcross2.test: New files.
* tests/Makefile.am: Add them.
* tests/core/dra2dba.test, tests/core/sbacc.test,
tests/core/streett.test: Use autcross.
 2017-07-28 10:33:14 +02:00