ChangeLog

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

	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
	couvreur99_check_result::accepting_cycle): Rewrite the BFSs using
	the bfs_steps class.

	* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use
	the new bfs_steps class.

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

	* src/tgbaalgos/gv04.cc (gv04::result): New struct to compute
	counter examples.
	(gv04:check): Return a gv04::result.

2004-11-23  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/tau03opt.cc: Fix a warning.

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

	* src/tgbaalgos/gv04.cc (gv04): Inherit from ec_statistics.
	(gv04::check, gv04::push, gv04::pop): Update the statistics for
	randtgba.
	(gv04::print_stats): Print them here too.

	* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
	couvreur99_check_shy::check): Compute more statistics for
	randtgba.
	(couvreur99_check::print_stats): Print these here too.

	* src/sanity/style.test: Allow "'" after ",".

	* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly
	based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and
	src/tgbaalgos/tarjan_on_fly.hh former implementation.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
	tgbaalgos_HEADERS): Add them.
	* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the
	new algorithm.
	* src/tgbatest/emptchk.test: Test it.

2004-11-22  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc,
	src/tgbaalgos/weight.hh: New files.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
	src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
	capability.
	* src/tgbatest/randtgba.cc: Print these statistics.
	* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
	condition.
	* src/tgbatest/emptchk.test: Test tau03opt search.

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

	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc,
	src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03.cc,
	src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix
	copyright year, and do not include <iterator>.

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

	* src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics.
	(ce_stat): New struct.

2004-11-17  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo.
	* src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now
	the original one.
	* src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files
	implementing most of all the optimisations of tau03.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public.
	* src/tgbatest/tba_samples_from_spin.test: Test them.

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

	* src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh,
	src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos.

	* src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files
	from tba_samples_from_spin.
	* src/tgbatest/tba_samples_from_spin.test: Get these example files
	from $srcdir, for the sake of VPATH builds.
	(light_run): Remove, not needed.

	* src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
	src/misc/escape.hh, src/misc/freelist.hh, src/misc/hash.hh,
	src/misc/hashfunc.hh, src/misc/minato.hh, src/misc/modgray.hh,
	src/misc/random.hh, src/misc/version.hh, src/tgba/state.hh: More
	Doxygen groups.

2004-11-17  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/magic.hh: Fix a comment and remove se05 interface.
	* src/tgbaalgos/magic.cc: Fix a comment.
	* src/tgbaalgos/se05.hh: New file.
	* src/tgbaalgos/se05.cc: Fix a comment.
	* src/tgbaalgos/tau03.hh: New file.
	* src/tgbaalgos/tau03.cc: New file.
	* src/tgbaalgos/Makefile.am: Add it.
	* src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check.
	* src/tgbatest/randtgba.cc: Add tau03 new emptiness check.
	* src/tgbatest/emptchkr.test: Fix a comment.
	* src/tgbatest/tba_samples_from_spin/explicit1_1.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_2.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_3.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_4.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_5.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_6.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_7.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_8.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_9.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_1.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_2.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_3.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_4.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_5.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_6.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_7.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_8.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_9.tba: New files
	* src/tgbatest/tba_samples_from_spin.test : New test.
	* src/tgbatest/Makefile.am: Add it.

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

	* src/tgba/tgba.hh, src/tgbaalgos/dotty.hh,
	src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
	src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
	src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
	src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
	src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
	src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
	src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
	src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.

	* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
	src/ltlast/constant.hh, src/ltlast/formula.hh,
	src/ltlast/multop.hh, src/ltlast/refformula.hh,
	src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
	src/ltlparse/public.hh, src/ltlvisit/apcollect.hh,
	src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh,
	src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.hh, src/ltlvisit/length.hh,
	src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen
	groups for LTL algorithms and types.
	* doc/Makefile.am (fast-doc): New target.

	* src/misc/hashfunc.hh: Include cstddef to define size_t, and guard
	the file for multiple inclusions.

	* src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
	src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
	src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
	src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
	src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
	src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
	src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
	groups in the documentation.  Presently this only covers the
	tgba/ directory, and the emptiness-check algorithms.
	* doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
	in src/evtgbaparse/.

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

	* src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the
	functionality of the old tgba_tba_proxy.
	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
	tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
	each state, skipping the `bddtrue' stage now used only in
	tgba_sba_proxy.  Doing so removes approximately 6% of states in
	the degeneralized tests of spotlbtt.test.
	(tgba_sba_proxy): Implement it.
	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
	to take a tgba_sba_proxy.
	* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
	never_claim_reachable().

	* src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash.
	* src/tgba/tgbaproduct.cc (state_product::hash): Likewise.

	* src/misc/hashfunc.hh (wang32_hash): New file and function,
	extracted from...
	* src/evtgba/product.cc (evtgba_product_state::hash): ... here.
	* src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh.

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

	* src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness
	check, degeneralize the automaton only if it has too much
	acceptance conditions.  This makes it easier to reproduce runs
	of randtgba.
	* src/tgbatest/emptchk.test: Adjust.

2004-11-15  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/magic.cc: Fix a stupid bug.
	* src/tgbaalgos/se05.cc: Fix the same bug.
	* src/tgbatest/Makefile.am: Signify that emptchkr.test pass.

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

	* tgbatest/randtgba.cc: Add options -e and -r.
	* tgbatest/emptchkr.test: New file.
	* src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak
	if debug==false.

	* src/tgbaalgos/randomgraph.cc (random_graph): Do declare all the
	acceptance conditions in the produced automaton, in case they are
	not actually used.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the
	supplied stream, not std::cout.

2004-11-15  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/magic.cc: Add a bit state hashing version.
	* src/tgbaalgos/se05.cc: Add a bit state hashing version.
	* src/tgbaalgos/magic.hh: Make them public.
	* src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks.
	* src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test.
	* src/tgbatest/dfs.test: Introduce new characteristic explicit tests.

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

	* wrap/python/cgi/ltl2tgba.in: Add options to check the produced
	automata for emptiness, using the existing algorithms.
	* wrap/python/spot.i: Declare spot::explicit_magic_search,
	and spot::explicit_se05_search as allocating their output.

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

	* configure.ac: Check for srand48 and drand48.
	* src/misc/random.cc (srand, drand): Use srand48 and drand48 if
	available.

	* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS)
	(libtgbaalgos_la_SOURCES): Add them.
	* src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public.
	* src/tgbatest/randtgba.cc: New file.
	* src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it.
	* src/tgbatest/readsave.test: Check a random graph.

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

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

	* src/evtgbaparse/public.hh (evtgba_parse): Fix doxygen comments.
	* src/tgbaalgos/projrun.hh (project_tgba_run): Likewise.

	* src/tgbaalgos/emptiness.hh (print_tgba_run): Document it.

	* src/tgbaalgos/replayrun.hh,
	src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
	option to decide whether the output should look like that of
	print_tgba_run() or a complete debug trace.
	* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
	debug=true.

	* iface/gspn/ltlgspn.cc (main): Adjust to recent changes to
	src/tgbaalgos/magic.cc, call explicit_magic_search() instead of
	building a spot::magic_search.
	* iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run().

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

	* src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test
	and se05.test.

	* src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword
	some help strings.

2004-11-09  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/magic.cc: rewrite to externalize the heap and
	prepare it to a bit state hashing version.
	* src/tgbaalgos/magic.hh: adapt to the new interface of
	magic_search and se05_search.
	* src/tgbaalgos/se05.cc: new file.
	* src/tgbaalgos/Makefile.am: Add it.
	* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
	* src/tgbatest/emptchk.test: more tests.
	* src/tgbatest/dfs.test: new file.
	* src/tgbatest/Makefile.am: Add it.

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

	* src/tgbaalgos/emptiness.cc (print_tgba_run): Output the
	labels as formulae rather than bdd sets.

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

	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path):
	Rewrite as ...
	(couvreur99_check_result::accepting_cycle): ... this less complex
	implementation.
	(couvreur99_check_result::complete_cycle): Delete.
	* src/tgbatest/emptchke.test: More explicit examples.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Do not leak
	the initial state when no valid outgoing transition is found.

	* src/tgbaparse/tgbaparse.yy: Add `%destructor's so the parser
	does not leak on errors.
	* src/tgbatest/ltl2tgba.cc: Free the automata if it could not be
	fully parsed.

	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run):
	Remove spurious FIXME.

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

	* src/evtgbaalgos/save.cc (save_bfs::output_acc_set): Sort
	acceptance conditions in the output.
	* src/evtgbatest/readsave.test, src/evtgbatest/product.test: Adjust.

	* src/tgbaalgos/rundotdec.cc (tgba_run_dotty_decorator::link_decl):
	Typo.

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

	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::process_link):
	Adjust prototype.

	* src/tgba/tgba.hh, src/tgba/tgba.cc
	(tgba::number_of_acceptance_conditions): New method.
	* src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it.

	* wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh,
	tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and
	tgbaalgos/rundotdec.hh.

	* src/tgbaalgos/lbtt.cc (lbtt_bfs::process_link): Adjust prototype.

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

	* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
	src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
	as third parameter.
	* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
	dotty_bfs::process_link): Use the decorator.
	* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
	is given.
	* src/tgbatest/emptchk.test: Exercise -g.

	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl.

	* tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc
	(tgba_reachable_iterator::process_link): Take the state* as arguments
	in addition to the state numbers.
	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
	(tgba_explicit::copy_acceptance_conditions_of): New method.
	* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
	copy_acceptance_conditions_of.
	(dupexp_iter::process_state, duplex_iter::declare_state,
	dupexp_iter::name_): Remove.
	(dupexp_iter::process_link): Adjust prototype, and format
	the state here rather than in process_state.
	* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
	of process_link.

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>

	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine
	fair_loop_approximation when branching postponement is not used.

	Cache formula translations, and canonize formulae before doing
	branching postponement.
	* src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with
	bits extracted from fill_dests and ltl_to_tgba_fm.
	(fill_dests, ltl_to_tgba_fm): Adjust to use formula_canonizer.

	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
	fair_loop_approx.
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the
	fair_loop_approx optimization.
	(ltl_promise_visitor, ltl_possible_fair_loop_visitor,
	possible_fair_loop_checker): New classes.
	* src/tgbatest/ltl2tgba.cc: Add the -L option.
	* src/tgbatest/spotlbtt.test: Exercise fair_loop_approx.
	* wrap/python/cgi/ltl2tgba.in: Make it an option.

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

	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
	branching_postponement.
	* src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
	from ltl_to_tgba_fm().
	(ltl_to_tgba_fm): Implement the branching_postponement optimization.
	* src/tgbatest/ltl2tgba.cc: Add the -p option.
	* src/tgbatest/spotlbtt.test: Exercise branching postponement.
	* wrap/python/cgi/ltl2tgba.in: Make it an option.

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

	* src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify
	some GCC version.  Report from Denis Poitrenaud.

	* wrap/python/cgi/ltl2tgba.in: Fix output HTML.

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

	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then
	free all formulae entered into canonical_succ, to avoid errors
	when a formula is entered into canonical_succ but not into
	formulae_seen.
	* src/tgbatest/ltl2tgba.test: Add a new test, and check with -f.
	Report from Thomas Martinez.

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

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

	* configure.ac, NEWS: Bump version to 0.0t.
	* HACKING: Update tools requirements.
	* src/sanity/Makefile.am (EXTRA_DIST): Distribute includes.test.

	* src/sanity/Makefile.am, src/sanity/includes.test: New files.
	* src/Makefile.am (SUBDIRS): Add sanity.
	* configure.ac: Output src/sanity/Makefile.in.

	* src/tgbatest/Makefile.am (check_PROGRAMS): Move ltl2tgba ...
	(noinst_PROGRAMS): ... here.
	* iface/gspn/Makefile.am (check_PROGRAMS): Rename as ...
	(noinst_PROGRAMS): ... this.

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

	* src/tgbatest/explicit.test: Reorder bdd variables in output.
	Report from Denis Poitrenaud.

	* wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics
	when show_never_claim.  Change the title to LTL-to-TGBA.
	Suggested by Denis Poitrenaud.

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

	* wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's
	version a separate variable.

	* wrap/python/cgi/ltl2tgba.in: Pass the formula to
	never_claim_reachable, and cgi.escape its output.
	Lighten the color a bit.

	* src/tgbaalgos/gtec/ce.hh, src/misc/freelist.hh,
	src/tgba/bddprint.hh: Fix Doxygen comments.

	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document
	arguments.
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
	New method.
	(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
	Use it.

	* wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
	the new variable dot_bgcolor.

	* wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output
	using this new function.

	* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
	* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.

2004-04-21  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/ltlvisit/tostring.hh (to_spin_string): New function.
	Convert a formula into a string parsable by Spin.
	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
	Print the never claim in Spin format of a degeneralized TGBA.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
	never claim in Spin format of a degeneralized TGBA.
	* src/tgbatest/ltl2neverclaim.test: New file.
	* src/tgbatest/Makefile.am: Add it.

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

	* src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode
	when valgrind is not used.
	Reported by Denis Poitrenaud.

	* src/tgba/tgba.hh (tgba::succ_iter): Doco.
	* src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document
	it.
	Reported by Denis Poitrenaud.

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

	* iface/gspn/ltlgspn.cc (main) [SSP]: Use the standard
	counter-example computation for -e5 too.

	* iface/gspn/ltlgspn.cc (main) [!SSP]: Do not accept -e3, -e4, or -e5.
	(main) [SSP]: Use the standard counter-example computation
	for -e and -e1.

2004-04-15  Soheib Baarir  <Souheib.Baarir@lip6.fr>
	    Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Rename EESRG as SSP.
	* iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
	iface/gspn/dottyeesrg.cc: Rename as ...
	* iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc:
	... these.  Adjust all classes and function names.
	* iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes
	filenames and function names.
	* m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS.

	* src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find):
	Rewrite.
	(numbered_state_heap_hash_map::index): New functions.
	(numbered_state_heap_hash_map::filter): Delete.
	* src/tgbaalgos/gtec/nsheap.hh
	(numbered_state_heap_hash_map::index): New functions.
	(numbered_state_heap_hash_map::filter): Delete.
	* iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find,
	numbered_state_heap_eesrg_semi::index): Rewrite.
	(numbered_state_heap_eesrg_semi::filter): Remove.
	* src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc:
	Adjust to use find() and index() instead of filter()..


	* iface/gspn/eesrg.cc (connected_component_eesrg::has_state):
	Free filtered states.
	(emptiness_check_shy_eesrg): New class.
	(emptiness_check_eesrg_shy): New function.
	* iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
	* iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
	* * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
	(emptiness_check_shy::check): Move arc, num, succ_queue, and todo
	as attributes.
	(emptiness_check_shy::find_state): New virtual function.

2004-04-14  Soheib Baarir  <Souheib.Baarir@lip6.fr>
	    Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/ltlgspn.cc (connected_component_eesrg,
	connected_component_eesrg_factory, numbered_state_heap_eesrg_semi,
	numbered_state_heap_eesrg_const_iterator,
	numbered_state_heap_eesrg_factory_semi): New classes.
	(emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi,
	counter_example_eesrg): New functions.
	* iface/gspn/eesrg.hh (emptiness_check_eesrg_semi,
	emptiness_check_eesrg_shy_semi, counter_example_eesrg): New
	functions.
	* iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.

2004-04-14  Soheib Baarir  <Souheib.Baarir@lip6.fr>

	* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg,
	state_gspn_eesrg): Compute the array of all successors of the
	right state beforehand, pass it to Greatspn (left automata) at
	once, let it compute the resulting synchronized arcs, and iterate
	on that result.

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

	* src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory,
	numbered_state_heap_hash_map_factory): New class.
	* src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory):
	Implement it.
	* src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check,
	emptiness_check_shy::emptiness_check_shy): Take a
	numbered_state_heap_factory argument.
	* tgbaalgos/gtec/status.hh
	(emptiness_check_status::emptiness_check_status): Likewise.
	(emptiness_check_status::h): Make it a numbered_state_heap*.
	* src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc,
	tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h.

	* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc:
	Delete and split into ...
	* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
	src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
	src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
	src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
	these new files.
	* src/tgbaalgos/gtec/Makefile.am: New file.
	* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
	Recurse into gtec and link gtec/libgtec.la.
	(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
	and emptinesscheck.cc.
	* configure.ac: Output src/tgbalagos/gtec/Makefile.
	* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
	* README: Update tree description.

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

	* src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator,
	numbered_state_heap, numbered_state_heap_hash_map): New classes.
	* src/tgbaalgos/emptinesscheck.cc
	(numbered_state_heap_hash_map_const_iterator): New class.
	(numbered_state_heap_hash_map): Implement it.

	* src/tgbaalgos/emptinesscheck.hh
	(explicit_connected_component_factory,
	connected_component_hash_set_factory): New classes.
	(counter_example::counter_example): Take an
	explicit_connected_component_factory factory argument.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

	* src/tgbaalgos/emptinesscheck.hh (explicit_connected_component):
	New class.
	(counter_example::connected_component_set): Rename as ...
	(connected_component_hash_set): ... this, and inherit from
	explicit_connected_component.
	(counter_example::accepting_path, counter_example::complete_cycle):
	Take an explicit_connected_component argument instead of a
	connected_component_set.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

	* src/tgbaalgos/emptinesscheck.hh
	(counter_example::connected_component_set::has_state): Return
	a const state* and behave like h_filt.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

	* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move
	into ...
	(emptiness_check_shy): This new subclass of emptiness_check.
	* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
	iface/gspn/ltlgspn.cc: Adjust.

	* src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig.

	* src/tgbaalgo/semptinesscheck.hh (counter_example): New class,
	extracted from ...
	(emptiness_check): ... here.
	* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
	iface/gspn/ltlgspn.cc: Adjust.

	* wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx)
	($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c.

	* src/tgbaalgo/semptinesscheck.hh (emptiness_check_status): New class,
	extracted from ...
	(emptiness_check): ... here.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

	* src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted
	from ...
	(emptiness_check): ... here.
	(emptiness_check::root): Redefined as a scc_stack object.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

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

	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
	Do not visit a state more than once.  Report from Soheib Baarir.

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

	* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var
	variables from a shared bdd_dict.  Register Next variables as
	anonymous variables.
	(translate_dict::translate_dict, translate_dict::~translate_dict,
	translate_dict::register_proposition,
	translate_dict::register_a_variable,
	translate_dict::register_next_variable,
	translate_dict::dump, translate_dict::var_to_formula,
	ltl_to_tgba_fm): Adjust.
	(translate_dict::dict): New attribute.
	(translate_dict::a_map, translate_dict::a_formula_map,
	translate_dict::var_map, translate_dict::var_formula_map): Delete.

	* src/misc/freelist.cc (free_list::remove): Work around
	invalidated iterators.
	* tgba/bdddict.cc (unregister_variable): New methods,
	extracted from ...
	(bdd_dict::unregister_all_my_variables): ... here.
	* tgba/bdddict.hh (unregister_variable): Declare them.

2004-03-23  Alexandre DURET-LUTZ  <adl@src.lip6.fr>

	* src/misc/freelist.hh (free_list::remove, free_list::insert): New
	methods.
	* src/misc/freelist.cc (free_list::register_n,
	free_list::releases_n): Rewrite using free_list::remove and
	free_list::insert.
	(free_list::remove, free_list::insert): New methods.
	* src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables):
	New method.
	(bdd_dict::annon_free_list): New subclass.
	(bdd_dict::free_annonymous_list_of_type_of): New attribute.
	* src/tgba/bdddict.cc (bdd_dict::register_all_variables_of,
	bdd_dict::unregister_all_my_variables): Handle anonymous variables
	too.
	(bdd_dict::register_anonymous_variables,
	bdd_dict::annon_free_list::annon_free_list,
	bdd_dict::annon_free_list::extend): New methods.

	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path)
	Fix handling of PATH when backtracking.  Report from Soheib Baarir.

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

	Move the free_list management into a separate class for reuse.

	* src/misc/freelist.hh, src/misc/freelist.cc: New files.
	* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
	* src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
	make dump_free_list visible.
	* src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
	all the code into free_list::register_n() and
	bdd_allocator::extend(), and call the former.
	(bdd_allocator::release_variables): Move all the code into
	free_list::release_n() and call it.
	(bdd_allocator::extend): New method.
	* src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;

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

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