Reported by Joachim Klein.

* src/bin/ltlcross.cc: Here.
* NEWS, THANKS: Update.

Reported by František Blahoudek.

* src/bin/genltl.cc (R_n): Really generate (GFp1 || FGp2), not
(GFp1 || GFp2).
* NEWS: Mention the bug.
* THANKS: Update.

This follows up on a mail from Sonali Dutta.

* src/tgba/bdddict.hh (assert_emptiness, ~bdd_dict): Better
documentation.
* src/tgba/formula2bdd.hh (formula_to_bdd): Mention
unregister_all_my_variables().
(bdd_to_formula): Complete the documentation.
* THANKS: Add Sonali Dutta.

* src/ltlparse/ltlparse.yy: Add new printers.  Suggested by Akim
Demaille.

* THANKS, src/tgbaalgos/ltl2tgba_fm.cc: Here.

* bench/emptchk/formulae.ltl: Do not use + and * in the list of
formulas.  Use | and & instead.  The * operator was removed on
2010-01-30.  Reported by Étienne Renault.

Especially with should write !(p0) and not !p0, because p0 is
usually #define'd by the user and he may have forgotten to quote
the value of the macro.  This issue was discovered by Kristin
Yvonne Rozier and diagnosed by Gerard Holzmann.

* src/tgbaalgos/neverclaim.cc (process_link): Call
to_spin_string(..., true) to fully parentheses the string.
* src/tgbatest/neverclaimread.test: Add a test.

* src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the
documentation after a report from Nikos Gorogiannis.

* src/tgba/tgbasafracomplement.cc
(tgba_safra_complement::tgba_safra_complement)
(tgba_safra_complement::succ_iter): Correct the declaration and
use of multiple acceptance conditions.
(state_complement::to_string): Output the L set, not U.  The previous
code caused different states to share the same names, causing issues
with the text-based output (state with identical names get merged).
* src/tgba/tgbasafracomplement.hh
(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
store BDDs.
* src/tgbatest/complementation.cc: Implement a new "-b" option
to output automata in Spot's syntax.
* src/tgbatest/complementation.test: Add a test-case supplied
by Martin Dieguez Lodeiro.
* THANKS: Add Martin.

Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.

* src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used
to record outgoing transitions by an Sgi::hash_map, and keep the
order of these transitions in a separate list.
* src/tgbatest/degendet.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* THANKS: Add Tomáš and convert to utf8.

We do that because the declaration of this type, which is local to
src/tgba/tgbasafracomplement.cc has a member in an anonymous
namespace, and some versions of g++-4.2 issue a very annoying
warning about this legitimate code.  See Bug 29365 on GCC's
Bugzilla.  Report by Silien Hong <silien.hong@lip6.fr>.

* src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not
forward declare.
(tgba_safra_complement): Use void* instead of
safra_tree_automaton*.
* src/tgba/tgbasafracomplement.cc: static_cast void* to
safra_tree_automaton* anywhere needed.

* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions.  I realized this while looking at experiments from
Rüdiger Ehlers.

* bench/ltlcounter/README, bench/ltlcounter/run,
bench/ltlcounter/plot.gnu, bench/ltlcounter/defs.in,
bench/ltlcounter/Makefile.am: New files.
* bench/Makefile.am (SUBDIRS): Add ltlcounter.
* configure.ac (AC_CONFIG_FILES): Adjust.
* THANKS: Add her.

* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
src/ltltest/nenoform.test, src/ltltest/parse.test,
src/ltltest/parseerr.test, src/ltltest/tostring.test,
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run().
* Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files,
Automake 1.8 find them automatically.
* configure.ac: Require Automake 1.8, in gnits mode, and check
for valgrind.
* THANKS: New empty file.