GitLab

* src/bddop.c: Avoid the first recursion when it is obvious that the
second will fail.

* src/bddop.c (bdd_implies): Fix documentation.

Related to #188.  This is a third fix that independently
makes `'utfilt --is-unambiguous -q smaller.hoa' instantaneous.

* spot/twaalgos/remfin.cc: Clean the received automaton if
necessary.
* bin/autfilt.cc: No need to call cleanup_acceptance_here() before
remove_fin() anymore.
* tests/core/remfin.test: Add an additional test.
* NEWS: Mention the change.

* bin/autfilt.cc, spot/twaalgos/isweakscc.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sccinfo.cc: Use mask_keep_accessible_states instead of
mask_keep_states.

* src/kernel.c: The initialization code of the BDD cache was
awfully slow due to multiple references to global variables.

As observed in #188, the smaller.hoa automaton is made only of
1-state/1-self-loop SCCs, for which calling remove_fin is a complete
waste of time.  This patch alone (i.e., without the other changes
suggested by #188) improves the run time of

% autofilt -q --is-unambiguous smaller.hoa

from 38s to 0.05s.

* spot/twaalgos/sccinfo.cc: If a single-state SCC has undeterminate SCC
and only one self-loop, then it is necessarily rejecting.
* NEWS: Mention the change.

Avoid calling scc_info::determine_unknown_acceptance on the product, as
suggested in #188.

* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite.
* tests/core/unambig.test: Add the automaton from #188.
* NEWS: Mention the improved function.
* spot/twaalgos/mask.cc,
spot/twaalgos/mask.hh (mask_keep_accessible_states): New function.

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

In order to match the tarballs of the FORTE'14 paper.

* bench/dtgbasat/stats.sh, bench/dtgbasat/README: Here.

* spot/twaalgos/dot.cc: Rearrange options to speed up their
initialization and avoid an "uninitialized read" error from valgrind
when compiling with clang-3.9.  The uninitialized read is still a bit
misterious to me; valgrind was complaining about opt_shape_ who is
actually initialized in the code.  However looking into the assembly
code generated revealed that all consecutive 0/false values were
initialized together, so this patch reorganize the options to encourage
that.  Also the palette was copied over for each call to print_dot(), so
this is now declared statically.

* bench/dtgbasat/formulas: Typo.
* NEWS: Mention the fix.
* AUTHORS: Add Alexandre.

Alexandre GBAGUIDI AISSE authored Sep 21, 2016 and Alexandre Duret-Lutz committed Oct 13, 2016

* bench/dtgbasat/formulas: Fix bin's path.
* bench/dtgbasat/prepare.sh: Fix bin's path & ltl2tgba@-sD option.
* bench/dtgbasat/stats.sh: Fix bin's path.
* bench/dtgbasat/stat.sh: Fix bin's path, ltl2tgba@-sD option

Suggested by František Blahoudek.

* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.

Report from František Blahoudek.

* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.

Etienne Renault authored Oct 10, 2016 and Alexandre Duret-Lutz committed Oct 10, 2016

* NEWS, python/spot/ltsmin.i: here.

Fix a5d6aa25.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Use
-Djava.awt.headless=true, not -Djava.awt.headless.

* m4/gccwarn.m4: Here.

* NEWS: Mention the fix.
* HACKING: Mention the new macro.
* spot/misc/common.hh (SPOT_FALLTHROUGH): Add the macro.
* bin/randltl.cc, spot/misc/escape.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.hh, spot/tl/snf.cc, spot/twa/acc.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/sepsets.cc, spot/twaalgos/translate.cc: Use it.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Make sure plantuml is
started via "java -Djava.awt.headless".

* bin/genltl.cc: Implement the families.
* NEWS, bin/man/genltl.x: Document them.
* tests/core/genltl.test: Add a test.

* bin/.gitignore, doc/org/.gitignore: Here.

* doc/org/concepts.org: Here.

* bin/common_cout.cc (check_cout): Force a flush of cout if more than
20ms has elapsed since the last explicit flush.
* bin/common_setup.cc (setup): Untie cin and cout if the input
is not a TTY, so that cout is flush less often.
* NEWS: Mention the change.

Fixes #186.

* configure.ac, NEWS: Update version.

Fixes #185.

* spot/tl/simplify.cc: Implement the new rule.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/reduccmp.test: Test it.

* spot/tl/formula.hh, spot/tl/formula.cc: Rework the
initialization of fnode.
* NEWS: Mention the bug.

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

Reported by František Blahoudek.

* bin/genltl.cc: Here.
* NEWS: Mention it, and the typos previously fixed in spot-x.7.

* spot/twaalgos/dtwasat.cc: Update a mark check.