ChangeLog

2004-11-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc.

	* src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* iface/gspn/ltlgspn.cc (main): Call project_tgba_run if -P.

	* src/tgbaalgos/emptiness.cc,
	src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba*
	argument before the tgba_run* argument (for consistency with
	replay_tgba_run).
	* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust
	calls to print_tgba_run().

	* src/ltlast/formula.hh (ltl::formula::~formula): Make it protected.

2004-10-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	A tgba can now annotate a transition (i.e., the position of a
	tgba_succ_iterator) with some string.  This comes handy to
	associate that transition to its high-level name.
	* src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
	New method.
	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
	(tgba_product::transition_annotation): Implement it.
	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
	(tgba_tba_proxy::transition_annotation): Likewise.
	* src/tgbaalgos/replayrun.cc (print_annotation): New function.
	(replay_tgba_run): Use it.

	* src/tgbaalgos/gtec/gtec.cc,
	src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
	* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.

	* src/sanity/style.test: Diagnose superfluous constructs such
	as `if (x) delete x;'.
	* iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc,
	src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/magic.cc,
	src/tgbatest/ltl2tgba.cc: Remove such constructs.

	* src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by
	-eALGO and -EALGO to ease the addition of new algorithms.
	* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust.

	* src/misc/version.cc: Fix trailing whitespace.
	* src/sanity/style.test: Diagnose trailing whitespace.

	* src/tgbatest/ltl2tgba.cc: Fix lines longer than 80 chars.
	* src/sanity/80columns.test: Use expand to untabify, the previous
	recipe was incomplete.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Note duplicate states.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Verify the run is
	accepting.

	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path):
	Initialize best_end to remove a spurious warning.

	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
	couvreur99_check_result::complete_cycle,
	couvreur99_check_result::accepting_path): Record conditions and
	acceptance conditions in the accepting run.  Simplify the
	todo BFS stack for accepting_run and complete_cycle.
	* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
	now everything works.
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
	when an outgoing transition is not found.

2004-10-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search):
	Record the acceptance conditions in the accepting run.
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic.

	* src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files.
	Cannot test them because the run returned by the emptiness checks
	are currently incomplete (they lack the acceptance conditions, and
	sometimes even the labels in the prefix).
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
	when the emptiness checks are fixed.

2004-10-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Introduce an emptiness-check interface, and modify the existing
	algorithms to conform to it, uniformly.  This will unfortunately
	break third-party code that were using these algorithms.
	* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
	* src/tgbaalgos/Makefile.am: New files.
	* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
	conform to the new emptiness-check interface.
	* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
	Likewise.  The classes have been renamed are as following
	  emptiness_check -> couvreur99_check
	  emptiness_check_shy -> couvreur99_check_shy
          emptiness_check_status -> couvreur99_check_status
	  counter_example -> couvreur99_check_result
	* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
	iface/gspn/ssp.cc: Adjust to renaming and new interface.

	* src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh:
	New files.
	* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
	libevtgbaalgos_la_SOURCES): Add them.
	* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
	New files.
	* src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
	(ltl2evtgba_SOURCES): New variable.

	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert
	that the true state has only one link when unobs is used.

2004-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/evtgbatest/Makefile.am (CLEANFILES): New variable.

2004-10-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Preliminary support for Event-based GBA.
	* src/evtgba/Makefile.am, src/evtgba/evtgba.cc,
	src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
	src/evtgba/explicit.cc, src/evtgba/explicit.hh,
	src/evtgba/product.cc, src/evtgba/product.hh,
	src/evtgba/symbol.cc, src/evtgba/symbol.hh,
	src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
	src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
	src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
	src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am,
	src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
	src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
	src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
	src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
	src/evtgbatest/explicit.test, src/evtgbatest/product.cc,
	src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
	src/evtgbatest/readsave.test: New files.
	* configure.ac: Create the Makefiles in these new subdirectories.
	* src/Makefile.am: Recurse them.

	* src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word):
	New function.

	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to
	anonymous namespace.

2004-10-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* wrap/python/Makefile.am (_spot_la_SOURCES): Add spot_wrap.h.

2004-10-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done,
	loopless_modular_mixed_radix_gray_code::last): Declare as const.

	* src/misc/bareword.hh, src/misc/bareword.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.

	* src/misc/modgray.hh, src/misc/modgray.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
	* wrap/python/spot.i: Activate directors, and interface modgray.hh.
	* wrap/python/tests/modgray.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

2004-10-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc,
	src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc,
	src/ltlvisit/dump.cc, src/ltlvisit/length.cc,
	src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
	src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
	src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc,
	src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc,
	src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc,
	src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
	src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc,
	src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
	Declare private classes and helper function in anonymous namespaces.
	* HACKING, src/sanity/style.test: Document and check this.
	Also check for trailing { after namespace or class.
	* src/ltlast/predecl.hh, src/ltlast/visitor.hh,
	src/tgba/tgbareduc.hh: Fix trailing {.

2004-10-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21.

	Back out all Thomas's changes on emptiness checks since
	2004-08-23.  Some of these will need to be reintegrated more
	slowly and cleanly.

	* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
	src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
	src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
	* src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
	src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
	src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
	Delete.

2004-10-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltltest/reduc.test: Do source ./defs.  Revert mistaken
	change from 2004-09-13.

	* src/tgbatest/explicit.test: Typo.

2004-10-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	The computation of the counter example fails the valgrind tests
	and is wrong into two ways: the search stack is generally not a
	path, and does not run until the end of the STL container.
	Remove it.
	* src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh
	(tarjan_on_fly): Do not inherit from the emptiness_search class,
	because the check method will no longer return a counter example.
	(tarjan_on_fly::check): Return only a boolean.
	(tarjan_on_fly::build_counter): Delete.
	* src/tgbatest/ltl2tgba.cc: Adjust.

	* src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state,
	tgba_explicit_succ_iterator::current_condition,
	tgba_explicit_succ_iterator::current_accepting_conditions): Assert
	the iteration is not finished.

2004-10-12  Alexandre Duret-Lutz  <adl@gnu.org>

	* wrap/python/tests/run.in: Typo.  From Akim Demaille.

2004-10-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Empty CFLAGS and CXXFLAGS.
	* m4/debug.m4: Update CXXFLAGS too.

2004-10-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Doxyfile.in: Upgrade to Doxygen 1.3.9.

2004-09-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Suggest using "x->y", not "(*x).y".
	* src/tgbaalgos/tarjan_on_fly.cc: Fix.

2004-09-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Suggest ++i over i++ when it does not
	matter, for consistency.
	* src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc,
	src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust.

	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument.
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
	* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.

2004-09-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename
	emptyness_search to emptiness_search.

	* src/sanity/style.test: Warn about places where size() is used
	instead of empty().
	* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
	than size() when checking emptiness of lists.
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc,
	src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc,
	src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc,
	src/misc/minato.cc: Likewise.
	* src/ltlast/multop.cc (multop::instance): Call ->size() only once.

2004-09-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Update to SWIG 1.3.22.
	* wrap/python/libpy.c: Delete.
	* wrap/python/swigpy.i: New file.
	* wrap/python/Makefile.am (swigpy_wrap.c): Build this from swigpy.i
	and use it instead of libpy.c.

	* INSTALL, lbtt/INSTALL: New upstream version.

2004-09-14  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/emptchk.test
	src/tgbaalgos/tarjan_on_fly.hh,
	src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/minimalce.cc: To correct a bug.

	* src/ltltest/reduc.test (FICH): bad file name.

2004-09-13  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc:
	New algorithm for emptiness check.

	* src/tgbatest/spotlbtt.test,
	src/tgbatest/reductgba.cc,
	src/tgbatest/ltl2tgba.cc:
	Add option for reduction of TGBA.

	* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
	src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
	Remove some bugs.

	src/tgbaalgos/gtec/ce.cc:
	Modification of construction of counter example.

	* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/reductgba_sim_del.cc,
	src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
	Modification for delayed simulation.


2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbaalgos/tarjan_on_fly.hh,
	src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/colordfs.hh,
	src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check.

	* src/tgbaalgos/gtec/ce.hh,
	src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
	object in minimalce.hh.

	* src/tgbatest/ltl2tgba.cc,
	src/tgbatest/emptchk.test,
	src/tgbaalgos/Makefile.am: Add files for emptiness-check.

2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
	* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
	for scc reduce.

2004-08-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac, NEWS: Bump version to 0.0y.

	* configure.ac, NEWS: Bump version to 0.0x.

2004-08-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Doxyfile.in (GENERATE_TAGFILE): Build spot.tag.
	* doc/Makefile.am (dist_pkgdata_DATA): Add spot.tag.

	* src/tgbatest/ltl2tgba.cc (syntax): Typo.

	* doc/Doxyfile.in (STRIP_FROM_PATH): Strip @srcdir@ so its
	does not appear when listing mainpage.dox.

2004-08-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh:
	Typos in Doxygen comments.

2004-08-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/apcollect.hh: Fix include guard.  Report from Denis.
	* src/sanity/includes.test: Include files twice to check include
	guards.

	* src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case
	assert() is disabled.

	* src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable,
	to force C++ linking.

	* iface/gspn/ltlgspn.cc: Fix a gcc warning in case assert() is
	disabled.

2004-08-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: New files,
	based on code from <Denis.Poitrenaud@lip6.fr>.
	* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES, ltlvisit_HEADERS):
	Add them.

	* iface/gspn/common.cc, iface/gspn/common.hh,
	src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
	src/ltlparse/fmterror.cc, src/ltlparse/public.hh,
	src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
	src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
	src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc,
	src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
	src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
	src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
	src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
	src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
	src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd>
	in headers, and prefer <ostream> in the body whenever possible.
	* src/sanity/style.test, HACKING: Check and document this.

	* src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh,
	src/ltlast/binop.hh, src/ltlast/constant.hh,
	src/ltlast/formula.hh, src/ltlast/multop.hh,
	src/ltlast/predecl.hh, src/ltlast/refformula.hh,
	src/ltlast/unop.hh, src/ltlast/visitor.hh: Use \file to introduce
	each file.

	* doc/Doxyfile.in (STRIP_FROM_INC_PATH): Define, so that the
	`#include' references are correct.

	* README: Update.

	* m4/gccoptim.m4: Compute optimization flags for CXX too.

	* m4/ndebug.m4: Update CPPFLAGS, not CFLAGS.

	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all
	parameters.
	* src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise.

2004-08-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Call AC_PROG_CC and AM_PROG_CC_C_O.
	* wrap/python/Makefile.am (_buddy_la_LDFLAGS): Move libspotswigpy.la ...
	(_buddy_la_LIBADD): ... here.

2004-08-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.2.

2004-07-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.1.

2004-07-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Doxyfile.in: Update for Doxygen 1.3.8.

2004-07-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Call AC_LIBTOOL_WIN32_DLL
	* src/Makefile.am (libspot_la_LDFLAGS): Add -no-undefined.

2004-07-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/explicit.test: Do not use `-i', it's not needed
	and it is wrong to put it after `-e'.  Caught by Denis too.

	* src/ltltest/reduc.test: Use `test a = b' not `test a == b'.
	Reported by <Denis.Poitrenaud@lip6.fr> (failure on Cygwin).

2004-07-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/defs.in (VALGRIND): Specify --tool=memcheck for
	compatibility with valgrind 2.1.x.
	* src/ltltest/defs.in (VALGRIND): Likewise.

2004-07-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* m4/gccwarn.m4: Do not check nor use -Wstrict-prototypes.
	g++-3.4 complains it makes no sense in C++.

	* iface/gspn/ssp.cc: Typos.

	* iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn):
	Set size_ to 1 when stuttering is needed, so that done() does not
	return true immediately.

2004-07-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/gtec/gtec.hh: Typos in comments.

2004-07-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen
	example.

	* src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed,
	reduc_tgba_sim): Fix warnings about Doxygen comment.
	* src/ltlvisit/reduce.hh (reduce): Likewise.

	* doc/footer.html: New file, link to RefDocComments on the wiki.
	* doc/Doxyfile.in (HTML_FOOTER): Use footer.html.
	* doc/Makefile.am (EXTRA_DIST): Add footer.html.

	* THANKS: Fill in.

	* src/tgbatest/ltl2baw.pl: Do not use -T anymore.  Fix comments.

2004-07-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	lbtt 1.1.0 supports TGBAs, use that and remove old workarounds.
	* src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal,
	state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo
	lbtt_reachable): Remove.
	(nonacceptant_lbtt_bfs): Rename as ...
	(lbtt_bfs): ... this, and adjust to output acceptance conditions
	on transitions.
	(nonacceptant_lbtt_reachable): Rename as ...
	(lbtt_reachable): ... this.
	* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete.
	* src/tgbatest/ltl2tgba.cc: Suppress option "-T".

	Patch from Heikki Tauriainen <heikki.tauriainen@hut.fi>.
	* src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do
	not parenthesize the type after the new operator (g++ 3.4 complains).
	* src/tgbaalgos/dupexp.cc (dupexp_iter::process_state,
	dupexp_iter::declare_state): Use this->automata_instead of
	automata_.  Local protected member automata_ inherited from
	template base class must be prefixed or g++ 3.4 will not look it
	up (conforming to 14.6.2.3).

2004-07-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.0.
	* src/tgbatest/spotlbtt.test: Adjust config file syntax to
	please lbtt 1.1.0.

	* src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add
	comments.
	* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise.
	Soheib and I had a hard time figuring why we did this...

2004-07-02  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
	src/tgbaalgos/reductgba_sim.cc,	src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.

	* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
	* src/tgbatest/spotlbtt.test: More test (delayed simulation)

2004-06-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac, NEWS: Bump version to 0.0w.

	* configure.ac, NEWS: Bump version to 0.0v.

2004-06-28  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reduccmp.test: Bug.

	* src/tgbatest/reductgba.test: More Test.

	* src/tgbatest/ltl2tgba.cc: Adjust ...
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/reductgba_sim.cc: try to optimize.

	* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Scc reduction
	and we remove some acceptance condition in scc which are not accepting.
	* src/ltlvisit/syntimpl.cc : Some case wasn't detect.
	* src/ltlvisit/basicreduce.cc: Case FGa || FGb = F(Ga | Gb) added.
	* src/ltltest/syntimpl.test: More Test.
	* src/ltltest/syntimpl.cc: Put the formula in negative normal form.

2004-06-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* buddy/: Merge buddy-2-3.

2004-06-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc (main): Degeneralize before
	the simulations.

2004-06-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/tostring.cc (is_bare_word): New function.
	(to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word
	to better check which atomic proposition need to be quoted.
	* src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_
	or G_.
	* src/ltltest/equals.test, src/ltltest/tostring.test: More tests.

	* src/tgba/tgbatba.cc (tgba_tba_proxy::format_state): Use
	bdd_format_accset to print the acceptance condition part of the state.
	That produces more readable output.

	* wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options.
	* wrap/python/spot.i: Wrap src/ltlvisit/reduce.hh.

	* src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files,
	extracted from ...
	* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
	again.
	* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
	simplify_f_g() in addition to unabbreviate_logic().
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
	Add simpfg.cc and simpfg.hh.

	* src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ...
	* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
	the function name.
	* ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am,
	tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames.

	* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):
	Factorize.

	* src/ltlvisit/basicreduce.hh: New file, extracted from ...
	* src/ltlvisit/reducform.hh: ... here.
	* src/ltlvisit/basereduc.cc: Rename as ...
	* src/ltlvisit/basicreduce.cc: ... this, to match the function name.
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
	Adjust filenames.
	* src/ltlvisit/reducform.cc: Adjust includes.

	* src/ltlvisit/lunabbrev.hh: Revert superfluous change from
	2004-05-10.

2004-06-22  Thomas Martinez  <martinez@src.lip6.fr>

	* src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc,
	src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh
	src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test,
	src/tgbatest/reductgba.cc: 80 columns and style.

2004-06-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Typo.

2004-06-22  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc,
	src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
	bug in delayed simulation.

	* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
	src/tgba/tgbareduc.cc: bug in scc reduction.

2004-06-21  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc:
	There is bug in reduction with scc.
	* src/tgbatest/reduccmp.test: More test.

2004-06-17  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reductgba.test: Wrong test are removed.

2004-06-17  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/spotlbtt.test: We don't check the post-reduction
	with scc and delayed simulation.

	* src/tgbatest/ltl2tgba.cc: Adjust parameters.
	* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
	* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
	* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
	Remove some useless comments.
	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.

	* src/ltlvisit/reducform.cc: Correct some bug for multop.
	* src/ltltest/reduc.cc: Thinko
	* src/ltltest/equals.cc: Reduction compare

2004-06-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s.
	This fixes a memory leak observed by Soheib Baarir.

2004-06-16  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test: Test for
	reduction of tgba.

2004-06-15  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc: Add some option for the reduction of
	automata.
	* src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
	test for reduction of automata.
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
	to reduce a tgba.
	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
	of tgba for the reduction.
	* src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
	Add the reduction of automata.
	* src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
	Lot of mistake are corrected.
	* src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
	src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
	* src/ltltest/equals.cc, src/ltltest/reduccmp.test,
	src/ltltest/Makefile.am: Add a test for reduction.

2004-06-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/common.cc, iface/gspn/common.hh: Remove the
	class gspn_environment, and move it to ...
	* src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file
	as class declarative_environment.
	* src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh.
	(libltlenv_la_SOURCES): Add declenv.cc.
	* iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc,
	iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
	iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references
	to declarative_environment.

	* HACKING, src/sanity/style.test: NULL is not portable, prohibit it.
	* iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
	src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/syntimpl.cc: Use 0 instead of NULL.

2004-06-01  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ...
	* src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
	* src/ltltest/Makefile.am: Adjust.
	* src/ltlvisit/forminf.cc: Rename as...
	* src/ltlvisit/syntimpl.cc: ... this.
	* src/ltlvisit/syntimpl.hh: New file with definitions extracted
	from ...
	* src/ltlvisit/reducform.hh: ... this one.
	* src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust.

2004-05-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
	inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
	as ...
	(eventual_universal_visitor, inf_right_recurse_visitor,
	inf_left_recurse_visitor): ... these.
	(is_GF, is_FG): Move ...
	* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
	are only used here.
	(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
	(basic_reduce, basic_reduce_visitor): ... these.
	* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
	(reduce_visitor): ... this.
	* src/ltltest/inf.cc: Adjust calls.
	* src/sanity/style.test: Improve missing-space after coma detection.

2004-05-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)):
	Simplify.

	* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc: Use
	dynamic_cast instead of node_type_form_visitor, this is usually
	smaller.
	* src/ltlvisit/reducform.hh,
	src/ltlvisit/forminf.cc (node_type_form_visitor): Delete.
	* src/sanity/style.test: Two more checks.

2004-05-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/formlength.cc: Rename as ...
	* src/ltlvisit/length.cc: ... this.
	* src/ltlvisit/length.hh: New file, extracted from ...
	* src/ltlvisit/reducform.hh: ... here.
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh.
	(libltlvisit_la_SOURCES): Rename formlength.cc as length.cc.
	* src/ltltest/reduc.cc: Include length.hh.

	* src/ltlvisit/formlength.cc (length_form_vistor): Rename as ..
	(length_visitor): ... this.
	(form_length): Rename as ...
	(length): ... this.
	* src/ltlvisit/reducform.hh (form_length): Rename as ...
	(length): ... this.
	* src/ltltest/reduc.cc: Adjust.

	* src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove
	useless includes.

	* AUTHORS: Update.

	* src/ltlvisit/reducform.hh: Update Doxygen comments for
	previous change.

	* src/ltlvisit/reducform.hh (option): Rename as ...
	(reduce_options): ... this, and use it as a bit field so
	option can be combined easily.
	(reduce): Adjust argument.
	(reduce_form): Remove, not needed anymore.
	* src/ltlvisit/reducform.cc, src/ltltest/reduc.cc,
	src/tgbatest/ltl2tgba.cc: Adjust.

	* src/sanity/style.test: Catch {.*{ and }.*}.
	* src/sanity/80columns.test: Untabify files.
	* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.

	* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.

	* wrap/python/cgi/ltl2tgba.in: Typos.

2004-05-24  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Catch `;'-not-followed-by-space.
	* src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style.

	* src/ltlvisit/reducform.hh: Fix some Doxygen comments.

	* src/tgbatest/ltl2tgba.cc (syntax): Keep options sorted.

	* src/sanity/Makefile.am (EXTRA_DIST): Distribute 80columns.test
	and style.test.

	* src/ltltest/Makefile.am (EXTRA_DIST): Distribute formulae.txt.
	* src/ltltest/formulae.txt: New file (2200 LTL formulea generated
	by Wring).
	* src/ltltest/formules.ltl: Delete.
	* src/reduc.test: Read formulae.txt.

2004-05-24  Soheib Baarir  <Souheib.Baarir@lip6.fr>

	* iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface): Add
	the `inclusion' flag.
	* iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call
	inclusion_version when inclusion is set.
	* iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3,
	-e4, and -e5.

2004-05-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop,
	and dead_prop from the dead argument passed to the constructor.
	(tgba_succ_iterator_gspn): Stutter on dead transitions.
	(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
	(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
	* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
	dead argument.
	* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
	dead property.
	* iface/gspn/udcseltl.test: Try option -d.

	* src/sanity/style.test: Check the iface/ tree too.
	* iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style.

	* src/sanity/80columns.test: Check the iface/ tree too.
	* iface/gspn/dcswaveltl.test, iface/gspn/dcswavefm.test,
	iface/gspn/dcswaveeltl.test, iface/gspn/udcsltl.test,
	iface/gspn/udcseltl.test, iface/gspn/udcsfm.test,
	iface/gspn/udcsefm.test: Wrap to fit 80 columns.

2004-05-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Makefile.am (EXTRA_DIST, spot.html): Built the html
	documentation in $(srcdir) since it is distributed.
	* doc/Doxyfile.in (HTML_OUTPUT): Likewise.  Upgrade to Doxygen 1.3.7.

2004-05-17  Thomas Martinez  <martinez@src.lip6.fr>

	* src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style.

	* src/ltlvisit/basereduc.cc (spot): 80 columns.
	* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
	src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,
	src/tgbatest/ltl2tgba.cc (main): More option.
	* src/ltltest/inf.test: More test.

2004-05-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* wrap/python/buddy.i: Define typemap for input_buf and use it
	for fdd_extdomain.  Define const_int_ptr and use it for fdd_vars.

	* src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress.
	(bdd_allocator::bdd_allocator): Adjust.
	(bdd_allocator::extvarnum): Always call bdd_varnum(), so that
	it doesn't matter if the number of variable has been augmented
	externally.
	* src/misc/bddalloc.hh (bdd_allocator::varnum): Suppress.

	* src/ltlvisit/formlength.cc: Fix style to please sanity checks.

	* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.

	* src/tgbaalgos/neverclaim.cc: Fix them.
	* sanity/style.test: Diagnose semicolons with leading spaces.

	* src/ltlvisit/forminf.cc: Fix style to please sanity checks.
	Also avoid node_type_form_visitor where a dynamic_cast is done.

2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.

	* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
	* sanity/style.test: More tests.

	* src/tgbatest/ltl2tgba.cc (main): Fix style.
	* HACKING: Mention `else if'.

	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Do not output
	space before colon, and do not output the top-level formula using
	Spin's syntax.

2004-05-14  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc (main): Thinko.

	* src/ltlvisit/basereduc.cc (spot): Correct some mistakes.
	* src/ltlvisit/lunabbrev.cc (spot): Nothing change.
	* src/tgbatest/ltl2tgba.cc (main): More option to reduce
	formula.
	* src/tgbatest/spotlbtt.test: One more test.

2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/tostring.cc (to_spin_string_visitor,
	to_string_visitor): Do not parenthesize the top-level formula.
	* tgbatest/explicit.test, tgbatest/explpro2.test,
	tgbatest/explpro3.test, tgbatest/explprod.test,
	tgbatest/readsave.test, tgbatest/tgbaread.test,
	tgbatest/tripprod.test: Adjust expected output.
	* sanity/style.test: Fix regexes to catch an error seen in
	tostring.cc.

	* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):
	Do not try to erase state that are not found in H.
	Report from Soheib Baarir.

	* src/ltltest/reduc.test: Use ./defs and clean result.data.
	* src/ltltest/Makefile.am (CLEANFILES): Clean result.data.

2004-05-13  Thomas Martinez  <martinez@src.lip6.fr>

	* src/ltlvisit/Makefile.am: Copyright 2004.
	* src/ltltest/inf.test: More test.
	* src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot):
	Use dynamic_cast.
	* src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh,
	src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option
	to choose which rules applies to simplify the formula.

2004-05-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltltest/reduc.test: Typo.

	* src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens.
	(subformula): Recognize `ATOMIC_PROP OP_POST_POS' and
	`ATOMIC_PROP OP_POST_NEG'.
	* src/ltlparse/ltlscan.ll: Introduce the not_prop start condition,
	to restrict the set of atomic propositions allowed in places
	where they are not expected.  Make `true' and `false' case insensitive.
	* src/ltltest/parse.test, src/ltltest/tostring.test: More cases.
	* src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic
	propositions equal to "true" or "false".

2004-05-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last.

	* src/ltltest/reduc.test: POSIXify.

2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: New file.
	* src/sanity/Makefile.am (check-local): Run it.
	* src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc,
	src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc,
	src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc,
	src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc,
	src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc,
	src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style
	issues reported by style.test.

	* src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test,
	src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/reducform.hh: Fix copyright year, these files were
	created in 2004.

	* src/sanity/80columns.test: New file.
	* src/sanity/Makefile.am (check-local): Run it.
	* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
	src/ltltest/nenoform.test, src/ltltest/parseerr.test
        src/ltltest/tunabbrev.test, src/ltltest/reduc.cc,
	src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc,
	src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
	src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test,
	src/tgbatest/tripprod.test: Wrap long lines.

2004-05-10  Thomas MARTINEZ  <martinez@abacus.lip6.fr>

	* src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula.

	* src/ltltest/formules.ltl: A pattern of 2000 formulas.
	* src/ltltest/inf.test: Test some case of implies.
	* src/ltltest/inf.cc: Test some case of implies.
	* src/ltltest/reduc.test: Test reduction of a file of formula.
	* src/ltltest/reduc.cc: Test reduction of a formula.

	* src/ltlvisit/formlength.cc: Gives the lenght of a formula.
	* src/ltlvisit/forminf.cc: To know if a formula implies an other.
	* src/ltlvisit/basereduc.cc: Implement only basic reduction.
	* src/ltlvisit/reducform.cc: Implement reduction.
	* src/ltlvisit/reducform.hh: To reduce a formula.

2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>