2010-01-24 Alexandre Duret-Lutz * src/sanity/Makefile.am (EXTRA_DIST): Distribute readme.test. 2010-01-24 Alexandre Duret-Lutz * README: Add descriptions for subdirectories of bench/, src/sanity, and src/kripke. 2010-01-24 Guillaume Sadegh * src/sanity/readme.test: A script to check whether all the directories referenced in README exist. * src/sanity/Makefile.am: Adjust to call `readme.test' when make check is invoked. 2010-01-24 Guillaume Sadegh Update the README. * README: Reference src/saba/, src/sabaalgos/, src/sabatest/, iface/nips/, iface/nips/nipstest/ and iface/nips/nips_vm/. 2010-01-22 Alexandre Duret-Lutz Turn parse_error_list into an opaque type for Swig. This 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. 2010-01-22 Alexandre Duret-Lutz Fix the computation of the length of multops. * 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. 2010-01-21 Alexandre Duret-Lutz Please the style checks... * src/tgbaalgos/randomgraph.cc: Fix the copyright and make it fit on 80 columns. 2010-01-21 Alexandre Duret-Lutz * src/ltltest/reduc.cc (main): Fix harmless memory leak introduced today. 2010-01-21 Alexandre Duret-Lutz Fix taa_tgba_formula's destructor. * src/tgba/taatgba.cc (taa_tgba_formula::~taa_tgba_formula): Really destroy all formulae, not only half of them. 2010-01-21 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Do not include twice. 2010-01-21 Alexandre Duret-Lutz Speedup reduc.test by not spawning one process per formula. * 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. 2010-01-21 Alexandre Duret-Lutz Move the last test from emptchk.test to emptchke.test. * src/tgbatest/emptchk.test: Move the newly added test ... * src/tgbatest/emptchke.test: ... here, with other explicit test. Also test more algorithms. 2010-01-21 Alexandre Duret-Lutz Fix a memory leak in Cou99 statistics. * 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. 2010-01-21 Alexandre Duret-Lutz Fix a longstanding bug in our implementation of GV04. * 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. 2010-01-20 Damien Lefortier When iterating a hash_map, be careful not to delete i->first before doing ++i to avoid memory issues. * src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Fix them. 2010-01-20 Damien Lefortier Minor fixes to compile with GCC 3.3 * 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. 2010-01-20 Alexandre Duret-Lutz Remove some non-determinism in random_graph() * 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. 2010-01-19 Damien Lefortier * src/tgbaalgos/ltl2taa.cc: Fix the previous patch. 2010-01-18 Damien Lefortier * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues occuring when labels are pointers. * src/tgbaalgos/ltl2taa.cc: Fix a bug. * src/tgbatest/ltl2tgba.cc: Fix a bug. 2010-01-16 Guillaume Sadegh * src/saba/sabacomplementtgba.cc: Fix a bug. 2010-01-16 Damien Lefortier Use taa_tgba_formula instead of taa_tgba_string in ltl_to_taa to 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. 2010-01-16 Damien Lefortier Introduce taa_tgba_labelled