Because some old version of libpango will render a̅ as a‾, without
combining.

* wrap/python/ajax/spot.in: Add the code as a comment.

* wrap/python/ajax/spot.in: Adjust.

* src/ltltest/uwrm.test: New file.
* src/ltltest/Makefile.am: Add it.

* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Change the return
type.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.

* doc/tl/tl.tex, doc/tl/tl.bib: Here.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex: Document it.

* src/ltlvisit/wmunabbrev.hh, src/ltlvisit/wmunabbrev.cc: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltlvisit/tostring.cc (to_spin_string): Use the new rewriting.
* wrap/python/ajax/spot.in: Warn when a "Spin" still contain PSL
operators.
* wrap/python/ajax/ltl2tgba.html: Adjust help text.
* doc/tl/tl.tex, NEWS: Document the new rewriting.

* src/ltlparse/ltlscan.ll: Understand the combining overline, and
combining overbar as synonym for =0.
* src/ltlvisit/tostring.cc: Emit a combining overline for
single-letter atomic propositions.
* src/ltlast/atomic_prop.hh (is_atomic_prop): New function.
* doc/tl/tl.tex: Document these two characters.

* m4/pypath.m4: Here.  This is needed because PYTHON is used as
she-bang line in scripts.

* wrap/python/ajax/ltl2tgba.html: Add the checkbox.
* wrap/python/ajax/css/ltl2tgba.css: Add the necessary class.
* wrap/python/ajax/protocol.txt: Add the new option.
* wrap/python/ajax/spot.in: Handle it.
* wrap/python/ajax/README: Add a few lines to explain
how to run the CGI script from the command line for debugging.

* src/tgba/tgbaexplicit.hh: Rerganize a bit to
allow different functions to be used to format
states.  Add an enabled_utf8() method to
tgba_explicit_formula.
* src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc:
Simplify the interface by not depending on
dotty_decorator explicitely.
* src/tgba/bddprint.hh (enable_utf8): New function.
* src/tgba/bddprint.cc (enable_utf8): Implement it
and use the global utf8 flag in other functions.
* src/tgbatest/ltl2tgba.cc: Add an -8 option for
UTF-8 outpout.
* wrap/python/spot.i: Adjust for tgbexplicit.hh
changes.

* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc:
Return a tgba*, not a const tgba*.

* src/tgba/formula2bdd.hh: Fix the comments so Doxygen can
see them.

* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Here.
* src/ltltest/randltl.cc: Add option -8 to display utf-8 formulae.
* src/ltltest/utf8.test: Test it.

* src/misc/acccompl.cc: Do not include tgbaexplicit.hh.

* doc/tl/tl.tex: Here.

* src/ltlparse/public.hh (fix_utf8_locations): New function.
* src/ltlparse/fmterror.cc (fix_utf8_locations): Implement it.
(format_parse_errors): Rename as ...
(format_parse_errors_aux): ... this.
(format_parse_errors): New implementation that call fix_utf8_locations()
before format_parse_errors_aux() on valid utf8 strings.
* src/ltlparse/Makefile.am: Include $(top_srcdir).
* src/ltltest/utf8.test: New file.
* src/ltltest/Makefile.am: Add it.
* src/ltltest/parse.test: Fix header.

* utf8/doc/ReleaseNotes, utf8/doc/utf8cpp.html, utf8/utf8.h,
utf8/utf8/checked.h, utf8/utf8/core.h, utf8/utf8/unchecked.h:
New files.
* Makefile.am (EXTRA_DIST): Distribute them.

* src/ltlparse/ltlscan.ll: Recognize several utf8 operators
such as □, ◇, ◯, ↔, ⤇, etc.

* src/ltlparse/ltlparse.yy: Make all the above operators
right-associative.  Also let `:' have precedence over `;'.
* src/ltltest/reduccmp.test: Adjust for the `:' precedence.
* doc/tl/tl.tex, NEWS: Document this.

* NEWS: Here.

* wrap/python/ajax/ltl2tgba.html: Add a checkbox and some
code to keep it consistent with the basic rewriting checkbox.
* wrap/python/ajax/spot.in: Deal with the new option.
* wrap/python/ajax/protocol.txt: Document it.

* Makefile.am, src/ltlast/formula.cc, src/ltlast/formula.hh,
src/tgba/tgbaexplicit.hh, wrap/python/ajax/Makefile.am,
wrap/python/spot.i: Here.
* HACKING: Document -*- coding: utf-8 -*-.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.

* src/ltlvisit/simplify.cc (reduce_sere_ltl): New function,
to factor the code of the []-> and <>-> rewrittings.
* src/ltltest/reduccmp.test: Add more tests.
* doc/tl/tl.tex: Document these rewritings.

* src/ltlvisit/simplify.cc: Here.
* doc/tl/tl.tex: Document then.
* src/ltlast/bunop.hh (as_KleenStar): New helper function.
* src/ltltest/reduccmp.test: Add more tests.
* src/ltltest/reduc.cc: Also display the resulting formula
without reduce_size_stricly.

* src/ltlvisit/snf.cc, src/ltlvisit/snf.hh: New files.
* src/ltlvisit/Makefile.am: Distribute them.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Call snf(f) for
all f[*].
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex, doc/tl/tl.bib: Document it.

* src/ltlast/multop.cc (instance): Implement the reduction.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Add a test.

* src/ltlast/multop.cc (instance): Implement the reduction.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.

* src/ltlast/bunop.hh (one_star): New static method building 1[*].
* src/ltlast/bunop.cc (bunop::~bunop, bunop::instance_count): Adjust.
* src/ltlast/multop.cc: Implement the trivial rewriting.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.

Especially, 1&f and 1:f were mistakenly always reduced to f, which is
incorrect when f accept the empty word.

* src/ltlast/multop.cc: Here.
* src/ltlast/multop.hh, doc/tl/tl.tex: Adjust documentation.
* src/ltltest/equals.test: Add more tests.

It was a mistake to try to overload And/Or LTL operator for these when
trivial simplification are performed.  The reason is so simple it is
embarassing: And(f,1)=f is a trivial identity that should not be
applied with AndRat.  E.g. AndRat(a;b, 1) is equal to 0, not a;b.

* src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat
operators.
* src/ltlparse/ltlparse.yy: Build them.
* src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Adjust all switches.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: More tests.
* doc/tl/tl.tex: Document them.

* src/tgbaalgos/ltl2tgba_fm.cc: Here.
The check is done by next patch.

* src/ltlast/multop.cc (instance): Here.
* src/ltlast/multop.hh, doc/tl/tl.tex: Adjust documentation.
* src/ltltest/equals.test: Adjust test cases.