From 915115d9e269dfa4634e1976490a0d5fae2ac730 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 12 Mar 2012 16:41:32 +0100 Subject: [PATCH] Rename ChangeLog as ChangeLog.1 and leave an empty ChangeLog. The empty ChangeLog is required so that Automake does not complain. * ChangeLog: Rename as ... * ChangeLog.1: ... this. * Makefile.am (EXTRA_DIST): Distribute it. * ChangeLog: New empty file. --- ChangeLog | 10800 -------------------------------------------------- ChangeLog.1 | 10800 ++++++++++++++++++++++++++++++++++++++++++++++++++ Makefile.am | 8 +- 3 files changed, 10805 insertions(+), 10803 deletions(-) create mode 100644 ChangeLog.1 diff --git a/ChangeLog b/ChangeLog index 178c4050e..e69de29bb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,10800 +0,0 @@ -2012-03-09 Alexandre Duret-Lutz - - * configure.ac, NEWS: Bump version to 0.8.3a. - -2012-03-09 Alexandre Duret-Lutz - - Release Spot 0.8.3. - - * configure.ac, NEWS: Bump version to 0.8.3. - -2012-03-09 Alexandre Duret-Lutz - - Fix a segfault in the CGI script, reported by Denis. - - * src/tgbaalgos/emptiness.cc - (emptiness_check_instantiator::construct): Set *err = 0 - on success. This avoids problem with the python bindings - always converting *err to a string and sometimes failing - to do so when err was not initialized. - -2012-03-08 Alexandre Duret-Lutz - - ltl2tgba.html: Fix initialization of unset options on reload. - - * wrap/python/ajax/ltl2tgba.html: On page reload, do not ignore - fields for which no value has been set in the hash fragment. - Otherwise they will keep their default value. - Reported by Thomas Badie. - -2012-03-08 Alexandre Duret-Lutz - - * wrap/python/ajax/spot.in: Fix emulation of execfile. - -2012-03-04 Alexandre Duret-Lutz - - ltl2tgba.html: save state in URL to preserve history - - * wrap/python/ajax/js/jquery.ba-bbq.min.js: New file. - * wrap/python/ajax/Makefile.am: Distribute it. - * wrap/python/ajax/ltl2tgba.html: Include it, and - Adjust the code to update the URL's hash fragment, - and to read it. - -2012-03-04 Alexandre Duret-Lutz - - python: fix return value of emptiness_check_instantiator - - * wrap/python/spot.i: Fix typemap for - emptiness_check_instantiator::construct. The previous code used - to turn (None, "error") into simply ("error"). - * wrap/python/ajax/spot.in: Fix handling or errors when - instantiating emptiness checks. - -2012-02-25 Alexandre Duret-Lutz - - * NEWS: Summarize recent changes. - -2012-02-25 Alexandre Duret-Lutz - - Make all python code compatible with Python 2.x and Python 3.x. - - * 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. - -2012-02-24 Alexandre Duret-Lutz - - Fix computation of PYTHONINC for Python 3. - - * m4/pypath.m4: The print syntax changed in Python 3, so use - sys.stdout.write for compatibility with all versions. - -2012-02-04 Alexandre Duret-Lutz - - * HACKING: Minor updates and corrections. - -2012-02-15 Alexandre Duret-Lutz - - Fix a race condition on the CGI script. - - * 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). - -2012-01-24 Alexandre Duret-Lutz - - Fix a segfault reported by Etienne Renault using dve2check. - - * 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. - -2012-01-20 Alexandre Duret-Lutz - - * NEWS: Add missing dates. - -2012-01-19 Alexandre Duret-Lutz - - * configure.ac, NEWS: Bump version to 0.8.2a. - -2012-01-19 Alexandre Duret-Lutz - - Release Spot 0.8.2. - - * configure.ac, NEWS: Bump version to 0.8.2. - -2012-01-18 Alexandre Duret-Lutz - - Small speedup in safra_tree::compare(). - - * src/tgba/tgbasafracomplement.cc (safra_tree::compare): Improve - the order of the tests. - -2012-01-18 Alexandre Duret-Lutz - - * NEWS: Mention the last two changes. - -2012-01-18 Alexandre Duret-Lutz - - Implement a unicity table for states created by tgba_tba_proxy. - - 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(). - -2012-01-17 Alexandre Duret-Lutz - - Minor speedups in tgba_safra_complement(). - - * 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. - -2012-01-18 Alexandre Duret-Lutz - - * src/eltlparse/eltlparse.yy (realias): Add a useless return to - fix a g++ warning. - -2012-01-18 Alexandre Duret-Lutz - - * bench/ltlclasses/run: Typo in comment. - -2012-01-17 Alexandre Duret-Lutz - - Make it possible not to build Python bindings. - - * configure.ac: Add a --disable-python option tied to - a USE_PYTHON conditional. - * README: Document the option. - * wrap/Makefile.am: Use the conditional. - -2012-01-17 Alexandre Duret-Lutz - - Fix position of the Send button with WebKit. - - * 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. - -2012-01-17 Alexandre Duret-Lutz - - * wrap/python/ajax/spot.py: Add a required "None" second - argument to utime(). - -2012-01-17 Alexandre Duret-Lutz - - minimize_wdba() failed to fully minimize some automata. - - * 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. - -2012-01-13 Alexandre Duret-Lutz - - * NEWS: Update with recent fixes. - -2012-01-13 Alexandre Duret-Lutz - - Fix a 'make check' failure when valgrind is not installed. - - * 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(). - -2012-01-12 Alexandre Duret-Lutz - - Do use of tr1::unordered_map with G++ 4.0.0. - - * m4/stl.m4 (AC_HEADER_TR1_UNORDERED_MAP): Add some code so - we don't pick a broken tr1::unordered_map. - -2012-01-06 Alexandre Duret-Lutz - - * lrde-upload.sh: Retrieve the package version from configure.ac. - -2012-01-05 Ala-Eddine Ben-Salem - - Fix detection of the last iteration of minimize_dfa(). - - * 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. - -2012-01-05 Alexandre Duret-Lutz - - Fix computation of length of LTL formulas. - - * 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. - -2011-12-18 Alexandre Duret-Lutz - - * configure.ac, NEWS: Bump version to 0.8.1a. - -2011-12-18 Alexandre Duret-Lutz - - Release Spot 0.8.1. - - * configure.ac, NEWS: Bump version to 0.8.1. - -2011-12-18 Alexandre Duret-Lutz - - * NEWS: Summarize recent fixes. - -2011-12-18 Alexandre Duret-Lutz - - Fix VPATH builds, now that hash.hh include _config.h - - * iface/dve2/Makefile.am, src/eltlparse/Makefile.am - src/eltltest/Makefile.am, src/evtgba/Makefile.am, - src/evtgbaalgos/Makefile.am, src/evtgbaparse/Makefile.am, - src/evtgbatest/Makefile.am, src/kripke/Makefile.am, - src/kripketest/Makefile.am, src/ltlast/Makefile.am, - src/ltlparse/Makefile.am, src/ltltest/Makefile.am, - src/ltlvisit/Makefile.am, src/misc/Makefile.am, - src/neverparse/Makefile.am, src/saba/Makefile.am, - src/sabaalgos/Makefile.am, src/sabatest/Makefile.am, - src/sanity/Makefile.am, src/tgba/Makefile.am, - src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am, - src/tgbaparse/Makefile.am, src/tgbatest/Makefile.am, - wrap/python/Makefile.am (AM_CPPFLAGS): Make sure - $(top_builddir)/src is included. - -2011-12-16 Alexandre Duret-Lutz - - Perform WDBA minimization before degeneralization. - - 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. - -2011-12-16 Alexandre Duret-Lutz - - Don't rely on the g++ version to include tr1/unordered_map and co. - - 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. - -2011-12-01 Alexandre Duret-Lutz - - Fix mkdir error in ajax/spot.in. - - * wrap/python/ajax/spot.in: Do not print an error - when attempting to create an existing directory. - Reported by Étienne Renault. - -2011-11-29 Alexandre Duret-Lutz - - Fix build failure during "make check" on MacOS X. - - * 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. - -2011-11-28 Alexandre Duret-Lutz - - * AUTHORS: Sort alphabetically. - -2011-11-28 Alexandre Duret-Lutz - - Remove the old CGI interface. - - * wrap/python/cgi-bin: Remove this directory. - * wrap/python/Makefile.am (SUBDIRS): Remove it. - * configure.ac, README, wrap/python/ajax/README: Likewise. - -2011-11-28 Alexandre Duret-Lutz - - Undocument `.' from the web interface. - - * wrap/python/ajax/ltl2tgba.html: Remove `.' - from the list of acceptable symbols for AND. - -2011-11-28 Alexandre Duret-Lutz - - * NEWS, configure.ac: Bump version to 0.8a. - -2011-11-28 Alexandre Duret-Lutz - - Release Spot 0.8. - - * NEWS, configure.ac: Bump version to 0.8. - -2011-11-28 Alexandre Duret-Lutz - - Remove spotref.pdf. - - * doc/Doxyfile.in: Do not generate LaTeX output. - * doc/Makefile.am: Do not build spotref.pdf. - * NEWS, README: Adjust. - -2011-11-28 Alexandre Duret-Lutz - - Fix some Doxygen errors. - - * src/kripke/kripkeexplicit.hh: Reindent, and fix - some comments. - -2011-11-13 Alexandre Duret-Lutz - - Add more nodes when resizing BDD table. - - * src/misc/bddalloc.cc (bdd_allocator::initialize): Call - bdd_setmaxincrease(500000), because the default is 50000, - which cause garbage collection to occur too often. - -2011-11-28 Alexandre Duret-Lutz - - * NEWS: Mention the Kripke I/O. - -2011-11-27 Alexandre Duret-Lutz - - Don't flush the stream on each new line, when writing automata. - - * 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. - -2011-11-27 Alexandre Duret-Lutz - - Add an ltl2tgba option to read Kripke structure. - - Also offers two ways to output Kripke structures. - - * src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc - : Simplify includes. - * src/kripke/kripkeprint.hh (kripke_save_reachable, - kripke_save_reachable_renumbered): New declarations. - (KripkePrinter): Move and rename... - * src/kripke/kripkeprint.cc (kripke_printer): ... here. - (kripke_printer_renumbered): New class. - (kripke_save_reachable, kripke_save_reachable_renumbered): New - function. - * src/tgbatest/ltl2tgba.cc: Add an option to read Kripke - structures. - * iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered. - * iface/dve2/defs.in (run2): Remove. - * iface/dve2/kripke.test: Adjust tests. - -2011-11-27 Alexandre Duret-Lutz - - * AUTHORS: Add Thomas Badie. - -2011-05-07 Thomas Badie - - Add text I/O for Kripke structures. - - * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh, - src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files. - * src/kripke/Makefile.am: Add them. - * src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy, - src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh, - src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New - files. - * src/kripkeparse/Makefile.am: Add them. - * src/kripketest/bad_parsing.test, src/kripketest/defs.in, - src/kripketest/kripke.test, src/kripketest/origin, - src/kripketest/parse_print_test.cc: New files. - * src/kripketest/Makefile.am: Add them. - * src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest. - * README: Document src/kripketest/ and src/kripkeparse/. - * configure.ac: Generate src/kripkeparse/Makefile, - src/kripketest/Makefile, src/kripketest/defs. - * iface/dve2/defs.in (run2): New function. - * iface/dve2/dve2check.cc (syntax, main): Add option -gK. - * iface/dve2/kripke.test: New file. - * iface/dve2/Makefile.am (TESTS): Add kripke.test. - -2011-11-24 Alexandre Duret-Lutz - - Fix bench/emptchk/pml2tgba.pl for more recent Spin version. - - * 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. - -2011-11-24 Alexandre Duret-Lutz - - Update formulae.ltl not to use uncommon operators. - - * 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. - -2011-11-23 Alexandre Duret-Lutz - - More documentation. - - * src/tgbaalgos/randomgraph.hh: Document the fact that adding - acceptance conditions to the graph may generate graphs that do not - have any accepting cycle. - -2011-11-17 Alexandre Duret-Lutz - - Display transition annotations in dotty output. - - * src/tgbaalgos/dotty.cc (process_link): Call - transition_annotation(). Reported by Nikos Gorogiannis. - * src/tgba/tgba.hh (transition_annotation): More documentation. - * NEWS: Mention this change. - -2011-11-17 Alexandre Duret-Lutz - - * NEWS: Add an entry for the previous fix. - -2011-11-16 Alexandre Duret-Lutz - - Fully quote guards used by neverclaims. - - 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. - -2011-11-11 Alexandre Duret-Lutz - - Fix a g++-4.7 warning about a variable used only in an assert(). - - * 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. - -2011-11-08 Alexandre Duret-Lutz - - Allow neverclaim guards of the form `!(x)' or `! (x)'. - - * 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. - -2011-10-26 Alexandre Duret-Lutz - - Better documentation for print_tgba_run. - - * src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the - documentation after a report from Nikos Gorogiannis. - -2011-10-24 Alexandre Duret-Lutz - - * iface/dve2/finite.test: Swap -e and -E after change from 2011-07-26. - -2011-10-24 Alexandre Duret-Lutz - - * NEWS: Update with recent fixes. - -2011-10-23 Alexandre Duret-Lutz - - Safra: Fix usage of multiple acceptance conditions and fix text output. - - * 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. - -2011-10-23 Alexandre Duret-Lutz - - * src/tgba/tgbasafracomplement.cc: Fix two asserts. - -2011-10-23 Alexandre Duret-Lutz - - Improve the print_safra_automaton output. - - * src/tgba/tgbasafracomplement.cc (print_safra_tree): Fix output in - case of hash collision. Use the actual states to get a number, not - their hash value. - (print_safra_automaton): Output a mapping of values to states names. - (safra_tree_automaton::get_sba): New method, used by - print_safra_automaton. - -2011-08-28 Alexandre Duret-Lutz - - Fix errors reported by clang++-2.9. - - * src/evtgbaalgos/tgba2evtgba.cc (process_link): Fix prototype - to match tgba_reachable_iterator::process_link. - * src/ltlvisit/tunabbrev.hh: Add using super::visit, so that the - other visit() method are in scope when we overload one. - * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc (start, end, - process_link): Remove these empty methods. The default - implementations are empty too, and process_link had the - wrong prototype. - * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc - (start, end, process_link): Likewise. - -2011-08-27 Alexandre Duret-Lutz - - Improve SCC simplification by removing implied acceptance conditions. - - Spot 0.7.1 used to need 190 acceptance conditions to translate the - 188 literature formulae. With this patch we are down to 185. - That's not an impressive, but there are only ~20 formulae that - require more than 1 acceptance conditions; hence little room for - improvement. - - * src/misc/bddlt.hh (bdd_hash): New function. - * src/misc/accconv.hh, src/misc/accconv.cc: New files. - * src/misc/Makefile.am: Add them. - * src/tgbaalgos/scc.cc (scc_map::build_map): Adjust - to record all combination of acceptance conditions occurring in a SCC. - * src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description. - * src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance - conditions that are always implied by another acceptance - conditions. Previously, we only removed acceptance conditions - that where always present in accepting SCCs. - * src/tgbatest/sccsimpl.test: New file. - * src/tgbatest/Makefile.am (TESTS): Add it. - -2011-08-26 Alexandre Duret-Lutz - - Refine yesterday's change to the degeneralization. - - This avoids a small regression on the size of degeneralized - automata of our usual list of literature formulae. - - * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc - (tgba_tba_proxy::union_acceptance_conditions_of_original_state): - New method. - * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting - states, ignore only the last expected acceptance condition if its - common to all outgoing transitions AND if it is not used by any - outgoing transitions of the destination. - -2011-08-25 Alexandre Duret-Lutz - - Make sure the degeneralization is idempotent (up to renaming of - states). - - * src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the - acceptance conditions that are common to all outgoing transitions - of this state. This helps to make the degeneralization - idempotent. - * src/tgbatest/degenid.test: New test case. - * src/tgbatest/Makefile.am: Add it. - -2011-08-25 Alexandre Duret-Lutz - - Fix escaping of state name in save_reachable()'s output. - - * src/tgbaalgos/save.c (process_state): Escape quotes in the - name of source and destination states. This fixes a side bug - in the upcoming degenid.test test case. - -2011-08-25 Alexandre Duret-Lutz - - Running `ltl2tgba -R1q -R1t -N` would degeneralize before and - after the simulation-reduction. - - Report from Tomáš Babiak . - - * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take - a tgba as input. - * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call - state_is_accepting() only if this tgba turns out to be - a tgba_sba_proxy. Otherwise check the acceptance of one - outgoing transition as we do in dotty_bfs since 2011-03-05. - * src/tgbatest/ltl2tgba.cc: Do not redegeneralize before - calling never_claim_reachable() if we know the automaton is - degeneralized already. - * src/tgbatest/ltl2tgba.test: Add a test case. - -2011-08-17 Alexandre Duret-Lutz - - Please GCC 4.6. - - * src/tgbatest/complementation.cc (check, automaton): Remove - these unused variables. - -2011-08-17 Alexandre Duret-Lutz - - Fix a nondeterministic behavior of the degeneralization algorithm. - - Reported by Tomáš Babiak . - - * src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used - to record outgoing transitions by an Sgi::hash_map, and keep the - order of these transitions in a separate list. - * src/tgbatest/degendet.test: New file. - * src/tgbatest/Makefile.am (TESTS): Add it. - * THANKS: Add Tomáš and convert to utf8. - -2011-08-17 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. - -2011-07-26 Alexandre Duret-Lutz - - * iface/dve2/dve2check.cc: Add option -W and simplify formulae. - -2011-07-26 Alexandre Duret-Lutz - - -e means we expect an accepting run. - - * iface/dve2/dve2check.cc: Reverse the value of - expect_counter_example with respect to the -e/-E options. - * iface/dve2/dve2check.test: Swap -e and -E. - -2011-06-26 Alexandre Duret-Lutz - - Add some "drop shadow" in ltl2tgba.html. - - * wrap/python/ajax/ltl2tgba.html: Add shadow to all boxes. - * wrap/python/ajax/css/ltl2tgba.css (.shadow): New class. - -2011-06-25 Alexandre Duret-Lutz - - Revamp the ltl2tgba benchmark. - - * bench/ltl2tgba/algorithms: Reduce the number of Spot configuration - tested. - * bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt): - New rules. - * bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known: - Add a 15min timeout to the lbtt configuration. - * bench/ltl2tgba/defs.in: Adjust variable definitions to accept - variable inderections. - * bench/ltl2tgba/parseout.pl: Add an option to output the table in - LaTeX. Also consider all formulae, not just the positive - formulae. - * bench/ltl2tgba/README: Update. - -2011-06-16 Alexandre Duret-Lutz - - * src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break. - -2011-06-10 Alexandre Duret-Lutz - - * wrap/python/ajax/spot.in: Touch the directory containing - the cached result for the requests. So that it survives - the browser's cache. - (finish): Prune the cache only once per hour, and only eraes - files that are older than 2 hours. - -2011-06-09 Alexandre Duret-Lutz - - * wrap/python/ajax/ltl2tgba.html: Add focus on the formula field - on page load. - -2011-06-08 Alexandre Duret-Lutz - - * NEWS: Update with recent changes. - -2011-06-08 Alexandre Duret-Lutz - - Implement cache pruning in the CGI script. - - * wrap/python/ajax/spot.in (finish): Prune the cache once in a - while. We rely on hardlinks for garbage collecting the pictures - and dot sources that may be shared by different requests. - -2011-06-08 Alexandre Duret-Lutz - - Cache dot sources in the CGI script. - - * wrap/python/ajax/spot.in (render_dot, render_dot_maybe) - (render_automaton, render_formula): Cache the dot source, so that - we do not have to regenerate two pictures from the same contents. - * wrap/python/spot.i: Typo in the ostringstream declaration. - -2011-06-08 Alexandre Duret-Lutz - - Output a "Cache-Control:" header in the CGI script. - - * wrap/python/ajax/spot.in: Output a cache-control header, so that - browsers do no even send two identical requests. - -2011-06-08 Alexandre Duret-Lutz - - Cache results of the spot.py CGI script. - - * wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to - cache the result of the script. Open stdout without buffering and - redirect it to a file that we can dump later on cache hits. Parts - of this change are extracted from code from Pierre Parutto - . - * AUTHORS: Add him. - -2011-06-07 Alexandre Duret-Lutz - - * src/ltltest/genltl.cc (X_n): Fix assertion. - -2011-06-06 Alexandre Duret-Lutz - - * src/ltlvisit/dotty.cc (dotty_visitor): Reorder attributes. - -2011-06-06 Alexandre Duret-Lutz - - * src/ltltest/genltl.cc (fair_response): Typo. - -2011-06-06 Alexandre Duret-Lutz - - DVE2: Do not display state variables with only one possible value. - - * iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill - a format_filter_ array with boolean indicating whether each - variable should be printed. Ignore variable with only one - possible value. - (dve2_kripke::~dve2_kripke): Destroy it. - (dve2_kripke::format_state): Use it. - * iface/dve2/finite.test: Adjust. - -2011-06-06 Alexandre Duret-Lutz - - Remove Kristin Rozier's LTLcounter.pl scripts, now that we can - generate these formulae with "genltl". - - * src/tgbatest/ltlcounter/: Remove this directory. - * src/tgbatest/Makefile.am: Adjust. - * src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl - to generate the formulae. - * bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/ - anymore. - -2011-06-06 Alexandre Duret-Lutz - - Better layout of the LTL formula parse tree. - - * src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels - for binary operators. Gather all constants and atomic - propositions in a sub-graph with "rank=sink". - -2011-06-06 Alexandre Duret-Lutz - - Add more formula families to genltl. - - * src/ltltest/genltl.cc (fair_response, ltl_counter) - (ltl_counter_carry): New functions, constructing function from - gastin.03.cav and rozier.07.cav. The LTL counter will replace the - scripts in src/tgbatest/ltlcounter/. - (X_n): New helper function. - -2011-06-03 Alexandre Duret-Lutz - - Install a misc/_config.h to hide all the defines that clutter the - built output. - - This is also a step towards better checks for things like - __attribute__ or std::tr1. - - * m4/ax_prefix_config_h.m4: New file. - * configure.ac: Call AC_CONFIG_HEADERS and AX_PREFIX_CONFIG_H. - * src/misc/Makefile.am: Install misc/_config.h. - * src/misc/random.cc, src/misc/version.cc: Include misc/_config.h. - -2011-06-03 Alexandre Duret-Lutz - - Document the protocol used between ltl2tgba.html and spot.py. - - * wrap/python/ajax/protocol.txt: New file. - * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it. - -2011-06-02 Alexandre Duret-Lutz - - * iface/dve2/README: Document state compression. - -2011-06-02 Alexandre Duret-Lutz - - Update jQuery and jQuery-UI. - - * wrap/python/ajax/ltl2tgba.html: Adjust to use - jQuery 1.6.1 and jQuery-UI 1.8.13. Remove a useless check - of $("#autoupdate").attr("checked") since this checkbox no longer - exists. - * wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css: - Replace by ... - * wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This. - * wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust. - -2011-05-30 Alexandre Duret-Lutz - - * iface/dve2/dve2.cc: Kill a spurious warning. - -2011-05-30 Alexandre Duret-Lutz - - * bench/wdba/README: Typos. - -2011-05-18 Alexandre Duret-Lutz - - Some intvcomp2 speedups. - - * src/misc/intvcmp2.cc (stream_compression_base::run): - Implement a shift-less encoding for the 1-bit and 3-bit cases. - Also declare offsets as size_t, to help 64-bit compilers. - -2011-05-16 Alexandre Duret-Lutz - - * src/misc/intvcomp.hh, src/misc/intvcmp2.hh: Include stddef.h for - size_t. - -2011-05-05 Alexandre Duret-Lutz - - * src/misc/intvcmp2.cc: Cosmetics to please sanity checks. - -2011-05-05 Alexandre Duret-Lutz - - Fix compilation error with g++ <= 4.3. - - * src/misc/intvcmp2.cc (int_array_array_compression): Specify full - type of stream_compression_base in - constructor to please g++ versions <= 4.3. - -2011-05-02 Alexandre Duret-Lutz - - DVE2: Minor memory compaction. - - * iface/dve2/dve2.cc (dve2_state, dve2_compressed_state): Store - size and count on 16 bits, and hash on 32 bits, to limit memory - wasted. - -2011-05-01 Alexandre Duret-Lutz - - DVE2: Optionally use the new compression. - - * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc: - Add a -Z option and pass it through. - -2011-05-01 Alexandre Duret-Lutz - - Implement a new compression inspired from simple-9. - - * src/misc/intvcmp2.cc, src/misc/intvcmp2.hh: New files. - * src/misc/Makefile.am: Add them. - * src/tgbatest/intvcmp2.cc: New test. - * src/tgbatest/Makefile.am: Add it. - * src/tgbatest/intvcomp.test: Call it. - -2011-04-15 Alexandre Duret-Lutz - - * src/misc/intvcomp.cc: Low-level fine-tuning. - -2011-04-13 Alexandre Duret-Lutz - - Fix compression of large repetitions - - * src/misc/intvcomp.cc (stream_compression_base::run): Limit - repeatitions to 40, not 42. - (stream_decompression_base::refill): Refill the end of the stream - with 0. - (stream_decompression_base::look_n_bits): Add assertion. - * src/tgbatest/intvcomp.cc: Add a new test case. - -2011-04-12 Alexandre Duret-Lutz - - More interfaces to the int array compression routines. - - * src/misc/intvcomp.cc, src/misc/intvcomp.cc: Add interfaces to - compress vector to vector. - * src/tgbatest/intvcomp.cc: Test them. - * src/sanity/style.test: Refine check to avoid a spurious report. - -2011-04-11 Alexandre Duret-Lutz - - * iface/dve2/dve2.cc: Typo when handling dead==true. - -2011-04-10 Alexandre Duret-Lutz - - Always pass --enable-devel or --disable-devel to BuDDy. - - * configure.ac: Do not add CXXFLAGS and CFLAGS in ac_configure_args, - it causes problem when using config.cache. Instead ... - * m4/devel.m4: Add --enable-devel or --disable-devel on - ac_configure_args, now that BuDDy understands that. - -2011-04-10 Alexandre Duret-Lutz - - * src/misc/escape.hh: Fix Doxygen documentation. - * src/misc/intvcomp.hh: Likewise. - -2011-04-09 Alexandre Duret-Lutz - - Move the compression routines into their own *.cc file. - - * src/misc/intvcomp.hh: Move all code... - * src/misc/intvcomp.cc: ... in this new file. - * src/misc/Makefile.am: Add invcomp.cc - -2011-04-09 Alexandre Duret-Lutz - - DVE2: Use mspool for compressed states. - - * iface/dve2/dve2.cc: Adjust to use the new mspool allocator, - and get rid of the std::vector used to store compressed states. - * src/misc/intvcomp.hh: Add an "int* -> int*" interface - in addition to the "int* -> vector*" interface. - * src/tgbatest/intvcomp.cc: Test the two interfaces. - -2011-04-09 Alexandre Duret-Lutz - - Add a multiple-size memory pool implementation. - - * src/misc/mspool.hh: New file. - * src/misc/Makefile.am: Add it. - -2011-04-08 Alexandre Duret-Lutz - - * src/misc/fixpool.hh: Typo in comment. - -2011-04-08 Alexandre Duret-Lutz - - DVE2: preliminary implementation of compressed states. - - * iface/dve2/dve2.cc (dve2_compressed_state): New class. - (callback_context): Deal with general state*s, not dve2_state*s. - (transition_callback_compress): New function. - (dve2_kripke): Take a compress option. - (get_init_state, compute_state_condition, succ_iter, - format_state, state_condition): Handle compressed states. - (get_vars, compute_state_condition_aux): New helper methods. - * iface/dve2/dve2.hh (load_dve2): Add a compress option. - * iface/dve2/dve2check.cc: Add a -z option. - * iface/dve2/finite.test, iface/dve2/dve2check.test: Add more - tests. - -2011-04-08 Alexandre Duret-Lutz - - Preliminary implementation of an int array compressor. - - * src/misc/intvcomp.hh: New file. - * src/misc/Makefile.am: Add it. - * src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test: New files. - * src/tgbatest/Makefile.am: Add them. - -2011-04-09 Alexandre Duret-Lutz - - Fix two spurious segfaults in test cases for the Python interface. - - * wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py: - Clean all used bdd variables before calling bdd_done(), so that - bdd_delref() is never called after bdd_done(). In NDEBUG builds, - bdd_delref() does not check whether the BuDDy is running or not, - and calling it after bdd_done() will crash. - -2011-04-09 Alexandre Duret-Lutz - - * HACKING: Add an example for using callgrind. - -2011-04-06 Alexandre Duret-Lutz - - * iface/dve2/dve2check.cc (main): Catch out-of-memory errors - during emptiness check or counterexample generation. - -2011-04-03 Alexandre Duret-Lutz - - * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use - a fixed-size memory pool for product_state instances. - -2011-04-03 Alexandre Duret-Lutz - - * iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state - instances and their variables. - -2011-04-03 Alexandre Duret-Lutz - - Add a fixed-size memory pool implementation. - - * src/misc/fixpool.hh: New file. - * src/misc/Makefile.am (misc_HEADERS): Add fixpool.hh. - -2011-04-03 Alexandre Duret-Lutz - - * HACKING (command): Some notes about link-time optimizations. - -2011-04-03 Alexandre Duret-Lutz - - * configure.ac: Pass CXXFLAGS/CFLAGS/CPPFLAGS debug/optimization - settings to sub configure. - -2011-03-31 Alexandre Duret-Lutz - - Introduct a down_cast macro. - - * src/misc/casts.hh: New file. - * src/misc/Makefile.am: Add it. - * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc, - src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh, - src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc, - src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc, - src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, - src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc, - src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, - src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, - src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc, - src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when - appropriate. - -2011-03-31 Alexandre Duret-Lutz - - Cosmetics. - - * src/sanity/style.test: Catch some binary operators not - delimited with spaces. - * src/tgbaalgos/bfssteps.cc, src/tgbaalgos/magic.cc, - src/tgbaalgos/reducerun.cc, src/tgbaalgos/se05.cc, - src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Fix these. - -2011-03-31 Alexandre Duret-Lutz - - Make state_explicit instances persistent objects. - - * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge - state_explicit and tgba_explicit::state. In the past, - state_explicit was a small object encapsulating a pointer to the - persistent tgba_explicit::state; and we used to clone() and - destroy() a lot of state_explicit instance. Now state_explicit is - persistent, and clone() and destroy() have no effects. - * src/tgba/tgbareduce.cc: Adjust, since this inherits from - tgbaexplicit and uses the internals of state_explicit. - * src/tgbatest/reductgba.cc: Fix deletion order for automata. - * src/tgba/tgba.hh (last_support_conditions_input_, - last_support_variables_input_): Make these protected, so - they can be zeroed by tgba_explicit. - -2011-03-30 Alexandre Duret-Lutz - - Remove tgba_reduc::format_state(). - - * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (format_state): - Remove this useless copy of the tgba_explicit_string::format_state - method. - -2011-03-30 Alexandre Duret-Lutz - - Protect the state destructor. - - Client code should always call the destroy() method instead. (It - was introduced in Spot 0.7.) - - * src/tgba/state.hh (state::~state): Make it protected. - -2011-03-30 Alexandre Duret-Lutz - - Speedup tgba_product when one of the argument is a Kripke structure. - - The gain is not very impressive. The runtime of the first example - in iface/dve2/README (also in dve2check.test) is 15% faster. - - * src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ... - * src/tgba/tgbaproduct.cc (tgba_succ_iterator_product, - tgba_succ_iterator_product_common): ... in these two classes. - (tgba_succ_iterator_product_kripke): New class to speedup - successor computation on Kripke structures. We can assume that - all the transitions leaving the same state have the same label. - (tgba_product::tgba_product, tgba_product::succ_iter): Use - tgba_succ_iterator_product_kripke when appropriate. - (tgba_product_init::tgba_product_init): Adjust for the case - where tgba_product did reverse its operands. - -2011-03-30 Alexandre Duret-Lutz - - * iface/dve2/dve2check.cc: Remove stray debug output. - -2011-03-30 Alexandre Duret-Lutz - - * src/tgba/tgbaproduct.hh: Do not include statebdd.hh. - -2011-03-29 Alexandre Duret-Lutz - - Include in python modules to workaround Swig bug. - - * wrap/python/spot.i, wrap/python/buddy.i: Include - because Swig 2.0.2 uses ptrdiff_t and does not do the include - itself. In g++ most libstdc++ standard headers have been changed - to no longer include as an implementation detail, so - the difference shows. - -2011-03-20 Alexandre Duret-Lutz - - * THANKS: Add Michael Weber for his help on the DiVinE interface. - -2011-03-18 Alexandre Duret-Lutz - - * src/ltltest/genltl.cc (syntax): Typos in the help text. - -2011-03-17 Alexandre Duret-Lutz - - Improve a reduction rule for "a M b". - - * src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b" - to "a & b" if "a" is a pure eventual formula, remove the - constraint on "b". - * src/ltltest/reduccmp.test: Add two tests. - -2011-03-11 Alexandre Duret-Lutz - - * NEWS: Mention recent changes to dotty_reachable. - -2011-03-10 Alexandre Duret-Lutz - - Add support for finite behaviors in the DVE interface. - - * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument. - * iface/dve2/dve2.cc (callback_context): Add a destructor - to simplify... - (dve2_succ_iterator::~dve2_succ_iterator) ... this one. - (convert_aps): Skip the dead proposition. - (dve2_kripke::dve2_kripke): Take a dead argument, and - setup alive_prop and dead_prop. - (compute_state_condition, get_succ): Use a cache for the - conditions and successor of the last state, to share - some work between these two function. Add loops on dead - states. - (load_dve2): Pass dead to dve2_kripke and convert_aps. - * iface/dve2/dve2check.cc: Add a -dDEAD option. - * iface/dve2/finite.test, iface/dve2/finite.dve: New file. - * iface/dve2/Makefile.am: Declare them. - -2011-03-10 Alexandre Duret-Lutz - - * iface/dve2/dve2.cc (convert_aps): Fix two typos while - parsing >= and >, mistakenly registered as <= and <. - -2011-03-07 Alexandre Duret-Lutz - - Remove the Nips interface. - - * NEWS: Mention it. - * configure.ac, README: Remove it. - * iface/Makefile.am (SUBDIRS): Remove nips. - * iface/nips/: Delete this directory. - -2011-03-07 Alexandre Duret-Lutz - - Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface. - Suggested by Yann Thierry-Mieg. - - * iface/dve2/dve2.cc (convert_aps): Allow string on the right - of operators, and look them up. - * iface/dve2/dve2check.test: Test this syntax. - -2011-03-07 Alexandre Duret-Lutz - - Add some tests for the DVE2 interface. - - * iface/dve2/defs.in, iface/dve2/dve2check.test, - iface/dve2/beem-peterson.4.dve: New files. - * iface/dve2/Makefile.am: Add them. - * configure.ac: Generate iface/dve2/defs. - -2011-03-07 Alexandre Duret-Lutz - - Clear the timer map to help valgrind. - - * src/misc/timer.hh (reset_all): New method. - * iface/dve2/dve2check.cc: Use it to help valgrind. - -2011-03-07 Alexandre Duret-Lutz - - Some documentation of about the dve2 interface. - - * iface/dve2/README: New file. - * NEWS: Mention it. - -2011-03-06 Alexandre Duret-Lutz - - * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes - to please sanity checks. - -2011-03-06 Alexandre Duret-Lutz - - Call divine to compile dve models. - - * iface/dve2/dve2.cc (compile_dve2): New function. Compile - the *.dve source if there is no newer *.dve2C already. - (load_dve2): Call compile_dve2 when given a *.dve file. - * iface/dve2/dve2.hh (load_dve2): Document it. - -2011-03-06 Alexandre Duret-Lutz - - Allow atomic propositions and identifiers like `X.Y'. - - * src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND. Allow - it in atomic propositions. - * src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept - `.' in identifiers. - * src/misc/bareword.cc (is_bareword): Accept `.' inside - barewords, so that there is no need to quote `X.Y'. - * src/ltltest/parse.test: Do not use `.' as and operator.. - -2011-03-06 Alexandre Duret-Lutz - - Augment dve2check to perform LTL model checking. - - * iface/dve2/dve2check.cc: Add many option to perform - emptiness check and other debugging tasks. - -2011-03-05 Alexandre Duret-Lutz - - Teach the DVE2 interface about enumerated types. - - * iface/dve2/dve2.cc (convert_aps): Add support for - enumerated types. E.g. an atomic proposition such - as "P_0.CS" really means "P_0 == CS". - -2011-03-05 Alexandre Duret-Lutz - - Teach the DVE2 interface about atomic propositions such as "a <= - 10" or "b != 3". This only work for integer variables presently. - - * iface/dve2/dve2.hh (load_dve2): Take an atomic_prop_set - argument to indicate the AP to observe. - * iface/dve2/dve2.cc (convert_aps): New function. Parse the - atomic propositions in format them in a prop_set structure that - will allow fast generation of the state condition. - (load_dve2): Call convert_aps, and pass the resulting prop_set - structure to the kripke object. - (dve2_kripke::dve2_kripke): Store the prop_set structure. - (dve2_kripke::~dve2_kripke): Release the prop_set, and unregister - the bdd_variable associated to it. - (compute_state_condition): New method that uses the prop_set. - (succ_iter, state_condition): Call compute_state_condition(). - * iface/dve2/dve2check.cc: Adjust the call to load_dve2 to - pass it atomic propositions read from the command line. - -2011-03-05 Alexandre Duret-Lutz - - Display states variables in the state label. - - * iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Retrieve - the name of all the state variables. - (dve2_kripke::format_state): Use them to format the name - of the state. - -2011-03-05 Alexandre Duret-Lutz - - We can now explore a divine2 compiled model, but the atomic - properties are still missing. - - * iface/dve2/dve2.cc, iface/dve2/dve2.hh: Add - classes for presenting the DiVinE2 model as a kripke object. - (load_dve2): Load the *.dve2C file using libltdl. - * iface/dve2/Makefile.am: Add a dve2check program. - * iface/dve2/dve2check.cc: New file. Currently it just - outputs the reachability graph using dotty. - -2011-03-05 Alexandre Duret-Lutz - - Setup libltdl in ltdl/, so we can use it in the dve2 interface. - - Don't keep it under version control since it is installed by - autoreconf. - - * configure.ac: Call LT_CONFIG_LTDL_DIR and LTDL_INIT. - * README: Mention ltdl/. - * Makefile.am: Recurse into ldtl. - * iface/dve2/Makefile.am: Link with it. - -2011-03-05 Alexandre Duret-Lutz - - Setup build system for a new dve2 interface. - - * iface/dve2/dve2.cc, iface/dve2/dve2.hh: New dummy files. - * iface/dve2/Makefile.am: New file. - * iface/Makefile.am (SUBDIRS): Add dve2. - * configure.ac: Build iface/dve2/Makefile. - * README: Mention the new directory. - -2011-03-05 Alexandre Duret-Lutz - - Using double borders for acceptance states in SBAs. - - * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new - assume_sba argument. - * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new - mark_accepting_states arguments. - (dotty_bfs::process_state): Check if a state is accepting using - the state_is_accepting() method for tgba_sba_proxies, or by - looking at the first outgoing transition of the state. Pass - the result to the dectorator. - (dotty_reachable): Adjust function. - * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc, - src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc - (state_decl): Add an "accepting" argument, and use it to - decorate accepting states with a double border. - * src/tgbatest/ltl2tgba.cc: Keep track of whether the output - is an SBA or not, so that we can tell it to dotty(). - * wrap/python/ajax/spot.in: Likewise. - * wrap/python/cgi-bin/ltl2tgba.in: Likewise. - -2011-03-05 Alexandre Duret-Lutz - - * src/ltltest/genltl.cc (GF_n): Really use "op". - -2011-03-04 Alexandre Duret-Lutz - - * wrap/python/ajax/spot.in: Use the degeneralized automaton if - available while computing the emptiness check. - -2011-03-04 Alexandre Duret-Lutz - - Speedup build_result() called by minimize_dfa(). - - * src/tgbaalgos/minimize.cc (build_result): Speed it up by - removing one useless loop, creating many duplicate transitions - that had to be merged. - -2011-03-01 Alexandre Duret-Lutz - - * src/ltltest/genltl.cc: Add 10 more LTL formula classes. - -2011-02-21 Alexandre Duret-Lutz - - * src/tgba/bdddict.hh: Add more documentation. - -2011-02-21 Alexandre Duret-Lutz - - * src/misc/escape.hh: Correct documentation. - -2011-02-14 Alexandre Duret-Lutz - - Correct tgba_explicit::compute_support_conditions. - - * src/tgba/tgbaexplicit.cc (tgba_explicit::compute_support_conditions): - Fix logic. This function has always been returning bddtrue instead - of the actual computed value... - -2011-02-10 Alexandre Duret-Lutz - - Enable VERBOSE logs for nips, greatspn, and python tests. - - * wrap/python/tests/run.in, iface/nips/nipstest/defs.in, - iface/gspn/defs.in: Do not disable VERBOSE when running from "make - check". Since we have started using parallel-check on 2009-08-31, - we should always send verbose output to the log. - -2011-02-10 Alexandre Duret-Lutz - - This should finally fix kv.test and dotty.test on the LIP6 buildfarm. - - * src/tgbatest/kv.test, iface/nips/nipstest/dotty.test: Don't rely - on the ${DOT-...} syntax, because DOT is always set and might be - set to the empty value. - -2011-02-10 Alexandre Duret-Lutz - - * HACKING (Running coverage tests): New section. - -2011-02-09 Alexandre Duret-Lutz - - Previous patch did not work on MacOS X, and I don't have shell - access to that host. - - * src/tgbatest/kv.test: Use ${DOT-true} instead of ${DOT-:}. I - don't know, the MacOS shell must be mixing the syntaxes for - ${DOT:-} and ${DOT-:}. - * iface/nips/nipstest/dotty.test: Likewise - -2011-02-09 Alexandre Duret-Lutz - - Avoid running "dot" when it is not installed... - - * src/tgbatest/kv.test: Do not run dot if it is not installed. - * iface/nips/nipstest/dotty.test: Likewise - -2011-02-08 Alexandre Duret-Lutz - - Add some tricks into HACKING. - - * README: Typo. - * HACKING: s/CVS/GIT/ and add some tricks about libtool and doxygen. - -2011-02-08 Alexandre Duret-Lutz - - Adjust the WDBA test to count for sub-transitions. - - * bench/wdba/run: Use -kt to count sub-transitions. - * bench/wdba/README: Adjust comments. - -2011-02-08 Alexandre Duret-Lutz - - Fix a spurious g++ warning observed on Darwin builds. - - * src/tgba/taatgba.cc (taa_succ_iterator::taa_succ_iterator): - Initialize iterator i to silence a spurious g++ warning on Darwin. - -2011-02-07 Alexandre Duret-Lutz - - * configure.ac: s/gnit/gnu so that we can use 0.7.1a as a version. - -2011-02-07 Alexandre Duret-Lutz - - * NEWS: Typos. - -2011-02-07 Alexandre Duret-Lutz - - * NEWS, configure.ac: Bump version to 0.7.1a - -2011-02-07 Alexandre Duret-Lutz - - Release Spot 0.7.1. - - * NEWS: Update for 0.7.1. - * configure.ac: Bump version to 0.7.1. - -2011-02-07 Alexandre Duret-Lutz - - Generalize patch from 2011-02-03 by allowing guards like "! (...)". - - * src/neverparse/neverclaimscan.ll: Allow space between ! and (. - * src/tgbatest/neverclaimread.test: Add space for testing. - -2011-02-06 Alexandre Duret-Lutz - - Speedup scc_filter on tgba_explicit_number automata. - - * src/tgbaalgos/sccfilter.cc (scc_filter): If the input automaton - is an instance of tgba_explicit_number, create a similar automaton - for output, instead of a tgba_explicit_string. - -2011-02-06 Alexandre Duret-Lutz - - Document the new operators in the on-line tools. - - * wrap/python/ajax/ltl2tgba.html: Mention Goal's ~, -->, and <--> - operators. - * wrap/python/cgi-bin/ltl2tgba.in: Likewise. - -2011-02-06 Alexandre Duret-Lutz - - Fix a segfault in WDBA minimization. - - * src/tgbaalgos/minimize.cc (build_result, minimize_dfa, - minimize_wdba): Correctly handle (i.e. ignore) useless states. - * src/tgbatest/ltl2tgba.test: Add two more tests. - -2011-02-05 Alexandre Duret-Lutz - - Fix call to scc_filter in the CGI script. - - * wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f), - and keep some extra acceptance conditions (-R3) when - degeneralizing. The converse was done. - -2011-02-04 Alexandre Duret-Lutz - - * wrap/python/cgi-bin/ltl2tgba.in: Fix python error occurring - only when the user did not make any error... - -2011-02-04 Alexandre Duret-Lutz - - Prevent Spot from using an installed BuDDy version that does not - have the latest function we added. Reported by Kristin Rozier. - - * m4/buddy.m4 (AX_CHECK_BUDDY): Check for bdd_setxor. - -2011-02-04 Alexandre Duret-Lutz - - Add a way to count the number of sub-transitions. - - * src/tgbaalgos/stats.hh (tgba_sub_statistics): New class. - (sub_stats_reachable): New function. - * src/tgbaalgos/stats.cc (sub_stats_bfs): New class. - (tgba_sub_statistics::dump, sub_stats_reachable): New function. - * src/tgbatest/ltl2tgba.cc (-kt): New option. - * src/tgbatest/ltl2tgba.test: Use -kt. - -2011-02-03 Alexandre Duret-Lutz - - Read guard of the form !(x) in neverclaims. - - So far all neverclaims encountered would use (!(x)), but the - files from the Büchi store do not. - - * src/neverparse/neverclaimscan.ll: Accept ! in front of guard, - so that we can read Promela files from Goal's Büchi store. - * src/tgbatest/neverclaimread.test: Test it. - -2011-02-03 Alexandre Duret-Lutz - - Recognize Goal's syntax for Boolean operators. - - * src/ltlparse/ltlscan.ll: Recognize ~, -->, and <--> operators - from Goal, to ease the use of formulas provided by the Goal team. - * src/ltltest/equals.test: Use these once, just to be on the - safe side. - -2011-02-03 Alexandre Duret-Lutz - - Minor fixes to ltl2tgba.html. - - * wrap/python/ajax/css/ltl2tgba.css, - wrap/python/ajax/ltl2tgba.html: Tweak a few things for Firefox - 3.0, and fix a tag. - -2011-02-01 Alexandre Duret-Lutz - - * NEWS, configure.ac: Bump version to 0.7a. - -2011-02-01 Alexandre Duret-Lutz - - Release Spot 0.7. - - * NEWS, configure.ac: Bump version to 0.7. - -2011-02-01 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.test: Fix previous test case. - -2011-01-28 Alexandre Duret-Lutz - - Fixup minimize_monitor(). - - * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding - incorrect monitor if the input tgba is not deterministic. - * src/tgbatest/ltl2tgba.test: Add test case. - -2011-01-27 Alexandre Duret-Lutz - - Report formulas that are both safety and guarantee. - - * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both - safety and guarantee. - * src/tgbatest/obligation.test: Add cases. - -2011-01-27 Alexandre Duret-Lutz - - Rename is_safety_automaton() as is_guarantee_automaton() and - implement is_safety_mwdba(). - - Note: I swapped the name of safety and guarantee when I - implemented is_safety_automaton() on 2010-03-20. Fortunately, - is_safety_automaton() was only used where is_guarantee_automaton() - would have been correct. - - * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ... - (is_guarantee_automaton): ... this. - (is_safety_mwdba): New function. - * src/tgbaalgos/safety.hh: Adjust and add documentation. - * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead - of is_safety_automaton(). - * src/tgbatests/safety.test: Rename as ... - * src/tgbatests/obligation.test: ... this, and augment the - test. - * src/tgbatest/Makefile.am: Adjust. - * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula - represent a safety, guarantee, or obligation property. - * NEWS: Adjust. - -2011-01-27 Alexandre Duret-Lutz - - * NEWS: Minor rewritings. - -2011-01-27 Alexandre Duret-Lutz - - Replace delete by destroy in comments dealing with states. - - * src/tgba/succiter.hh, src/tgba/tgba.hh, - src/tgba/tgbabddconcrete.hh, src/tgba/tgbaproduct.hh, - src/tgba/tgbaunion.hh, src/tgbaalgos/bfssteps.hh, - src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.hh, - src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/replayrun.cc, - src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Update comments - to say that we "destroy" a state instead of "deleting" it. - -2011-01-26 Alexandre Duret-Lutz - - Update gspn interface for recent tools. - - * iface/gspn/ssp.cc: Use the new destroy() interface, and - fix a couple of recent g++ reports. - * iface/gspn/gspn.cc: Adjust to newer g++. - -2011-01-25 Alexandre Duret-Lutz - - Introduce a destroy() method on states, and use it instead of delete. - - Right now, destroy() just executes "delete this". But in a later - version, we will rewrite tgba_explicit so that it does not - allocate new states (and the destroy() method for explicit state - will do nothing). - - * src/tgba/state.hh (state::destroy): New method, to replace - state::~state() in the future. - (shared_state_deleter): New function. - * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc, - src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc, - src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc, - src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, - src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, - src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc, - src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc, - src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc, - src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, - src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx, - src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh, - src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc, - src/tgbaalgos/reductgba_sim.cc, - src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc, - src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, - src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc, - src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call - "s->destroy()" instead of "delete s". - * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc: - Pass shared_state_deleter to the shared_ptr constructor, so that - it calls destroy() instead of delete. - -2011-01-26 Alexandre Duret-Lutz - - * wrap/python/ajax/ltl2tgba.html: Display the Spot version in - the tooltip over the Spot logo. - -2011-01-26 Alexandre Duret-Lutz - - * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add icons/mail.png. - -2011-01-26 Alexandre Duret-Lutz - - * NEWS: Mention the new on-line ltl2tgba version. - -2011-01-26 Alexandre Duret-Lutz - - Updates to the ltl2tgba ajax version. - - * wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and - enable auto-update automatically after the first submission. Add - tools tips for the "Desired Output" tabs, and the Spot logo. - Add a email icon to encourage feedback. - * wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and - send button. Set position of mail icon. - * wrap/python/ajax/logos/mail.png: New logo, based on a public - domain SVG icon retrieved today from - http://commons.wikimedia.org/wiki/File:Internet-mail.svg - -2011-01-19 Alexandre Duret-Lutz - - * wrap/python/ajax/ltl2tgba.html: Disable the browser spellcheck - on the input box. - -2011-01-18 Alexandre Duret-Lutz - - Preliminary implementation of an ajax-based ltl2tgba translator. - - * configure.ac: Output wrap/python/ajax/Makefile. - * wrap/python/Makefile.am (SUBDIRS): Add ajax. - * wrap/python/ajax/Makefile.am, wrap/python/ajax/README, - wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files. - * wrap/python/ajax/css/, wrap/python/ajax/js, - wrap/python/ajax/logos: New directories. - * README: Document wrap/python/ajax/. - -2011-01-17 Alexandre Duret-Lutz - - Do not output empty parse error blocks in the CGI script. - - * wrap/python/spot.i: Provide a __nonzero__() method for - parse_error_list. - * wrap/python/cgi-bin/ltl2tgba.in: Do not call format_parse_errors() - unconditionally. - -2011-01-12 Alexandre Duret-Lutz - - Fix "unused function" warnings reported by clang++. - - * src/evtgbaparse/Makefile.am, src/ltlparse/Makefile.am, - src/neverparse/Makefile.am, src/tgbaparse/Makefile.am - (AM_CPPFLAGS): Define -DYY_NO_INPUT so that the unused yyinput() - function does not get compiled. - * src/eltlparse/Makefile.am (AM_CPPFLAGS): Likewise. - (AM_CXXFLAGS): Also enable warnings. - * src/eltlparse/eltlparse.yy: Move helper functions from - the "%code requires" block to the "%code" block, so that they - do not appear in the eltlparse.hh file (which is included in - two places...). - * iface/nips/nips.cc (search_error_callback_assert): Comment - this unused function. - -2011-01-12 Alexandre Duret-Lutz - - - Fix segfault with g++-3.3. - - * src/tgbaalgos/minimize.cc (minimize_dfa): Fix deletion of the - state_set_map. It led to a crash when compiled with g++-3.3. - -2011-01-12 Alexandre Duret-Lutz - - Fix a compilation failure with g++-3.3. - - * src/misc/hash.hh (identity_hash): New function. - * src/tgba/tgbaexplicit.hh (tgba_explicit_number): Use - identity_hash instead of std::tr1::hash that does not - exist with g++-3.3. - -2011-01-07 Alexandre Duret-Lutz - - Fix usage of minimize_obligation in the CGI script. - - * wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use - minimize_obligation_new a pass the formula. - * wrap/python/spot.i (minimize_obligation_new): New function, to - cope with the strange specification of spot::minimize_obligation() - not always creating a new automaton. - -2011-01-06 Alexandre Duret-Lutz - - * NEWS: Convert to utf-8 and fix a few typos. - -2011-01-06 Alexandre Duret-Lutz - - '([]a && XXXX!a)' was not properly minimized because its - translation contain useless SCCs that where not ignored for - minimization. - - * src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless - SCCs before minimization. - * src/tgbatest/ltl2tgba.test: Add a check. - -2011-01-06 Alexandre Duret-Lutz - - The neverclaim output by spin -f '([]a && XXXX!a)' was not - understood by Spot. - - * src/neverparse/neverclaimparse.yy: Support "if :: false fi;" - instructions. Spin sometimes output these on dead states. - Also rewrite the "transitions" rule as a left recursion. - * src/tgbatest/neverclaimread.test: Adjust output because - of the right->left recursion change, and add two more formula - to submit to Spin to test its output. - -2011-01-06 Alexandre Duret-Lutz - - Speed up computation of non_final states for minimize_wdba. - - * src/tgbaalgos/minimize.cc (minimize_dfa): Take final and - non_final sets. - (minimize_wdba): Fill in non_final at the same time as final. - (minimize_monitor): Call state_set() to fill non_final. - (init_sets): Simplify and rename as ... - (state_set): ... this. - -2011-01-06 Alexandre Duret-Lutz - - Introduce a class to complement a WDBA on-the-fly. - - * src/tgba/wdbacomp.hh, src/tgba/wdbacomp.cc: New file. - * src/tgba/Makefile.am: Add them. - * src/tgbaalgos/minimize.cc (minimize_obligation): Use - wdba_complement(). - -2011-01-05 Alexandre Duret-Lutz - - * src/tgbatest/Makefile.am: Remove the unused minimize program. - * src/tgbatest/minimize.cc: Delete. - -2011-01-05 Alexandre Duret-Lutz - - Cleanup the minimize.hh interface. - - * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc - (minimize): Split into ... - (minimize_wdba, minimize_monitor): ... these two functions. - * src/tgbatest/ltl2tgba.cc (main): Adjust the call to - minimize_monitor. - * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to - minimize_monitor and minimize_obligation. - * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba, - minimize_obligations. - * src/tgba/tgbaexplicit.hh (tgba_explicit_string) - (tgba_explicit_formula, tgba_explicit_number): Add fake - declarations so that SWIG can see they inherits from tgba. - -2011-01-05 Alexandre Duret-Lutz - - Cleanup the DFA minimization algorithm. - - * src/tgbaalgos/minimize.cc (minimize): Move the minimization - code into... - (minimize_dfa): ... this new function, and fix the condition - under which a partition is considered to be minimal. Also - use a map instead of a list to lookup known formulae. - -2011-01-05 Alexandre Duret-Lutz - - Speed up the obligation test. - - * src/tgbaalgos/minimize.cc (minimize_obligation): Do not - minimize aut_neg_f, complement min_aut_f instead. - * src/tgbaalgos/minimize.hh: Adjust description. - -2011-01-05 Alexandre Duret-Lutz - - * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm - to label transient states. - -2011-01-04 Alexandre Duret-Lutz - - Rewrite the check of WDBA state acceptance in minimize(). - - * src/tgbaalgos/powerset.hh (power_map): New structure, allowing - the caller to retrieve the set of original states corresponding to - the set in the deterministic automaton. - (power_set): Adjust prototype to take a power_map instead of the - acc_list. - * src/tgbaalgos/powerset.cc (power_set): Strip all code using - acc_list, and update power_set. - * src/tgbaalgos/minimize.cc (minimize): Rewrite, using an - algorithm similar to the one in the Dax paper to check whether - state of the minimized automaton should be accepting. - -2011-01-04 Alexandre Duret-Lutz - - * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial, - scc_map::one_state_of): Two new helper functions. - -2011-01-04 Alexandre Duret-Lutz - - * src/tgba/tgbaunion.hh: Remove one useless include. - -2011-01-04 Alexandre Duret-Lutz - - * README: Mention bench/wdba/. - -2011-01-04 Alexandre Duret-Lutz - - Define tgba_product_init, a new kind of product with different - initial states. - - * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc - (tgba_product_init): New class. - -2011-01-04 Alexandre Duret-Lutz - - * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many - failure because the minimization() algorithm is currently - incorrect when applied to non-weak automata. - -2011-01-04 Alexandre Duret-Lutz - - * src/tgbaalgos/scc.hh: Typo in documentation. - -2011-01-04 Alexandre Duret-Lutz - - Move the logic for detecting when the minimize() algorithm is - correct from ltl2tgba to the library. - - * src/tgbaalgos/minimize.hh, - src/tgbaalgos/minimize.cc (minimize_obligation): New function. - * src/tgbatests/ltl2tgba.cc (main): Fix constness of automata, - and call minimize_obligation() for -R3b. - -2010-12-26 Alexandre Duret-Lutz - - Make minimization of obligation properties and deterministic - monitor available in the CGI script. - - * wrap/python/spot.i: Declare the minimize() interface. - * wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and - reduce_wdba options. - -2010-12-14 Alexandre Duret-Lutz - - Add a WDBA benchmark. - - * bench/wdba/: New directory. - * bench/Makefile.am (SUBDIRS): Add wdba. - * NEWS: Mention it. - * configure.ac: Output bench/wdba/defs and bench/wdba/Makefile. - -2010-12-13 Alexandre Duret-Lutz - - * NEWS: Update the news about minimization. - -2010-11-26 Alexandre Duret-Lutz - - Speed up wdba.test, it was too slow for our buildfarm. - - * src/tgbatest/wdba.test: Speed up execution by running only a - couple of formula with valgrind. Half of those with`-l -R3b' and - the other half with `-f -R3'. - -2010-11-26 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc (syntax): Regroup -M, -s, and -S option - under the same heading "automaton conversion". - -2010-11-25 Alexandre Duret-Lutz - - Preliminary support for monitors. - - * src/tgbatest/ltl2tgba.cc (-M): New option for building - deterministic monitors. - * src/tgbaalgos/minimize.cc (minimize): Take a monitor - argument and adjust the code. - * src/tgbaalgos/minimize.hh (minimize): Document it. - -2010-11-25 Alexandre Duret-Lutz - - "ltl2tgba -Rm -X foo.tgba" would fail. - - * src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without - knowing the formula whose automaton is minimized. - -2010-11-25 Alexandre Duret-Lutz - - Fix bugs in minimize(). - - * src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory - leaks and a usage of the wrong automaton. - * src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with - valgrind. This caught all the bugs fixed above. - -2010-04-13 Alexandre Duret-Lutz - - Fix bugs in minimize(), caught by spotlbtt.test. - - * src/tgbaalgos/minimize.cc (minimize): Don't add acceptance - conditions if the final set is empty. - * src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state - to acc_list if it is accepting. Also do not compute an SCC build - map if we don't have to build acc_list. - -2010-04-13 Alexandre Duret-Lutz - - "ltl2tgba -Rm" will apply WDBA-minimization only if correct. - - * src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when - it is correct. Either we can quickly determine that a formula or - its negation is a safety formula, or we can slowly check the - equivalence of the WDBA-minimized automaton and the original - automaton. - * src/tgbatest/wdba.test: New test. - * src/tgbatest/safety.test: Adjust comment. - * src/tgbatest/spotlbtt.test: Use -Rm. - * src/tgbatest/Makefile.am (TESTS): Add wdba.test. - -2010-04-13 Alexandre Duret-Lutz - - Better resource handling in minimization. - - * src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton. - * src/tgbaalgos/minimize.cc (minimize): Remove the call to - unregister_variable() at the end. It was both - wrong (unregistering only the first variable) and useless ("delete - del_a" will unregister all these variables). Use a map and a set - to keep track of free BDD variable and reuse them, otherwise the - algorithm would sometimes use more variables than allocated. - -2010-03-20 Alexandre Duret-Lutz - - Implement is_safety_automaton(). - - * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New - files. - * src/tgbaalgos/Makefile.am: Add them. - * src/tgbatests/ltl2tgba.cc: Add option "-O". - * src/tgbaalgos/scc.hh: Update documentation. - * src/tgbatest/Makefile.am (TESTS): Add safety.test. - * src/tgbatest/safety.test: New file. - -2010-03-26 Felix Abecassis - - * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. - -2010-03-20 Felix Abecassis - - Small fixes. - - * src/tgbatest/minimize.cc: Delete useless includes. - * src/tgbaalgos/minimize.cc: Delete useless includes, - fixed acceptance conditions. - * src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization. - * src/tgba/tgbaexplicit.cc: Fixed typo. - -2010-03-20 Felix Abecassis - - Test program for the minimization algorithm. - - * src/tgbatest/minimize.cc: New file. Minimize an automaton - from a LTL formula and compare the size of the initial automaton - to the size of the minimized automaton. - -2010-03-20 Felix Abecassis - - * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: - New files. Algorithm to minimize an automaton using first the powerset - construction to determinize the input automaton, the automaton is then - minimized using the standard algorithm, using BDDs to check if states - are equivalent. - -2010-03-20 Felix Abecassis - - Modify the powerset algorithm to keep track of accepting states - from the initial automaton. - - * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: - Added class tgba_explicit_number, a tgba_explicit where states are - labelled by integers. - * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc: - When building the deterministic automaton, keep track of which states - were created from an accepting state in the initial automaton. - The states are added to the new optional parameter (if not 0), - acc_list. - Use tgba_explicit_number instead of tgba_explicit_string to build - the result. - * src/tgbaalgos/scc.cc (spot): Small fix. - Print everything on std::cout. - -2011-01-05 Alexandre Duret-Lutz - - Fix computation of support_conditions for bdd-based TGBA. - This fixes a bug in the powerset of such TGBA on the minimize branch. - - * src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also - account for the conditions from the acceptance relations. - * rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc - (acceptance_conditions_support): New variable to hold the value - of bdd_support(acceptance_conditions_support). - * src/tgba/tgbabddconcretefactory.cc (finish): Update - data_.acceptance_conditions_support. - -2010-12-26 Alexandre Duret-Lutz - - * wrap/python/cgi-bin/ltl2tgba.in: Remove all "new" markers. - -2010-12-23 Alexandre Duret-Lutz - - Define SWIG_TYPE_TABLE as suggested by the SWIG documentation. - - * wrap/python/Makefile.am: Add -DSWIG_TYPE_TABLE=spot. - -2010-12-23 Alexandre Duret-Lutz - - Use swig2.0 if available. - - * configure.ac: Search for swig2.0 and swig. - * wrap/python/Makefile.am: Use $(SWIG). - -2010-12-23 Alexandre Duret-Lutz - - Get rid of ltihooks.py. - - ltihooks.py apparently breaks the import mechanisms of Python 2.6, - causes SWIG's runtime to fail to share a global type table, and - yields various failures in our tests. - - * wrap/python/ltihooks.py: Delete. - * wrap/python/Makefile.am (EXTRA_DIST): remove ltihooks.py. - * 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, wrap/python/tests/optionmap.py, - wrap/python/tests/setxor.py: Do not use ltihooks. - * wrap/python/tests/run.in (pypath): Include the .libs/ directories - in the search path so that Python can find the *.so libraries. - * wrap/python/cgi-bin/ltl2tgba.in: Insert the .libs/ directories - into sys.path instead of importing ltihooks. - -2010-12-12 Alexandre Duret-Lutz - - * NEWS: Summarize recent changes. - -2010-12-11 Alexandre Duret-Lutz - - Merge transitions in tgba_tba_proxy. - - With this change the output of - ltl2tgba -f -x -k -DS "GF(p_1) & ... & GF(p_n) - uses less than (n+1)^2 transitions when it used - exactly (n+1)*(2^n) transitions before. - - * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Merge - transitions going to the same states if they are both accepting or - if neither are. - (state_ptr_bool_t, state_ptr_bool_less_than): Helper type to - store a transition in tgba_tba_proxy_succ_iterator. - * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh - (tgba_tba_proxy::transition_annotation): Remove. We cannot - implement this method if transitions are merged. - * src/tgbatest/ltl2tgba.test: Add a test. - -2010-12-10 Alexandre Duret-Lutz - - Augment the size of the ltlclasses benchmark. - - * bench/ltlclasses/run: Augment the max size to 20. - * bench/ltlcounter/run: Typo in comment. - -2010-12-10 Alexandre Duret-Lutz - - Introduce -ks to print only the size of the automaton (without - SCC information). - - * src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option. - * src/tgbatest/ltl2tgba.test, bench/ltlclasses/run, - bench/ltlcounter/run: Use -ks instead of -k to speed things up. - -2010-12-09 Alexandre Duret-Lutz - - Use a cache to speed up tgba_tba_proxy. - - tgba_tba_proxy used to spend a lot of time (re)computing the - acceptance condition common to all outgoing transition of a state. - - * src/tgba/tgbatba.hh (accmap_): New cache. - (common_acceptance_conditions_of_original_state): New method. - * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync) - Call common_acceptance_conditions_of_original_state() instead of - computing the result. - (~tgba_tba_proxy): Cleanup the cache. - (common_acceptance_conditions_of_original_state): Implement it. - -2010-12-07 Alexandre Duret-Lutz - - * src/ltltest/Makefile.am (genltl_SOURCES): Add missing variable. - -2010-12-07 Alexandre Duret-Lutz - - * README: Mention bench/ltlclases/. - -2010-12-04 Alexandre Duret-Lutz - - Preliminary benchmark using genltl, introduced earlier. - - * bench/ltlclasses/: New benchmark. - * bench/Makefile.am: Add it. - * configure.ac: Adjust. - -2010-12-04 Alexandre Duret-Lutz - - * src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s. - -2010-12-04 Alexandre Duret-Lutz - - Preliminary implementation of a tool to generate some interesting - families of LTL formulae. - - * src/ltltest/genltl.cc: New file. Based on five classes of - formulae defined in a paper by Cichón, Czubak, and Jasiński. - * src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl. - -2010-12-03 Alexandre Duret-Lutz - - Add full_parent support to to_spin_string(). - - * src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent - optional parameter, like for the to_string() function. - * src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the - handling of full_parent. - (to_spin_string_visitor): Handle full_parent. - -2010-12-01 Alexandre Duret-Lutz - - Halve the number of application of eventual_universal_visitor in - reduce_visitor::visit(binop). - - * src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_): - Move this method... - (recurse_eu): ... outside as a separate function. Likewise for - the universal/eventual result struct. - (reduce_visitor::visit(binop)): Call recurse_eu() once to replace - two calls to is_eventual and is_universal, thus replacing two - recursions by one. - -2010-12-01 Alexandre Duret-Lutz - - Move the eventual-universal functions where the belong. - - * src/ltlvisit/syntimpl.cc (eventual_universal_visitor, - is_eventual, is_universal): Move ... - * src/ltlvisit/reduce.cc (eventual_universal_visitor, - is_eventual, is_universal): ... here. - -2010-11-30 Alexandre Duret-Lutz - - * src/ltlvisit/randomltl.cc (random_ltl::update_sums): Typo in string. - -2010-11-30 Alexandre Duret-Lutz - - Remove a quadratic behavior in eventual_universal_visitor. - - * src/ltlvisit/syntimpl.cc (eventual_universal_visitor): Use - a union to store the eventual and universal properties as two - bit in a bit-field, and "AND" both of them at once. - (eventual_universal_visitor::recurse_un, - eventual_universal_visitor::recurse_ev): Replace these - two functions by ... - (eventual_universal_visitor::recurse_): ... this one, that - returns both bits as an unsigned. - -2010-12-01 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc (main): Delete the accepting run - even if it hasn't been printed. - -2010-11-30 Alexandre Duret-Lutz - - Rationalize options for counter-example output. - - * src/tgbatest/ltl2tgba.cc (main): Either replay the accepting - run or print it, but do not do both. - * src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR - when we expect the run to be displayed. - -2010-11-30 Alexandre Duret-Lutz - - Fix a GCC 4.6 warning. - - * src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A - variable (the upcoming GCC 4.6 would warn about it) and set opt_ec - to 1 if -A is used without -e. - -2010-11-27 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc (syntax): Typo. - -2010-11-27 Alexandre Duret-Lutz - - Another Clang report. - - * iface/nips/nips.cc (format_state): Do not use a variable-sized - array, this is not allowed in C++. - -2010-11-27 Alexandre Duret-Lutz - - Fix more errors reported by Clang. - - * src/tgbaalgos/reducerun.hh (tgba_run): Predeclare as a struct - since this is what it is. - * src/tgbatest/randtgba.cc (main): Avoid using "i" with two - different type in the same loop. - -2010-11-26 Alexandre Duret-Lutz - - Finalize Kripke interface. - - * src/kripke/fairkripke.hh, src/kripke/fairkripke.cc, - * src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and - document the Kripke interface. I have tested it by updating - checkpn to use it. - -2010-11-25 Alexandre Duret-Lutz - - Never claim output used to print the degeneralized automaton - before some optional operations (like more optimizations, or a - product). - - * src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last - automaton computed, not just the automaton when we degeneralized - it. We may have applied other algorithms since the original - degeneralization. - -2010-11-25 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.test: Test both -l and -f. This should - have been done on 2010-01-30 when the default translation was - changed from -l to -f. - -2010-11-25 Alexandre Duret-Lutz - - * src/tgbaalgos/scc.hh: Typos in the documentation. - -2010-11-24 Alexandre Duret-Lutz - - * src/tgbaalgos/sccfilter.hh: Fix some typos in the documentation. - -2010-11-24 Alexandre Duret-Lutz - - Suggest using bddtrue and bddfalse instead of bdd_true() and - bdd_false(). - - * src/sanity/style.test: Catch uses of bdd_true() or bdd_false(). - -2010-11-20 Alexandre Duret-Lutz - - Fix some struct/class missmatches reported by clang. - - * src/ltlast/predecl.hh: Predeclare the LTL AST nodes as class, - not struct. - * src/ltlast/nfa.hh (formula_tree::node): Predeclare as struct, - not class. - -2010-11-07 Alexandre Duret-Lutz - - Add interface for and test the bdd_setxor() function added to Buddy. - - * wrap/python/buddy.i (bdd_setxor): New function. - * wrap/python/tests/setxor.py: New file. - * wrap/python/tests/Makefile.am (TESTS): Add setxor.py. - -2010-11-06 Alexandre Duret-Lutz - - * src/Makefile.am (libspot_la_LIBADD): Rename libneverclaimparse.la - as libneverparse.la. - * src/neverparse/Makefile.am: Install files in - $(pkgincludedir)/neverparse, not $(pkgincludedir)/neverclaimparse. - -2010-11-06 Alexandre Duret-Lutz - - Cosmetics to please sanity checks. - - * src/neverparse/public.hh, src/neverparse/parsedecl.hh: Fix - inclusion guards. - * src/tgba/tgbaexplicit.hh, src/tgbatest/emptchk.test, - src/tgbatest/ltl2tgba.cc: Fix trailing whitespaces. - -2010-11-06 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc: Clock the time spent reading -P file. - -2010-11-06 Alexandre Duret-Lutz - - * src/tgbatest/neverclaimread.test: Check that Spot can read the - neverclaims it outputs. - -2010-11-06 Alexandre Duret-Lutz - - Do not output a counterexample by default in ltl2tgba, introduce - options -C and -CR for that. - - * src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control - whether we want the accepting run to be printed or replayed. - * src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test, - src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, - src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR. - -2010-11-06 Alexandre Duret-Lutz - - Make sure the neverclaim parser works on the output of spin and - ltl2ba. - - * src/neverparse/neverclaimparse.yy: Accept multiple labels - for the same state. Honor accepting states. Forward parse - error from the parser used for guards. Accept "false" as a - single instruction for a state. - * src/neverparse/neverclaimscan.ll: Recognize "false" specifically, - and remove the ";" hack. - * src/tgba/tgbaexplicit.cc - (tgba_explicit_string::~tgba_explicit_string): Adjust not to - destroy a state twice. - * src/tgba/tgbaexplicit.hh - (tgba_explicit_string::add_state_alias): New function. - * src/tgbatest/defs.in (SPIN, LTL2BA): New variables. - * src/tgbatest/neverclaimread.test: Check error messages for - syntax errors in guards. Make sure we can read the output - of `spin -f' and `ltl2ba -f' on a few test formulae. - -2010-11-06 Alexandre Duret-Lutz - - Cleanup neverclaim support. - - * src/neverclaimparse/: Shorthen as ... - * src/neverparse/:... this. - * src/Makefile.am: Adjust, and add back the directories mistakenly - removed by previous patch. - * README: Adjust, and keep the file's width under 80 columns. - * configure.ac: Adjust. - * src/neverparse/Makefile.am, src/neverparse/fmterror.cc, - src/neverparse/neverclaimparse.yy, - src/neverparse/neverclaimscan.ll, src/neverparse/public.hh: - Fix copyright. - * src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread. - * src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim. - * src/tgbatest/readneverclaim.cc: Delete. - * src/tgbatest/neverclaimread.test: Use ltl2tgba instead of - neverclaimread. - -2010-05-25 Felix Abecassis - - Add never claim parser. - - * src/neverclaimparse/: New directory. - * src/neverclaimparse/fmterror.cc: New file. Print a formatted parse - error on a output stream. - * src/neverclaimparse/neverclaimparse.yy: New file. Parser declaration - for Bison. - * src/neverclaimparse/neverclaimscan.ll: New file. Scanner declaration - for Flex. - * src/neverclaimparse/public.hh: New file. Public header for external - use. - * src/neverclaimparse/parsedecl.hh: New file. Header file for - Flex-Bison interaction. - * src/neverclaimparse/Makefile.am: New Makefile. - * src/tgbatest/neverclaimread.cc: New file. Test program for the - never claim parser. - * src/tgbatest/neverclaimread.test: New file. Test script for the - never claim parser. - * src/tgbatest/Makefile.am: Adjust. - * configure.ac : Adjust. - * README: Adjust. - -2010-11-06 Alexandre Duret-Lutz - - Remove `readsave' and fix line numbers in tgbaparse error messages. - - * src/tgbaparse/tgbaparse.yy (line): Fix computation of line number - for error messages when parsing conditions. - * src/tgbatest/readsave.test: Check the syntax position of syntax errors - in the diagnostics. Use ltl2tgba instead of readsave. - * src/tgbatest/Makefile.am (check_PROGRAMS): Remove readsave. - -2010-11-06 Alexandre Duret-Lutz - - * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.5. - -2010-10-07 Alexandre Duret-Lutz - - * configure.ac: Do not run CF_GXX_WARNINGS unless they are enabled. - -2010-10-07 Alexandre Duret-Lutz - - Hide the safra_tree_automaton type from the public interface. - - We do that because the declaration of this type, which is local to - src/tgba/tgbasafracomplement.cc has a member in an anonymous - namespace, and some versions of g++-4.2 issue a very annoying - warning about this legitimate code. See Bug 29365 on GCC's - Bugzilla. Report by Silien Hong . - - * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not - forward declare. - (tgba_safra_complement): Use void* instead of - safra_tree_automaton*. - * src/tgba/tgbasafracomplement.cc: static_cast void* to - safra_tree_automaton* anywhere needed. - -2010-05-20 Alexandre Duret-Lutz - - Fix the --enable-optimizations check. - - * m4/gccoptim.m4: Add missing AC_LANG_PUSH/AC_LANG_POP around the - C test. It was using the C++ compiler instead... - -2010-04-16 Alexandre Duret-Lutz - - * NEWS: Typo. - -2010-04-16 Alexandre Duret-Lutz - - * NEWS, configure.ac: Bump version to 0.6a. - -2010-04-16 Alexandre Duret-Lutz - - Release Spot 0.6. - - * NEWS, configure.ac: Bump version to 0.6. - -2010-04-15 Alexandre Duret-Lutz - - Reorder recent additions to reduccmp.test. - - * src/ltltest/reduccmp.test: Reorder the test added by the - previous patches. Some are not supposed to be reduced by - reductaustr. - -2010-04-15 Alexandre Duret-Lutz - - Fix a long-standing bug in the stronger rule for R and its recent - clone for M. - - * src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove - the stronger rules for R and M. They were wrong. - * src/ltltest/reduccmp.test: Test a simpple counterexample. - -2010-04-15 Alexandre Duret-Lutz - - More simplifications rules for M. - - * src/ltlvisit/reduce.cc (reduce_visitor): Add the following - implication rewriting rules: - a M (b M c) = a M c if a implies b. - a M (b R c) = a M c if a implies b. - a R (b R c) = a R c if a implies b. - a R (b M c) = b M c if b implies a. - a M (b M c) = b M c if b implies a. - The latter rule was fixed from an incorrectly copied&pasted - rule for a M (b R c) = b R c if b implies a (this is wrong). - Also remove the wrong rule for a W (b U c) = b U c if a implies b. - * src/ltltest/reduccmp.test: Add more tests. - -2010-04-15 Alexandre Duret-Lutz - - Speed up syntactic_implication() for constants. - - * src/ltlvisit/syntimpl.cc (syntactic_implication): Do not - create visitors if arguments are constant. - -2010-04-15 Alexandre Duret-Lutz - - Fix simplification of "a M true" as Fa. - - * src/ltlvisit/simpfg.cc: Typo. - * src/ltltest/reduccmp.test: Add more tests. - -2010-04-15 Alexandre Duret-Lutz - - * HACKING: Bison 2.4.2 has a bugfix we rely on. - -2010-04-15 Alexandre Duret-Lutz - - * src/tgbatest/ltl2tgba.cc (syntax): Add missing black line in - help output. - -2010-04-14 Alexandre Duret-Lutz - - * NEWS: Mention W and M. - -2010-04-14 Alexandre Duret-Lutz - - More LTL reductions for W and M. - - * src/ltlvisit/basicreduce.cc: Perform the following reductions: - (a R b) | Gb = a R b - (a M b) | Gb = a R b - (a U b) & Fb = a U b - (a W b) & Fb = a U b - * src/ltltest/reduccmp.test: Test them. - -2010-04-12 Alexandre Duret-Lutz - - * wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators. - -2010-04-12 Alexandre Duret-Lutz - - More LTL reductions for W and M. - - * src/ltlvisit/basicreduce.cc: Perform the following reductions: - (a U b) & (c W b) = (a & c) U b - (a W b) & (c W b) = (a & c) W b - (a R b) | (c M b) = (a | c) R b - (a M b) | (c M b) = (a | c) M b - * src/ltltest/reduccmp.test: Test them. - -2010-04-12 Alexandre Duret-Lutz - - Add LTL reductions for strong release. - - * src/ltlvisit/basicreduce.cc: Perform the following reductions. - a R (b & F(a)) = a M b - a M (b & F(a)) = a M b - a R Fa = Fa - a M Fa = Fa - a R b & Fa = a M b - a R b & a M c = a M (b & c) - a M b & a M c = a M (b & c) - * src/ltltest/reduccmp.test: More tests. - -2010-04-12 Alexandre Duret-Lutz - - Add LTL reductions for weak until. - - * src/ltlvisit/basicreduce.cc: Perform the following reductions. - a U (b | Ga) = a W b - a W (b | Ga) = a W b - a U b | Ga = a W b - a U b | a W c = a W (b | c) - a W b | a W c = a W (b | c) - a U Ga = Ga - a W Ga = Ga - * src/ltltest/reduccmp.test: More tests. - -2010-04-07 Alexandre Duret-Lutz - - Add support for W (weak until) and M (strong release) operators. - - * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for - these new operators. - * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them. - * src/ltltest/reduccmp.test: Add new tests for W and M. - * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, - src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, - src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh, - src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc, - src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc, - src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, - src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, - src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: - Add support for W and M. - * src/tgbatest/ltl2neverclaim.test: Test never claim output - using LBTT, this is more thorough. Also we cannot use -N - any more in the spotlbtt.test. - * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL. - * src/tgbatest/ltl2neverclaim.test: Test W and M, and use - -DS instead of -N, because lbtt-translate does not want - to translate these operators for tools that masquerade as Spin. - -2010-04-12 Alexandre Duret-Lutz - - Adjust ltl2tgba.py to call scc_filter() with the "full" option as - appropriate. - - * wrap/python/spot.i (spot::scc_filter): Make it available. - * wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter. - Use the "full" option unless the show_degen_png or - show_never_claim are set. Also reduce_scc the default. - -2010-04-08 Alexandre Duret-Lutz - - * src/ltlvisit/basicreduce.cc: Typo in comment. - -2010-04-08 Alexandre Duret-Lutz - - * NEWS: Summarize recent noteworthy changes. - -2010-04-07 Alexandre Duret-Lutz - - Modernize Bison parsers. - - * src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy, - src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use - token types for %destructor and %printer. Remove the yylex hack, - since %name-prefix is now honored by Bison. Also remove the - useless type. Suggested by Akim Demaille. - -2010-03-10 Alexandre Duret-Lutz - - Fix column in LTL error messages, it was off by one. - - * src/ltlparse/fmterror.cc (format_parse_errors): Count columns - starting at 1. Older Bison used to start at 0 but changed to - match the GNU Coding Standards. - * src/ltltest/parseerr.test: Add a test case. - -2010-03-07 Alexandre Duret-Lutz - - Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful. - - * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse): - Disable this rule unconditionally. - * src/ltltest/reduccmp.test: Adjust tests. - -2010-03-06 Alexandre Duret-Lutz - - * src/tgba/tgbatba.cc: Fix English in comments. - -2010-03-06 Alexandre Duret-Lutz - - Reverse the order of expected acceptance conditions in - degeneralization. - - * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the - list of acceptance condition in the reverse order. The order is - still arbitrary, but the bdd_satone() call seems to output the - acceptance conditions that are more used first, and this helps the - degeneralization process. - -2010-03-06 Alexandre Duret-Lutz - - Tweak precedence of "->" and <->. - - * src/ltlparse/ltlparse.yy: Change the precedence of "->" and - "<->" so that "a & b -> c" is interpreted as "(a & b) -> c" - instead of "a & (b -> c)". The new interpretation is more - intuitive, and matches that of LBTT. - -2010-03-06 Alexandre Duret-Lutz - - * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the - original paper by Somenzi and Bloem. Reported by Ruediger Ehlers. - -2010-03-06 Alexandre Duret-Lutz - - Fix memory leak introduced in yesterday's change. - - * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Do not - forget to free the initial state after usage. - -2010-03-06 Alexandre Duret-Lutz - - Keep acceptance conditions on transitions going to accepting SCCs - by default in scc_filter(). - - Doing so helps the degeneralization algorithm, because it will - have more opportunity to be in an accepting level when it reaches - the accepting SCCs. - - * src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a - remove_all_useless argument. - (filter_iter::process_link): Use the flag to decide whether to - filter acceptance conditions going to accepting SCCs. - (scc_filter): Take a remove_all_useless argument and pass it to - filter_iter. - * src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument - and document the function. - * src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3 - for remove_all_useless=false and add -R3f for - remove_all_useless=true. - * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes - the degeneralization worse than -R3. - -2010-03-05 Alexandre Duret-Lutz - - Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). - - * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace - the FG(a)|FG(b) == F(Ga|Gb) rule by the above more generic one. - Add the dual rule for G(a)&G(b), as we had none (this one won't - improve anything in the translation, but it is more symmetric - this way). Also simplify some pointer checks. - -2010-03-05 Alexandre Duret-Lutz - - Better selection of the acceptance of the initial state in SBA. - - * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set - cycle_start_ to start in the accepting layer of the degeneralized - automaton if the initial state has an accepting self-loop. - Otherwise, starts at the level of the first acceptance condition - as previously. - (tgba_sba_proxy::get_init_state): Use cycle_start_. - * src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so - that we can use it in tgba_sba_proxy::tgba_sba_proxy. - (tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state): - Declare. - * src/tgbatest/ltl2tgba.test: More tests. - -2010-03-05 Alexandre Duret-Lutz - - Generalize the previous patch to accepting states in SBA. - - * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move - the optimization step added by the previous patch outside the - before the bddtrue check, so that it also applies to accepting - states in SBA. - -2010-03-03 Alexandre Duret-Lutz - - Optimize tgba_tba_proxy and tgba_sba_proxy for states that share - an acceptance condition on all outgoing transitions. - - This was motivated by experiments from Rüdiger Ehlers, showing - that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a - U (b U c)'". With this change and the previous one, it is no - longer the case. - - * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store - a pointer to the source automaton and... - (tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra - optimization step to gather the acceptance conditions common - to all outgoing transitions of the destination state, and pretend - they are on the current (ingoing) transition. - (tgba_tba_proxy::succ_iter): Pass the - source automaton to the constructed iterator. - * src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7. - * src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'. - -2010-03-03 Alexandre Duret-Lutz - - ltl2tgba: apply -R3 before -D or -DS. - - * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the - degeneralization, because it might remove useless acceptance - conditions. I realized this while looking at experiments from - Rüdiger Ehlers. - -2010-02-24 Alexandre Duret-Lutz - - * src/sanity/style.test: Better fix for the previous error. - -2010-02-23 Alexandre Duret-Lutz - - Work around a spurious style.test error. - - * src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi - is the BibTex entry used as comment, because some version of sed - will choke on non-ascii character and cause sanity/style.test to - fail. - -2010-02-23 Alexandre Duret-Lutz - - Fix random_graph() not to generate dead states. - - This is actually the third time I fix random_graph(). On - 2007-02-06 I changed the function not to generated dead states, - but in a way that made it non-deterministic. On 2010-01-20 I made - the function deterministic again, but it started to generate dead - states as a side effect. This time, I'm making sure that dead - states won't come again with a test-case that we should have had - from the beginning. - - * src/tgbaalgos/randomgraph.cc (random_graph): Add an extra - indirection array, state_randomizer[], so that we can reorder - states indices after a random selection without actually changing - the value of the indices used by unreachable_states and - nodes_to_process. - * src/tgbatest/randtgba.test: New file. - * src/tgbatest/Makefile.am: Add randtgba.test. - -2010-02-17 Alexandre Duret-Lutz - - ltl2tgba cgi updates. - - * wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by - configure. - (os.system): Cleanup stale files only when the form has been - submitted. - (list options): Keep track of the selected value. - (draw_acc_run|print_acc_run): set ec=0 to detect if it has been - later set or not. Fix error message when using generalized - automata with degeneralized emptiness checks. - * wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@. - -2010-02-02 Alexandre Duret-Lutz - - * wrap/python/cgi-bin/ltl2tgba.in: Reword description of svg_output. - -2010-02-02 Alexandre Duret-Lutz - - Add SVG output and language containment options to the cgi script. - - * wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new. - (svg_output, reduce_langcout): Add these new options. - (render_dot): Support svg_output. - -2010-02-02 Alexandre Duret-Lutz - - * NEWS: Typo. - -2010-02-01 Alexandre Duret-Lutz - - * NEWS, configure.ac: Bump version to 0.5a. - -2010-02-01 Alexandre Duret-Lutz - - Release Spot 0.5. - - * NEWS, configure.in: Bump version to 0.5. - -2010-01-31 Alexandre Duret-Lutz - - * doc/Makefile.am ($(srcdir)/stamp): Do not depend on dot - explicitly, otherwise the documentation is always built and - distcheck fails. - -2010-01-31 Alexandre Duret-Lutz - - More Doxygen fixes. - - * src/sabaalgos/sabareachiter.hh (process_link): Document argument SI. - * src/eltlparse/public.hh (format_parse_errors): Remove the - non-existing eltl_string argument from the description. - (parse_file): Fix name of parameters in documentation. - -2010-01-31 Alexandre Duret-Lutz - - Build doxygen pictures with libgd to reduce their size. - - Doxygen only knows how to call dot with -Tpng, while using - -Tpng:gd produces pictures that are 10 times smaller. Use a - simple wrapper around dot to simplify this. - - * doc/dot.in: New file, that wrap the system's dot and replace - -Tpng by -Tpng:gd. - * doc/Makefile.am ($(srcdir)/stamp): Depend on dot. - * doc/Doxyfile.in: Update to 1.6.2. - (DOT_PATH): Set to @srcdir@ to use doc/dot instead of the - system's dot. - * configure.ac: Find the absolute path of dot, and generate - the doc/dot script. - -2010-01-31 Alexandre Duret-Lutz - - More Doxygen fixes. - - * src/tgba/tgbakvcomplement.hh: Use \verbatim around the bibtex - entry. - * src/saba/sabacomplementtgba.hh: Use latin1. - -2010-01-30 Alexandre Duret-Lutz - - * bench/split-product/Makefile.am (nodist_noinst_DATA): Do not - depend on files that cannot be built. - -2010-01-30 Alexandre Duret-Lutz - - Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. - - * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these - files. - * src/tgba/Makefile.am: Remove them. - * src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New - files. - * src/ltl/ltlparse/Makefile.am: Add them. - * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite - using the new class. - -2010-01-30 Alexandre Duret-Lutz - - Check for missing Copyright blurbs, and add them. - - * src/sanity/style.test: Check for missing Copyrights blurbs. - * src/sanity/Makefile.am: Run style.test before includes.test. - * iface/gspn/dcswave.test, iface/gspn/dcswaveeltl.test, - iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test, - iface/gspn/simple.test, iface/gspn/udcsefm.test, - iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, - iface/gspn/udcsltl.test, iface/nips/nipstest/dotty.test, - iface/nips/nipstest/emptiness.test, src/eltltest/acc.test, - src/eltltest/nfa.test, src/saba/sabacomplementtgba.cc, - src/sabatest/sabacomplementtgba.cc, src/tgbatest/eltl2tgba.test, - src/tgbatest/taatgba.test: Add missing Copyright blurb. - -2010-01-30 Alexandre Duret-Lutz - - * NEWS: More text. - -2010-01-30 Alexandre Duret-Lutz - - Touch up some doxygen comments and copyrights. - - * eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh, - tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc, - tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment - changes. - -2010-01-30 Alexandre Duret-Lutz - - Add SCC pruning options to the CGI script. - - * wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically - prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting - SCCs in all algorithms. - * src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to - SWIG. - * wrap/python/spot.i: Include reductgba_sim.hh. - -2010-01-30 Alexandre Duret-Lutz - - * src/evtgbatest/ltl2evtgba.test: Replace * by &. - -2010-01-30 Alexandre Duret-Lutz - - Make it possible to use the cgi script without installing a web - server. - - * wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the - script is not called as a CGI. Arrange to load libraries from - the build directory. Create the spotimg/ if needed when run as - a web server. - * wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean - the spotimg directory. - * wrap/python/cgi-bin/README, NEWS: Update. - -2010-01-30 Alexandre Duret-Lutz - - More * -> & replacements. - - * src/ltltest/parse.test, src/ltltest/syntimpl.test: Replace * by &. - -2010-01-30 Alexandre Duret-Lutz - - Remove the theoretically bogus "containment" option of ltl2tgba_fm. - - * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: - Remove the containment option. - * src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the - containment_ member. - * src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for - FM algorithm, use it exclusively for TAA. - -2010-01-30 Alexandre Duret-Lutz - - * src/tgba/tgbasafracomplement.hh: Add missing copyright and - fix some comments. - -2010-01-30 Alexandre Duret-Lutz - - Rename tgba_complement as tgba_kv_complement. - - * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: Rename - as... - * src/tgba/tgbakvcomplement.hh, src/tgba/tgbakvcomplement.cc: - ... these. It makes more sense since we also have - tgba_safra_complement. - * src/tgba/Makefile.am, src/tgbatest/complement.cc, NEWS: Adjust. - -2010-01-30 Alexandre Duret-Lutz - - Do not recognize "*" as "and". This leaves room for an - implementation of rational operators in a future version. - - * src/ltlparse/ltlscan.ll: Do not recognize "*". - * wrap/python/cgi-bin/ltl2tgba.in: Undocument it. - * NEWS: Mention this. - * src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test, - src/tgbatest/reductgba.test: Replace "*" by "&". - -2010-01-30 Alexandre Duret-Lutz - - Make Couvreur/FM the default translation. - - * src/tgbatest/ltl2tgba.cc (syntax, main): Do it. - * NEWS: Mention it. - * src/tgbatest/emptchk.test: Add missing -l. - -2010-01-30 Alexandre Duret-Lutz - - Overhaul LaCIM's ELTL options. - - * src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select - this algorithm and -lo to add the default LTL operators. This - replace the undocumented hack to add LTL operators when the - formula with read for command-line, or the automaton was output - for LBTT. - * src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update - call syntax. - * NEWS: Mention -le, -lo, and -taa. - -2010-01-30 Alexandre Duret-Lutz - - Touch up -R3b handling. - - * src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other - LaCIM options. - (main): Speak of "symbolic SCC pruning" instead of "deleting - unaccepting SCC", and do that right after the translation, before - degeneralization. Also error out when -R3b is used on non - symbolic automata. - -2010-01-29 Alexandre Duret-Lutz - - Update some text files for upcoming 0.5. - - * NEWS: Update for upcoming 0.5. - * HACKING: Update Automake requirement. - * README: Mention the mailing list. - * bench/ltlcounter/README: More text. - * configure.ac: Report bugs to spot@lrde.epita.fr. - -2010-01-29 Alexandre Duret-Lutz - - Rename wrap/python/cgi/ as wrap/python/cgi-bin/. - - * wrap/python/cgi/: Rename as ... - * wrap/python/cgi-bin/: ... this. - * configure.ac, spot/wrap/python/Makefile.am, README: Adjust. - -2010-01-29 Alexandre Duret-Lutz - - * src/tgbaalgos/gtec/gtec.hh: Fix copyright. - -2010-01-29 Felix Abecassis - - * src/tgba/taatgba.cc, src/tgba/taatbga.hh: Fix a memory issue on - Darwin. - -2010-01-25 Damien Lefortier - - * wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new - translation algorithm: Tauriainen/TAA. - -2010-01-25 Damien Lefortier - - * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead - of the UNIQUE_ID environment variable to avoid being - Apache-specific. - -2010-01-24 Guillaume Sadegh - - Fix copyrights. - - * bench/Makefile.am, bench/gspn-ssp/Makefile.am, - bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am, - bench/split-product/Makefile.am, configure.ac, - iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh, - iface/nips/Makefile.am, iface/nips/common.cc, - iface/nips/common.hh, iface/nips/dottynips.cc, - iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am, - src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy, - src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc, - src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am, - src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh, - src/evtgba/product.cc, src/evtgba/product.hh, - src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am, - src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in, - src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc, - src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc, - src/evtgbatest/product.test, src/evtgbatest/readsave.cc, - src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc, - src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, - src/ltlast/binop.hh, src/ltlast/constant.cc, - src/ltlast/constant.hh, src/ltlast/formula.cc, - src/ltlast/formula.hh, src/ltlast/formula_tree.cc, - src/ltlast/formula_tree.hh, src/ltlast/multop.cc, - src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh, - src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc, - src/ltlenv/declenv.hh, src/ltlenv/environment.hh, - src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy, - src/ltltest/Makefile.am, src/ltltest/defs.in, - src/ltltest/equals.cc, src/ltltest/equals.test, - src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, - src/ltltest/parse.test, src/ltltest/parseerr.test, - src/ltltest/randltl.cc, src/ltltest/readltl.cc, - src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc, - src/ltltest/syntimpl.test, src/ltltest/tostring.cc, - src/ltltest/tostring.test, src/ltltest/tunabbrev.test, - src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc, - src/ltlvisit/clone.cc, src/ltlvisit/clone.hh, - src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc, - src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc, - src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc, - src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, - src/ltlvisit/tostring.cc, src/misc/bddalloc.cc, - src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh, - src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh, - src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh, - src/saba/Makefile.am, src/saba/explicitstateconjunction.cc, - src/saba/explicitstateconjunction.hh, src/saba/saba.cc, - src/saba/saba.hh, src/saba/sabacomplementtgba.cc, - src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh, - src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am, - src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh, - src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh, - src/sabatest/Makefile.am, src/sabatest/defs.in, - src/sanity/Makefile.am, src/tgba/Makefile.am, - src/tgba/bdddict.cc, src/tgba/bddprint.cc, - src/tgba/formula2bdd.cc, src/tgba/state.hh, - src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh, - src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc, - src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc, - src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc, - src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc, - src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, - src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, - src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, - src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc, - src/tgbaalgos/eltl2tgba_lacim.cc, - src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc, - src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc, - src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc, - src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, - src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc, - src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc, - src/tgbaalgos/reductgba_sim.hh, - src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc, - src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am, - src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am, - src/tgbatest/bddprod.test, src/tgbatest/complementation.cc, - src/tgbatest/complementation.test, src/tgbatest/defs.in, - src/tgbatest/dfs.test, src/tgbatest/dupexp.test, - src/tgbatest/explicit.cc, src/tgbatest/explicit.test, - src/tgbatest/explpro3.test, src/tgbatest/explpro4.test, - src/tgbatest/explprod.cc, src/tgbatest/explprod.test, - src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc, - src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc, - src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc, - src/tgbatest/mixprod.test, src/tgbatest/powerset.cc, - src/tgbatest/readsave.cc, src/tgbatest/readsave.test, - src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc, - src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc, - src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test, - src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test, - wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py, - wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: - Fix copyrights. - -2010-01-24 Alexandre Duret-Lutz - - * src/tgbaalgos/ltl2tgba_fm.cc: More comments. - -2010-01-24 Alexandre Duret-Lutz - - Check that all directories are documented. - - * 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. - -2010-01-24 Alexandre Duret-Lutz - - * README: Typo. - -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 lot 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