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().
* 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.
* configure.ac: Add a --disable-python option tied to
a USE_PYTHON conditional.
* README: Document the option.
* wrap/Makefile.am: Use the conditional.
* 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.
* 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.
* 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().
* 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.
* 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.
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.
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.
* 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.
* src/misc/bddalloc.cc (bdd_allocator::initialize): Call
bdd_setmaxincrease(500000), because the default is 50000,
which cause garbage collection to occur too often.
* 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.
* 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.
* 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.
* src/tgbaalgos/randomgraph.hh: Document the fact that adding
acceptance conditions to the graph may generate graphs that do not
have any accepting cycle.
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.
* 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.
* 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.
* 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.
