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

* src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Use Perl for the unix2dos conversion.

* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/reduc0.test: Add a regression test.
* src/ltltest/reduccmp.test: Adjust test cases for its removal.
* NEWS: Mention it.

(No test, this is just a simple backport of a fix from the development
branch, where it is tested.)

* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* NEWS: Mention it.

* src/dstarparse/dstarscan.ll, src/kripkeparse/kripkescan.ll,
src/neverparse/neverclaimscan.ll, src/tgbaparse/tgbascan.ll:
Distinguish between 1-sized EOL and 2-sized EOL.
* src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Add more tests.
* NEWS: Mention it.
* src/kripkeparse/scankripke.ll: Remove this unused file.

* src/tgba/futurecondcol.cc: Use swap instead of assignement.  It is
more efficient, and it avoid the bug of gcc-snapshot mentionned two
commits below.

The ltl_to_tgba_fm() translation function was using a hash_map of
maps (ugh!) to merge transitions on output.  However recent libstd++
changed the implementation of hash_map (a.k.a. unordered_map) causing
transitions to be output in a different order.  This
implementation-dependent order caused the ltl2ta.test to fail because
the BA->TA transformation can produce TA of different sizes if you
simply change the order of transitions in the input BA! This does not
sound like a nice property for the BA->TA transformation, but Ala Eddine
isn't sure how to fix it yet.  In the meantime, this patch makes sure
ltl_to_tgba_fm() will return the same output regardless of the
implementation of hash_map.

The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
and with gcc-snapshot (5.0.0 20141016) on Debian.

* src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
using a std::vector and std::sort instead of nested maps tables.
* NEWS: Mention the fix.

* src/tgba/tgbasafracomplement.cc: Here.  Beside being more efficient,
the use of std::swap instead of an assignment also protects us from a
bug recently introduced in the development version of G++.
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=63698

* doc/org/init.el.in: Add compatibility with org 8.
* NEWS: Mention it.

We just changed the format specification today.

* src/tgbaalgos/hoaf.cc: Here.
* NEWS: mention it.

Reported by Joachim Klein.

* src/neverparse/neverclaimparse.yy: Store labels and the
location of their first definition in a global map to catch
redefinitions.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention it.

* src/bin/ltlcross.cc: Fix it.
* src/tgbatest/ltl2dstar.test: Test it.
* NEWS: Mention it.

* src/bin/ltlcross.cc: Implement it.
* NEWS: Mention it.

* configure.ac, doc/org/tools.org, NEWS: Bump version to 1.2.5.

* src/tgbaalgos/ltl2tgba_fm.cc: Fix.
* src/tgbatest/randpsl.test: Rewrite using ltlcross and add a testcase.
* NEWS: Mention it.

Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: Name the tab.
* wrap/python/ajax/css/ltl2tgba.css: Give it some space.

Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: New option.
* wrap/python/ajax/protocol.txt, NEWS: Document it.
* wrap/python/ajax/spot.in: Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.

Suggested by Joachim Klein.

* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/ltlcross3.test: Test it.
* doc/org/ltlcross.org, NEWS: Document it.

Reported by Joachim Klein.

* src/bin/randltl.cc: Here.
* NEWS: Mention the fix.

Suggested by Joachim Klein.

* src/bin/randltl.cc: Implement it.
* src/ltltest/rand.test: Test it.
* doc/org/randltl.org, NEWS: Document it.

The specifications are at http://adl.github.io/hoaf/

* src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/tgbatest/ltl2tgba.cc: Add option to output HOA.
* NEWS: Mention it.

Suggested by Joachim Klein.

* wrap/python/ajax/spot.in: Try parse_lbt() when parse() fails.
* NEWS: Mention it.

So that people using white-background terminal can still read them...
Reported by Joachim Klein.

* src/bin/ltlcross.cc: Adjust.
* NEWS: Mention it.

The bug was reported by Joachim Klein.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Reduce P(a M b) to P(a & b), not to P(a).
* src/tgbatest/ltlcross.test: Test Joachim's formula.
* src/tgbatest/ltl2ta.test: Adjust some expected values.
* NEWS: Mention the bug.

This was prompted by an exchange of emails with Caroline Lemieux.

* src/bin/man/ltl2tgba.x: Add notes and references.
* NEWS, THANKS: Update.

This can only cause failure when running under valgrind (i.e., in the
test suite), but is not a problem in practice as the test is certain
to fail the entry->c check whenever entry->b is uninitialized.

* src/bddop.c (bdd_implies): Here.

* doc/org/init.el.in (org-publish-timestamp-directory): Use a build
directory, not $HOME.