* 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.
* 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).
* 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.
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.
