* src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy,
src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use
token types for %destructor and %printer.  Remove the yylex hack,
since %name-prefix is now honored by Bison.  Also remove the
useless <token> type.  Suggested by Akim Demaille.

* src/ltlparse/fmterror.cc (format_parse_errors): Count columns
starting at 1.  Older Bison used to start at 0 but changed to
match the GNU Coding Standards.
* src/ltltest/parseerr.test: Add a test case.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse):
Disable this rule unconditionally.
* src/ltltest/reduccmp.test: Adjust tests.

degeneralization.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the
list of acceptance condition in the reverse order.  The order is
still arbitrary, but the bdd_satone() call seems to output the
acceptance conditions that are more used first, and this helps the
degeneralization process.

* src/ltlparse/ltlparse.yy: Change the precedence of "->" and
"<->" so that "a & b -> c" is interpreted as "(a & b) -> c"
instead of "a & (b -> c)".  The new interpretation is more
intuitive, and matches that of LBTT.

original paper by Somenzi and Bloem.  Reported by Ruediger Ehlers.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Do not
forget to free the initial state after usage.

by default in scc_filter().

Doing so helps the degeneralization algorithm, because it will
have more opportunity to be in an accepting level when it reaches
the accepting SCCs.

* src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
remove_all_useless argument.
(filter_iter::process_link): Use the flag to decide whether to
filter acceptance conditions going to accepting SCCs.
(scc_filter): Take a remove_all_useless argument and pass it to
filter_iter.
* src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
and document the function.
* src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
for remove_all_useless=false and add -R3f for
remove_all_useless=true.
* src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
the degeneralization worse than -R3.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace
the FG(a)|FG(b) == FG(a|b) rule by the above more generic one.
Add the dual rule for G(a)&G(b), as we had none (this one won't
improve anything in the translation, but it is more symmetric
this way).  Also simplify some pointer checks.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set
cycle_start_ to start in the accepting layer of the degeneralized
automaton if the initial state has an accepting self-loop.
Otherwise, starts at the level of the first acceptance condition
as previously.
(tgba_sba_proxy::get_init_state): Use cycle_start_.
* src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so
that we can use it in tgba_sba_proxy::tgba_sba_proxy.
(tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state):
Declare.
* src/tgbatest/ltl2tgba.test: More tests.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move
the optimization step added by the previous patch outside the
before the bddtrue check, so that it also applies to accepting
states in SBA.

an acceptance condition on all outgoing transitions.

This was motivated by experiments from Rüdiger Ehlers, showing
that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
U (b U c)'".  With this change and the previous one, it is no
longer the case.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
a pointer to the source automaton and...
(tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
optimization step to gather the acceptance conditions common
to all outgoing transitions of the destination state, and pretend
they are on the current (ingoing) transition.
(tgba_tba_proxy::succ_iter): Pass the
source automaton to the constructed iterator.
* src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
* src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.

* 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.

* src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi
is the BibTex entry used as comment, because some version of sed
will choke on non-ascii character and cause sanity/style.test to
fail.

This is actually the third time I fix random_graph().  On
2007-02-06 I changed the function not to generated dead states,
but in a way that made it non-deterministic.  On 2010-01-20 I made
the function deterministic again, but it started to generate dead
states as a side effect.  This time, I'm making sure that dead
states won't come again with a test-case that we should have had
from the beginning.

* src/tgbaalgos/randomgraph.cc (random_graph): Add an extra
indirection array, state_randomizer[], so that we can reorder
states indices after a random selection without actually changing
the value of the indices used by unreachable_states and
nodes_to_process.
* src/tgbatest/randtgba.test: New file.
* src/tgbatest/Makefile.am: Add randtgba.test.

* wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by
configure.
(os.system): Cleanup stale files only when the form has been
submitted.
(list options): Keep track of the selected value.
(draw_acc_run|print_acc_run): set ec=0 to detect if it has been
later set or not.  Fix error message when using generalized
automata with degeneralized emptiness checks.
* wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@.

* wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new.
(svg_output, reduce_langcout): Add these new options.
(render_dot): Support svg_output.

* NEWS, configure.in: Bump version to 0.5.

explicitly, otherwise the documentation is always built and
distcheck fails.

* src/sabaalgos/sabareachiter.hh (process_link): Document argument SI.
* src/eltlparse/public.hh (format_parse_errors): Remove the
non-existing eltl_string argument from the description.
(parse_file): Fix name of parameters in documentation.

Doxygen only knows how to call dot with -Tpng, while using
-Tpng:gd produces pictures that are 10 times smaller.  Use a
simple wrapper around dot to simplify this.

* doc/dot.in: New file, that wrap the system's dot and replace
-Tpng by -Tpng:gd.
* doc/Makefile.am ($(srcdir)/stamp): Depend on dot.
* doc/Doxyfile.in: Update to 1.6.2.
(DOT_PATH): Set to @srcdir@ to use doc/dot instead of the
system's dot.
* configure.ac: Find the absolute path of dot, and generate
the doc/dot script.

* src/tgba/tgbakvcomplement.hh: Use \verbatim around the bibtex
entry.
* src/saba/sabacomplementtgba.hh: Use latin1.

depend on files that cannot be built.

* src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these
files.
* src/tgba/Makefile.am: Remove them.
* src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New
files.
* src/ltl/ltlparse/Makefile.am: Add them.
* bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite
using the new class.

* src/sanity/style.test: Check for missing Copyrights blurbs.
* src/sanity/Makefile.am: Run style.test before includes.test.
* iface/gspn/dcswave.test, iface/gspn/dcswaveeltl.test,
iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test,
iface/gspn/simple.test, iface/gspn/udcsefm.test,
iface/gspn/udcseltl.test, iface/gspn/udcsfm.test,
iface/gspn/udcsltl.test, iface/nips/nipstest/dotty.test,
iface/nips/nipstest/emptiness.test, src/eltltest/acc.test,
src/eltltest/nfa.test, src/saba/sabacomplementtgba.cc,
src/sabatest/sabacomplementtgba.cc, src/tgbatest/eltl2tgba.test,
src/tgbatest/taatgba.test: Add missing Copyright blurb.

* eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh,
tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc,
tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment
changes.

* wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically
prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting
SCCs in all algorithms.
* src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to
SWIG.
* wrap/python/spot.i: Include reductgba_sim.hh.

server.

* wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the
script is not called as a CGI.  Arrange to load libraries from
the build directory.  Create the spotimg/ if needed when run as
a web server.
* wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean
the spotimg directory.
* wrap/python/cgi-bin/README, NEWS: Update.

* src/ltltest/parse.test, src/ltltest/syntimpl.test: Replace * by &.