* src/sanity/readme.test: For each AC_OUTPUT Makefile, check that
the directory is documented in README. Also skip non distributed
directories in readme.test.
* README: Fit on 80 columns.
kills a memory leak warning from swig/python.
* src/ltlparse/public.hh (parse_error_list): Declare
as an empty struct for Swig.
* wrap/python/tests/ltlparse.py: Fix copyright.
Let "make dvi" work on Ubuntu.
* doc/lbtt.texi (The formula generation algorithm): Use op^\prime
instead of op', because etex on Ubuntu hangs (an infinite loop?)
on the later when texi2dvi tries to compile a dvi.
Get rid of some "deprecated conversion from string constant to
`char*'" warnings.
* examples/bddcalc/parser_.h (yyerror): Declare the format
as a "const char*".
* examples/bddcalc/parser.yxx (yyerror): Likewise.
* src/ltlvisit/length.cc (visit(multop*)): New function. "a & b &
c" has length 5, not 4, even though it is stored as And(a,b,c).
This caused reduc.test to fail on some formulae.
Kill some warnings on Ubuntu.
* src/UserCommandReader.cc (UserCommandInterface): Explicitly
ignore the return code of system() to kill a warning.
* src/TestOperations.cc (generateBuchiAutomaton): Explicitly
ignore the return code of write() to kill a warning.
* src/ltltest/reduc.cc: Add an option -f to read a lost of
formulae from a file. Running a process for each formula was
too slow. Also add an option -h to hide reduced formulae.
* src/ltltest/reduc.test: Simplify accordingly.
* src/tgbatest/emptchk.test: Move the newly added test ...
* src/tgbatest/emptchke.test: ... here, with other explicit test.
Also test more algorithms.
* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::acss_states):
Delete the iterator after using it.
* src/tgbatest/emptchkr.test: Run 'randtgba -z' with valgrind too.
* src/tgbaalgos/gv04.cc (push): Fix the tracking of the accepting
link. This bug was discovered on a random generated graph with
a complex accepting cycle.
* src/tgbatest/emptchk.test: Add the troublesome graph as
test case.
* src/ltlast/automatop.cc, src/ltlast/automatop.hh: Rename nfa as
get_nfa to avoid a name clash with the `nfa' class.
* src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/tostring.cc, src/tgbaalgos/eltl2tgba_lacim.cc: Use
get_nfa instead of nfa.
* src/tgba/tgbasafracomplement.cc: Don't use a
const_reverse_iterator.
* src/tgbaalgos/randomgraph.cc (random_graph): Revert the part of
the patch from 2007-02-06 which silently replaced the use of state
index by state pointers. Storing states pointer in this map cause
some non-determinism because of the memory layout. It was almost
impossible to reproduce bugs found by tests based on randtgba.
speed up a little the translation.
* src/tgbaalgos/ltl2taa.cc: Adjust. Also fix a bug with
acceptance conditions in all_n_tuples.
* src/tgba/taatgba.cc, src/tgba/taatgba.hh: Adjust.
taa_tgba instances labelled by other objects than strings
in the same way Alexandre did for tgba_explicit.
* src/tgba/taatgba.cc, src/tgba/taatgba.hh: Split taa_tgba in two
levels: taa_tgba with no label and taa_tgba_labelled templated by
the type of the label. Define taa_tgba_string (with the interface
of the former taa_tgba class) and taa_tgba_formula for future use
in ltl2taa.cc.
* src/tgbaalgos/ltl2taa.cc, src/tgbatest/taatgba.cc: Adjust to use
taa_tgba_string.
* src/tgbatest/eltl2tgba.cc: Remove.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an
extended LTL instead of an LTL, a feature previously offered by
eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc.
* src/tgbatest/spotlbtt.test: Adjust.
Inline bdd_addref() and bdd_delref() to speedup BDD operations.
* src/kernel.c, src/kernel.h (bdd_addref, bdd_delref): Move these
functions and there associated global variables...
* src/bdd.c (bdd_error): ... and this function ...
* src/bdd.h (bdd_addref, bdd_delref, bdd_error): ...here so that
they can be inlined.
* src/saba/sabacomplementtgba.hh,
src/saba/sabacomplementtgba.cc: New. The algorithm.
* src/saba/Makefile.am: Adjust.
* src/sabatest/sabacomplementtgba.cc, src/sabatest/Makefile.am,
src/sabatest/defs.in: New. Test the algorithm.
* configure.ac, src/Makefile.am: Adjust to the new directory
`sabatest'.
Automata (SABA).
* src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh,
src/saba/sabasucciter.hh: New. Interface for
SABA (State-labeled Alternating Büchi Automata).
* src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh: New. Default
implementation for a conjunction of states.
* src/saba/Makefile.am: New.
* src/Makefile.am, configure.ac: Adjust.
* src/sabaalgos/sabareachiter.cc,
src/sabaalgos/sabareachiter.hh: New. Iterate over all reachable
states of a spot::saba.
* src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New.
Print reachable states in dot format.
* src/sabaalgos/Makefile.am: New.
Fix generation of random formulae on 64bits systems.
* src/main.cc (testLoop): Generate random short ints between 0 and
SHRT_MAX, not between 0 and LONG_MAX. On systems where long ints
are 64bits, LRAND(0,LONG_MAX) was returning a value with the lower
32 bits set to 0, and the latter truncation to short int always
yielded the value 0. Consequently all generated formulae were
identical...
* src/misc/timer.hh (time_info::running): New attribute.
(time_info::start, time_info::stop): Update and check
time_info::running.
* src/misc/timer.cc (timer_map::print): Mark running timers with
a "+" in the output.
* src/tgbatest/ltl2tgba.cc (main): Rename the name of the timers
for SCC and simulation reduction, and actually stop the SCC timer.
