rules for "a U b" and "a R b", an implication check is enough.

bdd_isrunning() and don't run bdd_init() if it has already been
called.

generation of the graph.  Some states had no successors or
duplicate transitions because of that bug.

tgbaparse/tgbaparse.yy: Fix Bison warnings about unset $$.

install location.hh and position.hh, since we no longer share
those of ltlvisit.
* src/evtgbaparse/Makefile.am (evtgbaparse_HEADERS): Likewise.

* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh:
Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger
flags, and call reduce_tau03.
* src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the
default.
* src/ltlvisit/contain.cc: Style.
* src/ltltest/reduc.cc: Simplify using the reduce() interface
instead of reduce_tau03.
* src/tgbatest/ltl2tgba.cc: Likewise.  Add -fr5, -fr6, and -fr7
options.
* src/tgbatest/spotlbtt.test: Remove cases using "-c", since its
current implementation is not always correct (and apparently
reduces less than -fr7).

src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh,
src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbaparse/tgbascan.ll: Adjust for Bison 2.3.  Use %name-prefix
instead of the "#define yy ... " kludge.

check containment on demand.

New function, performing LTL reduction a la tauriainen.03.a83.
* src/ltltest/equals.cc, src/ltltest/reduc.cc: Add support for
the new reduction.
* src/ltltest/reduc.test: Cut the test in half, and additionally
test the new reduction.
* src/ltltest/reduccmp.test: Run on the new reduction.
* src/ltltest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: Add new options to apply the reduction.
* src/tgbatest/spotlbtt.test: Use them.

conditions.

New function.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Use it to
distinguish acceptance conditions that are identical in both
operands.
* src/tgbatest/explpro4.test: New file.
* src/tgbatest/explpro2.test, src/tgbatest/Makefile.am: Adjust.

* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
(spot::ltl::language_containment_checker): ... in these new files.
* src/ltlvisit/Makefile.am: Adjust.

* src/misc/Makefile.am: Add them.
* src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh: Add a "vmsize" statistic.

Rename as ...
(free_anonymous_list_of): ... this, and correct their update on
release.  Also correct yesterday's the correction (ahem!).
(dump): Improve verbosity.
* src/misc/freelist.cc (free_list::remove, free_list::insert): Fix
longstanding thinkos.
(free_list::free_count): New function.

2006-05-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>
* src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Count the

src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, src/tgba/tgbatba.hh:
Remove superfluous class qualifiers worrying gcc 4.1.2.

(ltl_to_tgba_fm): Add a new option "containment_checks" to enable
some language containment checks (via emptiness checks) during the
translation.  This first attempt currently only use containment
checks to merge states bisimulating each other.
* src/tgbatest/ltl2tgba.cc: Bind this to option "-c".
* src/tgbatest/spotlbtt.test: Check it.

call release_n(), not remove() to repopulated the freelist of
anonymous BDD variables.  New code I'm working on triggered an
assertion inside remove(), but I'm surprised this bug hadn't
manifested before !

iface/gspn/ltlgspn.cc, iface/gspn/dottygspn.cc, iface/gspn/ssp.cc,
iface/gspn/dottyssp.cc: s/exeption/exception/g.

(couvreur99_check_shy_ssp): Add a onepass_ attribute to
disable the "shyness", and do not increment pos before calling
find_state since gspn's implementation uses it.
* iface/gspn/ssp.cc: Enable "onepass_" for all "shy" variants,
and also fix find_state for the case where onepass_ is
disabled (but I do not yet know why the latter fix isn't enough).

each container into lists of states with identical formula states.

src/tgbaalgos/gtec/gtec.hh: New option (-e6) to disable
inclusion check in the stack.

Count the number of removed components.

numbered_state_heap_ssp_semi): Implement a double hash_map using
greatspn's new container() function.
* iface/gspn/ssp.hh (gspn_ssp_interface): Add a doublehash option.
* iface/gspn/ltlgspn.cc: Add option -1 to disable this optimization.

instead of one : one for the atomic propositions, and one
for the acceptance conditions.  This way it's easy for
the tools in iface/gspn/ to require some atomic proposition
to be declared and allow any acceptance conditions (there is nothing
to adjust in this files because of the default value of the argument).
* src/tgbaparse/tgbaparse.yy: Adjust.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/readsave.cc,
src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc: Adjust calls.

conditions rejected by the environment.

(main): Use it.
* iface/gspn/ssp.cc: Add more counters for statistics.

update the emptiness statistics.

* m4/gspnlib.m4: Typo.

Reorganize this function so that syntactically there is only one
loop over the successors, and not two.  Call reintroduce the call
to couvreur99_check_shy::state_index(), needed by SSP, and
suppress that to index_and_insert introduced on 2004-12-29.  Also
split the "group" option in two: "group" and "group2".  "group2"
is the equivalent of the older "group", while the new "group" is
weaker and faster.
(couvreur99_check_shy::state_index): Change prototype as needed by
the algorithm.
* src/tgbaalgos/gtec/gtec.hh: Adjust.
* src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc
(index_and_insert): Remove.
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust
to new prototype.
* bench/emptchk/README, bench/emptchk/algorithms: Adjust references
to group/group2.

accepting runs.

* wrap/python/cgi/ltl2tgba.in: Offers all 6 emptiness
check algorithms, and a text box for options.

Initialize tmp to suppress a GCC 4.0.1 warning (seen on Darwin).