add a "dot source" source behind each picture instead.  Do
not run `dot' on big automata.

in comment.  Skip false transitions, and do not compute
sub-formulae reachable only via false transitions.

yesterday's change.  This optimization is NOT covered by exprop.
In fact it could be generalized.

cond_for_true optimization.  It is covered by exprop.

Fix reference to Oddoux's thesis.

symb_merge argument.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise.
* src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y
to unset symb_merge.
* wrap/python/cgi/ltl2tgba.in: Remove the exprop version
of the FM translator, make exprop and symb_merge options.

suppress the GFy optimisation introduced on 2003-11-26, it is
generalized by the identification of states with same symbolic
rewriting introduced on 2004-02-02.

closed.

filename for the formula.  Merge the transitions of automata
read with -X.
* src/tgbatest/spotlbtt.test: Add many disabled algorithms.
It is convenient to reuse the `config' file created by this
test when making statistics.
* src/tgbatest/ltl2baw.pl: New file.
* src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl.

Define as && and || as in Spin.
* src/SpotWrapper.hh: Update by email.

* HACKING: Update versions.

argument.  Consider all possible combinations of propositions when
generating arcs.  Suggested by Jean-Michel Couvreur.
* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust.
* src/tgbatest/ltl2tgba.cc: Honor -fx.
* src/tgbatest/spotlbtt.test: Exercise -fx.
* wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded
properties.

showing formula.
* wrap/python/cgi/README: Mention unique_id.

formula automaton and the synchronized product) from LBTT.
Idea from Jean-Michel Couvreur.

* src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
(nonacceptant_lbtt_reachable): New function.
* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
function.
* src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
if the -T option is used.
* src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
default.

* wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler)
(reset_alarm): New functions.  Kill the script and its
children if it runs for too long.
(render_dot): Call reset_alarm.

with IE, Safari, konqueror, ... None of these support
rules="groups" frame="border" properly (Mozilla is OK).

to stdout early.

the number of acceptance conditions.

wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py: Specify coding system to
accommodate newer Python versions.

* wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh.
* wrap/python/tests/minato.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add minato.py.

src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc: Add missing copyright license.

with dot, without using convert.
* wrap/python/cgi/README: Do not mention convert.

(render_bdd): New functions, extracted from the rest of the code.

to trans_fm.
(translators): Show trans_fm before trans_lacim.

it to display the size of the generalized and degeneralized
automata.

* src/tgbalagos/Makefile.am: Add them.
* wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and
src/tgbalagos/stats.hh

with identical successors.  This optimizes the translation
of `a R (b R c)', for instance.
* src/tgbatest/ltl2tgba.test: Add two new tests.

with identical successors.  This optimizes the translation
of `a R (b R c)', for instance.
* src/tgbatest/ltl2tgba.test: Add two new tests.

with identical successors.  This optimizes the translation
of `a R (b R c)', for instance.
* src/tgbatest/ltl2tgba.test: Add two new tests.