* doc/tl/tl.tex (Other Equivalences): Move...
(Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$): ... here.

* src/ltlvisit/simplify.cc: Add new rules.
* doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Add test cases.

* doc/tl/tl.tex (Syntactic Hierarchy Classes): Document the ->,
<->, and xor operators.  Also add a \phi_F class.

* src/ltlast/binop.cc (binop::binop): Fix computation
of syntactic guarantee and syntactic obligation for the Implies
operator.  Reported by Étienne Renault.
* src/ltltest/kind.test: Add more tests.

The actual rules are a bit more complex:
a & X(G(a&b...)&c...) = Ga & X(G(b...)&c...)
a | X(Fa | c) = F(a) | c
with the second rule being applied only if all XF can
be removed.  See the documentation for an example.

* src/ltlvisit/simplify.cc: Implement these new rules.
* doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Add test cases.

* src/ltlvisit/simplify.cc: Implement these rules.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document them.

* src/ltlvisit/simplify.cc: Implement them here, and augment them
to support M, and W operators.
* src/ltltest/reduccmp.test: Add some tests.
* doc/tl/tl.tex (Simplifications Based on Implications): Document
these rules.
* doc/tl/tl.bib (babiak.12.tacas): New entry.

* src/ltlvisit/length.hh (length_boolone): New function.
* src/ltlvisit/length.cc (length_boolone): Implement it using...
(length_boolone_visitor): ... this new visitor.
* src/ltltest/randltl.cc: Use length_boolone() to check the result
of the random generator, and ignore any formula larger (in
length()) than opt_f.  This fix a bug where the random formula
generator would sometime produce formula larger than requested,
because of the trivial rewriting of {f}[]->e as e|!f.
* src/ltltest/length.cc: Add option -b to call length_boolone().
* src/ltltest/length.test: Test length_boolone().

* src/ltlvisit/simplify.cc (simplify_visitor): Implement these
rules.
* doc/tl/tl.tex: Document these rules.

* doc/tl/Makefile.am (LATEXMK): Set BIBINPUTS for VPATH builds.
(EXTRA_DIST): Distribute tl.tex and tl.bib.
($(srcdir)/tl.pdf): Fix update in srcdir.

* src/ltlvisit/simplify.cc (simplify_visitor::visit(multop)):
Initialize `ri' to kill a warning.

* src/ltlparse/ltlscan.ll: Parse "inf" as OP_UNBOUNDED.
* src/ltltest/equals.test: Add some tests.
* doc/tl/tl.tex: Document it.

* src/ltlvisit/dotty.cc (dotty_visitor::visit): Do not
declare bunop as sinks.

* src/ltlparse/ltlparse.yy: Cleanup the names used in the grammar.
* src/ltlparse/public.hh (parse_ratexp): Rename as...
(parse_sere): ... this.
* src/ltltest/consterm.cc: Adjust call to parse_ratexp().

* wrap/python/ajax/spot.in: Diagnose attempt to use LaCIM or Tau
on PSL formulae.
* wrap/python/ajax/css/ltl2tgba.css (.ltl2tgba .error): New entry.

* src/tgbatest/ltl2tgba.cc: Diagnose attempt to use -l and -taa
on PSL formulae.  Switch back to -f for these formulae.

* doc/tl/tl.tex: Replace all occurrences of ``rational
[expression]'' by SERE.  Add a couple of more notes and
bibliographic references.
* doc/tl/tl.bib: More entries.

* src/ltlvisit/simplify.cc: Add four rules.
* doc/tl/tl.tex: Document these rules.
* src/ltltest/reduccmp.test: Add tests.

* src/ltlparse/ltlparse.yy: Diagnose them.
* src/ltltest/parseerr.test: Add tests.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_ratexp): Replace
a dynamic cast by a call to kind().

* doc/tl/tl.tex: Document the rules.
* src/ltlvisit/simplify.cc (simplify_visitor): Implement them.
* src/ltltest/reduccmp.test: Test them.

* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add a test.
* doc/tl/tl.tex: Document it.
* src/ltlast/multop.cc: Fix the computation of is.accepting_eword
for Fusion.  The Fusion operator never accepts [*0].

* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add more tests.
* doc/tl/tl.tex: Document it.

* doc/tl/Makefile.am: Rewrite using latexmk instead of texi2dvi.
Also define the SpotVersion when calling latexmk, not in tl.tex.
* doc/tl/tl.tex: Assume SpotVersion is defined outside the file.

* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
simplify_mark): Rewrite these two functions as methods of
(mark_tools): this new class.
* src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
of not_marked to ignore marked operators that are not at
the top-level.  I.e., something like X(!{a}) is not marked.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
instance of mark_tools.
(formula_canonizer::translate) Adjust calls to
mark_concat_ops() and simplify_mark().

* src/ltlast/binop.cc, src/ltlast/binop.hh: Here.
* doc/tl/tl.tex, src/ltltest/equals.test: Adjust.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation.  I.e., it would still work without the patch.

* src/kernel.h (PAIR, TRIPLE): Redefine these hash functions
using something that is simpler to compute.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
creating transitions.  Use the bdd directly, and register the used
transitions later.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
Use boolean_to_bdd()