ChangeLog

2012-03-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	python: fix return value of emptiness_check_instantiator

	* wrap/python/spot.i: Fix typemap for
	emptiness_check_instantiator::construct.  The previous code used
	to turn (None, "error") into simply ("error").
	* wrap/python/ajax/spot.in: Fix handling or errors when
	instantiating emptiness checks.

2012-02-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Summarize recent changes.

2012-02-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make all python code compatible with Python 2.x and Python 3.x.

	* wrap/python/buddy.i (__le__, __lt__, __eq__, __ne__, __ge__
	__gt__): New operators for bdd.
	* wrap/python/spot.i (__le__, __lt__, __eq__, __ne__, __ge__
	__gt__, __hash__): New operators for formula.
	(nl_cout, nl_cerr): New functions.
	* wrap/python/tests/bddnqueen.py,
	wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
	wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
	wrap/python/tests/minato.py, wrap/python/tests/modgray.py: Adjust
	to the new print syntax by using sys.output.write() or nl_cout()
	instead.
	* wrap/python/tests/optionmap.py: Remove all print calls.
	* wrap/python/ajax/spot.in: Massive adjustments in order to work
	with both Python 2 and 3.  In python 3, reopening stdout as
	unbuffered requires it to be open as binary, which in turns
	requires any string output to be encoded manually.  BaseHTTPServer
	and CGIHTTPServer have been merged into http.server, so we have
	to try two different import syntaxes.  execfile no longer exists,
	so it has to be emulated.
	This also fixes two bugs where the script would segfault on
	empty input, or when calling Tau03 on automata with less then
	one acceptance conditions.

2012-02-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix computation of PYTHONINC for Python 3.

	* m4/pypath.m4: The print syntax changed in Python 3, so use
	sys.stdout.write for compatibility with all versions.

2012-02-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING: Minor updates and corrections.

2012-02-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a race condition on the CGI script.

	* wrap/python/ajax/spot.in: Create all cache files in a temporary
	directory, and only rename this directory at the end.  This way if
	two processes are processing the same request, they won't attempt
	to populate the same directory (and only one of the first of two
	renames will succeed, but that is OK).

2012-01-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a segfault reported by Etienne Renault using dve2check.

	* src/misc/intvcmp2.cc (stream_compression_base::run): Fix a case
	where the "id" of the compression to use would be miscalculated,
	causing wrong values to be encoded.
	* src/tgbatest/intvcmp2.cc: Add this particular test case.

2012-01-20  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Add missing dates.

2012-01-19  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* configure.ac, NEWS: Bump version to 0.8.2a.

2012-01-19  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.2.

	* configure.ac, NEWS: Bump version to 0.8.2.

2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Small speedup in safra_tree::compare().

	* src/tgba/tgbasafracomplement.cc (safra_tree::compare): Improve
	the order of the tests.

2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention the last two changes.

2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement a unicity table for states created by tgba_tba_proxy.

	Suggested by Nikos Gorogiannis.

	* src/tgba/tgbatba.hh (tgba_tba_proxy::create_state): New method.
	(tgba_tba_proxy::uniq_map_): New attribute.
	* src/tgba/tgbatba.cc (state_tba_proxy): Use the default
	copy constructor.  Empty the destructor.  Implement an empty
	destroy() method.  Use addresses for comparison.  Make clone()
	a no-op.
	(tgba_tba_proxy): Allocate and deallocate the unicity table.
	Implement create_sates().
	(tgba_tba_proxy, tgba_sba_proxy, tgba_tba_proxy_succ_iterator):
	Adjust state construction to call create_state().

2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Minor speedups in tgba_safra_complement().

	* src/tgba/tgbasafracomplement.cc (safra_tree:succ_create): Do not
	lookup *i twice, and do not copy it->second.
	(safra_tree::normalize_siblings): Do not lookup *node_it before
	insertion.

2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/eltlparse/eltlparse.yy (realias): Add a useless return to
	fix a g++ warning.

2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* bench/ltlclasses/run: Typo in comment.

2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make it possible not to build Python bindings.

	* configure.ac: Add a --disable-python option tied to
	a USE_PYTHON conditional.
	* README: Document the option.
	* wrap/Makefile.am: Use the conditional.

2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix position of the Send button with WebKit.

	* wrap/python/ajax/css/ltl2tgba.css: Fix position of the "Send"
	button with WebKit.  The folding arrow icon had a vertical border
	that overlapped with the next line.

2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/spot.py: Add a required "None" second
	argument to utime().

2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	minimize_wdba() failed to fully minimize some automata.

	* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
	algorithm to use colors.  The previous implementation was an
	incorrect approximation.
	* src/tgbatest/wdba2.test: New file showing two equivalent
	formulas that were minimized in automata with different sizes.
	* src/tgbatest/Makefile.am: Add it.

2012-01-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent fixes.

2012-01-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a 'make check' failure when valgrind is not installed.

	* src/kripketest/defs.in (run2): Remove this function.  It was
	incorrectly trying to run valgrind even when valgrind is not
	installed.
	* src/kripketest/kripke.test: Simplify and use run().

2012-01-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Do use of tr1::unordered_map with G++ 4.0.0.

	* m4/stl.m4 (AC_HEADER_TR1_UNORDERED_MAP): Add some code so
	we don't pick a broken tr1::unordered_map.

2012-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* lrde-upload.sh: Retrieve the package version from configure.ac.

2012-01-05  Ala-Eddine Ben-Salem  <ala@lrde.epita.fr>

	Fix detection of the last iteration of minimize_dfa().

	* src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the
	last iteration.  An extra iteration case could be missed in case
	where a split generates only singletons, and yet predecessor
	classes need to be refined.

2012-01-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix computation of length of LTL formulas.

	* src/ltlvisit/length.cc: Fix computation for ltl::multop
	operator. "a&b&c" was reported with length 3, ignoring the
	"&" operators, because of a typo.
	* src/ltlvisit/length.hh: Fix description to correctly
	reflect this change intended since 2010-01-22.
	* src/ltltest/length.test, src/ltltest/length.cc: New files.
	* src/ltltest/Makefile.am: Add them.

2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* configure.ac, NEWS: Bump version to 0.8.1a.

2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.1.

	* configure.ac, NEWS: Bump version to 0.8.1.

2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Summarize recent fixes.

2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix VPATH builds, now that hash.hh include _config.h

	* iface/dve2/Makefile.am, src/eltlparse/Makefile.am
	src/eltltest/Makefile.am, src/evtgba/Makefile.am,
	src/evtgbaalgos/Makefile.am, src/evtgbaparse/Makefile.am,
	src/evtgbatest/Makefile.am, src/kripke/Makefile.am,
	src/kripketest/Makefile.am, src/ltlast/Makefile.am,
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am, src/misc/Makefile.am,
	src/neverparse/Makefile.am, src/saba/Makefile.am,
	src/sabaalgos/Makefile.am, src/sabatest/Makefile.am,
	src/sanity/Makefile.am, src/tgba/Makefile.am,
	src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am,
	src/tgbaparse/Makefile.am, src/tgbatest/Makefile.am,
	wrap/python/Makefile.am (AM_CPPFLAGS): Make sure
	$(top_builddir)/src is included.

2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Perform WDBA minimization before degeneralization.

	There is no point in degeneralizing an automaton if it can be WDBA
	minimized.  Doing so will only augment the number of states and
	slow down the powerset construction used by the WDBA minimization.

	* src/tgbatest/babiak.test: New file.  It includes 5 formulae
	which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
	translate if degeneralization and WDBA minimization were both
	requested.
	* src/tgbatest/Makefile.am (TESTS): Add it.
	* src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
	degeneralization.  The above formulae are now all translated in a
	few seconds.

2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Don't rely on the g++ version to include tr1/unordered_map and co.

	The previous setup failed with clang++ 3.0.

	* m4/stl.m4: New file.
	* configure.ac: Call AC_HEADER_UNORDERED_MAP,
	AC_HEADER_TR1_UNORDERED_MAP, and AC_HEADER_EXT_HASH_MAP.
	* src/misc/hash.hh: Include _config.h, and used the
	SPOT_HAVE_UNORDERED_MAP, SPOT_HAVE_TR1_UNORDERED_MAP,
	or SPOT_HAVE_EXT_HASH_MAP defines to decide which
	file to include.

2011-12-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix mkdir error in ajax/spot.in.

	* wrap/python/ajax/spot.in: Do not print an error
	when attempting to create an existing directory.
	Reported by Étienne Renault.

2011-11-29  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix build failure during "make check" on MacOS X.

	* src/kripketest/Makefile.am (LDADD): Remove a broken dependency.
	Reported by Yann Thierry-Mieg.
	* src/sanity/style.test: Make sure it does not appear again.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Sort alphabetically.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove the old CGI interface.

	* wrap/python/cgi-bin: Remove this directory.
	* wrap/python/Makefile.am (SUBDIRS): Remove it.
	* configure.ac, README, wrap/python/ajax/README: Likewise.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Undocument `.' from the web interface.

	* wrap/python/ajax/ltl2tgba.html: Remove `.'
	from the list of acceptable symbols for AND.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS, configure.ac: Bump version to 0.8a.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.

	* NEWS, configure.ac: Bump version to 0.8.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove spotref.pdf.

	* doc/Doxyfile.in: Do not generate LaTeX output.
	* doc/Makefile.am: Do not build spotref.pdf.
	* NEWS, README: Adjust.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix some Doxygen errors.

	* src/kripke/kripkeexplicit.hh: Reindent, and fix
	some comments.

2011-11-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add more nodes when resizing BDD table.

	* src/misc/bddalloc.cc (bdd_allocator::initialize): Call
	bdd_setmaxincrease(500000), because the default is 50000,
	which cause garbage collection to occur too often.

2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention the Kripke I/O.

2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Don't flush the stream on each new line, when writing automata.

	* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/dotty.cc,
	src/tgbaalgos/save.cc: Prefer '\n' over std::endl to speedup I/O.
	* src/ltltest/genltl.cc (syntax): Use '\n' too, although it won't
	make a big difference.

2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add an ltl2tgba option to read Kripke structure.

	Also offers two ways to output Kripke structures.

	* src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
	: Simplify includes.
	* src/kripke/kripkeprint.hh (kripke_save_reachable,
	kripke_save_reachable_renumbered): New declarations.
	(KripkePrinter): Move and rename...
	* src/kripke/kripkeprint.cc (kripke_printer): ... here.
	(kripke_printer_renumbered): New class.
	(kripke_save_reachable, kripke_save_reachable_renumbered): New
	function.
	* src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
	structures.
	* iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
	* iface/dve2/defs.in (run2): Remove.
	* iface/dve2/kripke.test: Adjust tests.

2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Add Thomas Badie.

2011-05-07  Thomas Badie  <badie@lrde.epita.fr>

	Add text I/O for Kripke structures.

	* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
	src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
	* src/kripke/Makefile.am: Add them.
	* src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
	src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
	src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
	files.
	* src/kripkeparse/Makefile.am: Add them.
	* src/kripketest/bad_parsing.test, src/kripketest/defs.in,
	src/kripketest/kripke.test, src/kripketest/origin,
	src/kripketest/parse_print_test.cc: New files.
	* src/kripketest/Makefile.am: Add them.
	* src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
	* README: Document src/kripketest/ and src/kripkeparse/.
	* configure.ac: Generate src/kripkeparse/Makefile,
	src/kripketest/Makefile, src/kripketest/defs.
	* iface/dve2/defs.in (run2): New function.
	* iface/dve2/dve2check.cc (syntax, main): Add option -gK.
	* iface/dve2/kripke.test: New file.
	* iface/dve2/Makefile.am (TESTS): Add kripke.test.

2011-11-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix bench/emptchk/pml2tgba.pl for more recent Spin version.

	* bench/emptchk/pml2tgba.pl: Stop checking for version start lines
	depending on the Spin version.  This check was never always
	correct.  Reported by Étienne Renault.

2011-11-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Update formulae.ltl not to use uncommon operators.

	* bench/emptchk/formulae.ltl: Do not use + and * in the list of
	formulas.  Use | and & instead.  The * operator was removed on
	2010-01-30.  Reported by Étienne Renault.

2011-11-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	More documentation.

	* src/tgbaalgos/randomgraph.hh: Document the fact that adding
	acceptance conditions to the graph may generate graphs that do not
	have any accepting cycle.

2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Display transition annotations in dotty output.

	* src/tgbaalgos/dotty.cc (process_link): Call
	transition_annotation().  Reported by Nikos Gorogiannis.
	* src/tgba/tgba.hh (transition_annotation): More documentation.
	* NEWS: Mention this change.

2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Add an entry for the previous fix.

2011-11-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fully quote guards used by neverclaims.

	Especially with should write !(p0) and not !p0, because p0 is
	usually #define'd by the user and he may have forgotten to quote
	the value of the macro.  This issue was discovered by Kristin
	Yvonne Rozier and diagnosed by Gerard Holzmann.

	* src/tgbaalgos/neverclaim.cc (process_link): Call
	to_spin_string(..., true) to fully parentheses the string.
	* src/tgbatest/neverclaimread.test: Add a test.

2011-11-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a g++-4.7 warning about a variable used only in an assert().

	* src/tgbaalgos/weight.cc (inc_weight_handler)
	(dec_weight_handler): Remove these assertions that require the
	loop the be completed, and use break to exit ASAP.

2011-11-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Allow neverclaim guards of the form `!(x)' or `! (x)'.

	* src/neverparse/neverclaimscan.ll: Make the space between `!' and
	`(' optional.  This fixes the patch from 2011-02-07 that made this
	space mandatory...
	* src/tgbatest/neverclaimread.test: Augment test case.

2011-10-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Better documentation for print_tgba_run.

	* src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the
	documentation after a report from Nikos Gorogiannis.

2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/finite.test: Swap -e and -E after change from 2011-07-26.

2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent fixes.

2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Safra: Fix usage of multiple acceptance conditions and fix text output.

	* src/tgba/tgbasafracomplement.cc
	(tgba_safra_complement::tgba_safra_complement)
	(tgba_safra_complement::succ_iter): Correct the declaration and
	use of multiple acceptance conditions.
	(state_complement::to_string): Output the L set, not U.  The previous
	code caused different states to share the same names, causing issues
	with the text-based output (state with identical names get merged).
	* src/tgba/tgbasafracomplement.hh
	(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
	store BDDs.
	* src/tgbatest/complementation.cc: Implement a new "-b" option
	to output automata in Spot's syntax.
	* src/tgbatest/complementation.test: Add a test-case supplied
	by Martin Dieguez Lodeiro.
	* THANKS: Add Martin.

2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgba/tgbasafracomplement.cc: Fix two asserts.

2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Improve the print_safra_automaton output.

	* src/tgba/tgbasafracomplement.cc (print_safra_tree): Fix output in
	case of hash collision.  Use the actual states to get a number, not
	their hash value.
	(print_safra_automaton): Output a mapping of values to states names.
	(safra_tree_automaton::get_sba): New method, used by
	print_safra_automaton.

2011-08-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix errors reported by clang++-2.9.

	* src/evtgbaalgos/tgba2evtgba.cc (process_link): Fix prototype
	to match tgba_reachable_iterator::process_link.
	* src/ltlvisit/tunabbrev.hh: Add using super::visit, so that the
	other visit() method are in scope when we overload one.
	* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc (start, end,
	process_link): Remove these empty methods.  The default
	implementations are empty too, and process_link had the
	wrong prototype.
	* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc
	(start, end, process_link): Likewise.

2011-08-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Improve SCC simplification by removing implied acceptance conditions.

	Spot 0.7.1 used to need 190 acceptance conditions to translate the
	188 literature formulae.  With this patch we are down to 185.
	That's not an impressive, but there are only ~20 formulae that
	require more than 1 acceptance conditions; hence little room for
	improvement.

	* src/misc/bddlt.hh (bdd_hash): New function.
	* src/misc/accconv.hh, src/misc/accconv.cc: New files.
	* src/misc/Makefile.am: Add them.
	* src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
	to record all combination of acceptance conditions occurring in a SCC.
	* src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
	* src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
	conditions that are always implied by another acceptance
	conditions.  Previously, we only removed acceptance conditions
	that where always present in accepting SCCs.
	* src/tgbatest/sccsimpl.test: New file.
	* src/tgbatest/Makefile.am (TESTS): Add it.

2011-08-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Refine yesterday's change to the degeneralization.

	This avoids a small regression on the size of degeneralized
	automata of our usual list of literature formulae.

	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
	(tgba_tba_proxy::union_acceptance_conditions_of_original_state):
	New method.
	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting
	states, ignore only the last expected acceptance condition if its
	common to all outgoing transitions AND if it is not used by any
	outgoing transitions of the destination.

2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make sure the degeneralization is idempotent (up to renaming of
	states).

	* src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the
	acceptance conditions that are common to all outgoing transitions
	of this state.  This helps to make the degeneralization
	idempotent.
	* src/tgbatest/degenid.test: New test case.
	* src/tgbatest/Makefile.am: Add it.

2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix escaping of state name in save_reachable()'s output.

	* src/tgbaalgos/save.c (process_state): Escape quotes in the
	name of source and destination states.  This fixes a side bug
	in the upcoming degenid.test test case.

2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Running `ltl2tgba -R1q -R1t -N` would degeneralize before and
	after the simulation-reduction.

	Report from Tomáš Babiak <xbabiak@fi.muni.cz>.

	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
	a tgba as input.
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
	state_is_accepting() only if this tgba turns out to be
	a tgba_sba_proxy.  Otherwise check the acceptance of one
	outgoing transition as we do in dotty_bfs since 2011-03-05.
	* src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
	calling never_claim_reachable() if we know the automaton is
	degeneralized already.
	* src/tgbatest/ltl2tgba.test: Add a test case.

2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Please GCC 4.6.

	* src/tgbatest/complementation.cc (check, automaton): Remove
	these unused variables.

2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a nondeterministic behavior of the degeneralization algorithm.

	Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.

	* src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used
	to record outgoing transitions by an Sgi::hash_map, and keep the
	order of these transitions in a separate list.
	* src/tgbatest/degendet.test: New file.
	* src/tgbatest/Makefile.am (TESTS): Add it.
	* THANKS: Add Tomáš and convert to utf8.

2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D.

2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2check.cc: Add option -W and simplify formulae.

2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	-e means we expect an accepting run.

	* iface/dve2/dve2check.cc: Reverse the value of
	expect_counter_example with respect to the -e/-E options.
	* iface/dve2/dve2check.test: Swap -e and -E.

2011-06-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add some "drop shadow" in ltl2tgba.html.

	* wrap/python/ajax/ltl2tgba.html: Add shadow to all boxes.
	* wrap/python/ajax/css/ltl2tgba.css (.shadow): New class.

2011-06-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Revamp the ltl2tgba benchmark.

	* bench/ltl2tgba/algorithms: Reduce the number of Spot configuration
	tested.
	* bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt):
	New rules.
	* bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known:
	Add a 15min timeout to the lbtt configuration.
	* bench/ltl2tgba/defs.in: Adjust variable definitions to accept
	variable inderections.
	* bench/ltl2tgba/parseout.pl: Add an option to output the table in
	LaTeX.  Also consider all formulae, not just the positive
	formulae.
	* bench/ltl2tgba/README: Update.

2011-06-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break.

2011-06-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/spot.in: Touch the directory containing
	the cached result for the requests.  So that it survives
	the browser's cache.
	(finish): Prune the cache only once per hour, and only eraes
	files that are older than 2 hours.

2011-06-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/ltl2tgba.html: Add focus on the formula field
	on page load.

2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent changes.

2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement cache pruning in the CGI script.

	* wrap/python/ajax/spot.in (finish): Prune the cache once in a
	while.  We rely on hardlinks for garbage collecting the pictures
	and dot sources that may be shared by different requests.

2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Cache dot sources in the CGI script.

	* wrap/python/ajax/spot.in (render_dot, render_dot_maybe)
	(render_automaton, render_formula): Cache the dot source, so that
	we do not have to regenerate two pictures from the same contents.
	* wrap/python/spot.i: Typo in the ostringstream declaration.

2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Output a "Cache-Control:" header in the CGI script.

	* wrap/python/ajax/spot.in: Output a cache-control header, so that
	browsers do no even send two identical requests.

2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Cache results of the spot.py CGI script.

	* wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to
	cache the result of the script.  Open stdout without buffering and
	redirect it to a file that we can dump later on cache hits.  Parts
	of this change are extracted from code from Pierre Parutto
	<parutto@lrde.epita.fr>.
	* AUTHORS: Add him.

2011-06-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltltest/genltl.cc (X_n): Fix assertion.

2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltlvisit/dotty.cc (dotty_visitor): Reorder attributes.

2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltltest/genltl.cc (fair_response): Typo.

2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Do not display state variables with only one possible value.

	* iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill
	a format_filter_ array with boolean indicating whether each
	variable should be printed.  Ignore variable with only one
	possible value.
	(dve2_kripke::~dve2_kripke): Destroy it.
	(dve2_kripke::format_state): Use it.
	* iface/dve2/finite.test: Adjust.

2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove Kristin Rozier's LTLcounter.pl scripts, now that we can
	generate these formulae with "genltl".

	* src/tgbatest/ltlcounter/: Remove this directory.
	* src/tgbatest/Makefile.am: Adjust.
	* src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl
	to generate the formulae.
	* bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/
	anymore.

2011-06-06  Alexandre Duret-Lutz  <adl@va-et-vient.net>

	Better layout of the LTL formula parse tree.

	* src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels
	for binary operators.  Gather all constants and atomic
	propositions in a sub-graph with "rank=sink".

2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add more formula families to genltl.

	* src/ltltest/genltl.cc (fair_response, ltl_counter)
	(ltl_counter_carry): New functions, constructing function from
	gastin.03.cav and rozier.07.cav.  The LTL counter will replace the
	scripts in src/tgbatest/ltlcounter/.
	(X_n): New helper function.

2011-06-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Install a misc/_config.h to hide all the defines that clutter the
	built output.

	This is also a step towards better checks for things like
	__attribute__ or std::tr1.

	* m4/ax_prefix_config_h.m4: New file.
	* configure.ac: Call AC_CONFIG_HEADERS and AX_PREFIX_CONFIG_H.
	* src/misc/Makefile.am: Install misc/_config.h.
	* src/misc/random.cc, src/misc/version.cc: Include misc/_config.h.

2011-06-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Document the protocol used between ltl2tgba.html and spot.py.

	* wrap/python/ajax/protocol.txt: New file.
	* wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it.

2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/README: Document state compression.

2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Update jQuery and jQuery-UI.

	* wrap/python/ajax/ltl2tgba.html: Adjust to use
	jQuery 1.6.1 and jQuery-UI 1.8.13.  Remove a useless check
	of $("#autoupdate").attr("checked") since this checkbox no longer
	exists.
	* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css:
	Replace by ...
	* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This.
	* wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust.

2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Kill a spurious warning.

2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* bench/wdba/README: Typos.

2011-05-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Some intvcomp2 speedups.

	* src/misc/intvcmp2.cc (stream_compression_base::run):
	Implement a shift-less encoding for the 1-bit and 3-bit cases.
	Also declare offsets as size_t, to help 64-bit compilers.

2011-05-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcomp.hh, src/misc/intvcmp2.hh: Include stddef.h for
	size_t.

2011-05-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcmp2.cc: Cosmetics to please sanity checks.

2011-05-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix compilation error with g++ <= 4.3.

	* src/misc/intvcmp2.cc (int_array_array_compression): Specify full
	type of stream_compression_base<int_array_array_compression> in
	constructor to please g++ versions <= 4.3.

2011-05-02  Alexandre Duret-Lutz  <adl@va-et-vient.net>

	DVE2: Minor memory compaction.

	* iface/dve2/dve2.cc (dve2_state, dve2_compressed_state): Store
	size and count on 16 bits, and hash on 32 bits, to limit memory
	wasted.

2011-05-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Optionally use the new compression.

	* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc:
	Add a -Z option and pass it through.

2011-05-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement a new compression inspired from simple-9.

	* src/misc/intvcmp2.cc, src/misc/intvcmp2.hh: New files.
	* src/misc/Makefile.am: Add them.
	* src/tgbatest/intvcmp2.cc: New test.
	* src/tgbatest/Makefile.am: Add it.
	* src/tgbatest/intvcomp.test: Call it.

2011-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcomp.cc: Low-level fine-tuning.

2011-04-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix compression of large repetitions

	* src/misc/intvcomp.cc (stream_compression_base::run): Limit
	repeatitions to 40, not 42.
	(stream_decompression_base::refill): Refill the end of the stream
	with 0.
	(stream_decompression_base::look_n_bits): Add assertion.
	* src/tgbatest/intvcomp.cc: Add a new test case.

2011-04-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	More interfaces to the int array compression routines.

	* src/misc/intvcomp.cc, src/misc/intvcomp.cc: Add interfaces to
	compress vector<int> to vector<unsigned>.
	* src/tgbatest/intvcomp.cc: Test them.
	* src/sanity/style.test: Refine check to avoid a spurious report.

2011-04-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Typo when handling dead==true.

2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Always pass --enable-devel or --disable-devel to BuDDy.

	* configure.ac: Do not add CXXFLAGS and CFLAGS in ac_configure_args,
	it causes problem when using config.cache.  Instead ...
	* m4/devel.m4: Add --enable-devel or --disable-devel on
	ac_configure_args, now that BuDDy understands that.

2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/escape.hh: Fix Doxygen documentation.
	* src/misc/intvcomp.hh: Likewise.

2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Move the compression routines into their own *.cc file.

	* src/misc/intvcomp.hh: Move all code...
	* src/misc/intvcomp.cc: ... in this new file.
	* src/misc/Makefile.am: Add invcomp.cc

2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Use mspool for compressed states.

	* iface/dve2/dve2.cc: Adjust to use the new mspool allocator,
	and get rid of the std::vector used to store compressed states.
	* src/misc/intvcomp.hh: Add an "int* -> int*" interface
	in addition to the "int* -> vector<unsigned>*" interface.
	* src/tgbatest/intvcomp.cc: Test the two interfaces.

2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add a multiple-size memory pool implementation.

	* src/misc/mspool.hh: New file.
	* src/misc/Makefile.am: Add it.

2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/fixpool.hh: Typo in comment.

2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: preliminary implementation of compressed states.

	* iface/dve2/dve2.cc (dve2_compressed_state): New class.
	(callback_context): Deal with general state*s, not dve2_state*s.
	(transition_callback_compress): New function.
	(dve2_kripke): Take a compress option.
	(get_init_state, compute_state_condition, succ_iter,
	format_state, state_condition): Handle compressed states.
	(get_vars, compute_state_condition_aux): New helper methods.
	* iface/dve2/dve2.hh (load_dve2): Add a compress option.
	* iface/dve2/dve2check.cc: Add a -z option.
	* iface/dve2/finite.test, iface/dve2/dve2check.test: Add more
	tests.

2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Preliminary implementation of an int array compressor.

	* src/misc/intvcomp.hh: New file.
	* src/misc/Makefile.am: Add it.
	* src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test: New files.
	* src/tgbatest/Makefile.am: Add them.

2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix two spurious segfaults in test cases for the Python interface.

	* wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py:
	Clean all used bdd variables before calling bdd_done(), so that
	bdd_delref() is never called after bdd_done().  In NDEBUG builds,
	bdd_delref() does not check whether the BuDDy is running or not,
	and calling it after bdd_done() will crash.

2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING: Add an example for using callgrind.

2011-04-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2check.cc (main): Catch out-of-memory errors
	during emptiness check or counterexample generation.

2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use
	a fixed-size memory pool for product_state instances.

2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state