* NEWS, configure.ac: Bump version number.

* src/tgbaalgos/simulation.cc: Remove unused typedef.

* src/Graph.h.in (PathElement::hasEdge): Check the correct
pointer, not the address of some member function.
* src/BuchiAutomaton.cc, src/Configuration.cc,
src/TestOperations.cc, src/TestOperations.h: Recode these files in
utf-8.

* wrap/python/spot.i: Export degeneralize().
* wrap/python/ajax/spot.in: Use it.

* examples/bddcalc/Makefile.am (ACLOCAL_AMFLAGS): Add -I. for
parse.c.  Reported by Pierre Parutto.

Thomas Badie authored Jun 19, 2012 and Alexandre Duret-Lutz committed Jun 20, 2012

* bench/ltl2tgba/lbtt2csv.pl: Write a perl script to change the
format outputted by `lbtt' into a csv format.
* bench/ltl2tgba/Makefile.am: Add the script to EXTRA_DIST.

* src/ltlparse/ltlparse.yy: Keep the left operand of binary operator,
if the right one is erroneous.  Also keep the sane beginning of
parenthesized blocks.
* src/ltltest/parseerr.test: Adjust test cases.
* NEWS: Mention it.

Thomas Badie authored Jun 19, 2012 and Alexandre Duret-Lutz committed Jun 19, 2012

* bench/ltl2tgba/parseout.pl: Fix a warning when using an option
by shifting the option when there is one.

* NEWS: Update.
* wrap/python/ajax/README: Explain the ltl3ba requirement.

* wrap/python/ajax/ltl2tgba.html: Adjust text.

* wrap/python/ajax/ltl2tgba.html: Update tooltips for LTL3BA.

* wrap/python/ajax/ltl2tgba.html: Here.

* wrap/python/ajax/css/loading.gif: New file.
* wrap/python/ajax/css/ltl2tgba.css (.loading): New class.
* wrap/python/ajax/ltl2tgba.html: Display loading.gif after 200ms if
the answer hasn't arrived
* wrap/python/ajax/spot.in: Do not suggest not to draw the automaton
on timeout.
* wrap/python/ajax/js/jquery.ba-dotimeout.min.js: New file.
* wrap/python/ajax/Makefile.am: Distribute it.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add options 'o' and 'p'.
* wrap/python/ajax/spot.in: Handle these, and use '-v' to check
version.

* wrap/python/ajax/ltl2tgba.html: Display the ltl3ba version, and
disable its tab when unavailable.
* wrap/python/ajax/protocol.txt: Add option for ltl3ba's version.
* wrap/python/ajax/spot.in: Implement this option, and catch
errors when ltl3ba is not installed.

* src/tgbaalgos/sccfilter.cc: tgba_explicit_numbered replace
tgba_explicit_string for the general case.  This way we don't have to
prefix the result of format_state() in case to states have the same
description.  We just number the states instead.  For the specific
cases where the input automata are instance of tgba_explicit_string or
tgba_explicit_formula, we clone the label.

* wrap/python/ajax/ltl2tgba.html: Add a dedicated tab with
two columns of options.
* wrap/python/ajax/css/ltl2tgba.css: Support for two columns.
* wrap/python/ajax/protocol.txt: Document new options.
* wrap/python/ajax/spot.in: Handle the new options.
* wrap/python/ajax/Makefile.am: Substitude LTL3BA in spot.in.

* src/tgba/tgbaexplicit.hh (state_is_accepting): Implement without
creating then deleting an iterator.

* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New files, with
most of the logic extracted from src/tgba/tgbatba.cc (SBA version).
* src/tgbaalgos/Makefile.am: Distribute these.
* src/tgbatest/ltl2tgba.cc: Use the new degeneralization instead of
the on-the-fly version.

* src/ltlvisit/simplify.cc, src/tgba/tgbaproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc: Here.

* wrap/python/buddy.i (bdd_implies): New function.
* wrap/python/tests/implies.py: New file.
* wrap/python/tests/Makefile.am: Add it.

* src/bdd.h (bdd_implies): New function.
* src/bddop.c (bdd_implies): Implement it.
(CACHEID_IMPLIES, IMPLIES_HASH): New helper macros.

The unicity table was mixed with the bddNode table for now
apparent reason.  After the hash of some node is computed,
bddnodes[hash] did only contain some random node (not the one
looked for) whose .hash member would point to the actual node with
this hash.  So that's a two step lookup.  With this patch, we sill
have a two step lookup, but the .hash member have been moved to a
separate array.  A consequence is that bddNode is now 16-byte long
(instead of 20) so it will never span across two cache lines.

* src/kernel.h (bddNode): Remove the hash member, and move it...
(bddhash): ... as this new separate table.
* src/kernel.c, src/reorder.c: Adjust all code.

* wrap/python/tests/Makefile.am (TEST_ENVIRONMENT): Rename as...
(LOG_COMPILER): ... this.

* src/Config-parse.yy, src/Ltl-parse.yy, src/NeverClaim-parse.yy:
Rename these as..
* src/Config-parse.y, src/Ltl-parse.y, src/NeverClaim-parse.y:
... these.
* src/Config-parse_.cc, src/Ltl-parse_.cc,
src/NeverClaim-parse_.cc: New files to hack around
incompatibilities between Automake 1.12 and Automake 1.11.
* src/Makefile.am: Adjust.
* NEWS: Mention this change.

* examples/bddcalc/parser.yxx: Rename as ...
* examples/bddcalc/parser.y: ... this.
* examples/bddcalc/parser_.cxx: New file that includes parser.c.
* examples/bddcalc/Makefile.am: Adjust.
* examples/bddcalc/parser.hxx: Delete this unused file.