diff --git a/ChangeLog b/ChangeLog index d03bc0aa5..28029f610 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +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/. diff --git a/HACKING b/HACKING index d3138544c..118e4c293 100644 --- a/HACKING +++ b/HACKING @@ -10,7 +10,7 @@ Here are the tools you need to bootstrap the CVS tree, or more generally if you plan to regenerate some of the generated files. GNU Autoconf >= 2.61 - GNU Automake >= 1.10 + GNU Automake >= 1.11 GNU Libtool >= 2.2 GNU Flex (the version seems to matters, we used 2.5.31) GNU Bison >= 2.4 diff --git a/NEWS b/NEWS index ed21d5d2f..2b961ee83 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,70 @@ -New in spot 0.4a: +New in spot 0.5 (2010-01-31): + + * We have setup two mailing lists: + - is read-only and will be used to + announce new releases. You may subscribe at + https://www.lrde.epita.fr/mailman/listinfo/spot-announce + - can be used to discusse anything related + to Spot. You may subscribe at + https://www.lrde.epita.fr/mailman/listinfo/spot-announce + * Two new LTL translations have been implemented: + - eltl_to_tgba_lacim() is a symbolic translation for ELTL based + on Couvreur's LaCIM'00 paper. For this translation, all operators + are described as finite automata. A default set of operators is + provided for LTL and user may add more automaton operators. + - ltl_to_taa() is a translation based on Tauriainen's PhD thesis. + LTL is translated to "self-loop" alternating automata + and then to Transition-based Generalized Automata. + The "Couvreur/FM" translation remains the best LTL translation + available in Spot. + * The data structures used to represent LTL formulae have been + overhauled, and it resulted in a big performence improvement + (in time and memory consumption) for the LTL translation. + * Two complementation algorithms for state-based Büchi automata + have been implemented: + - tgba_complement is an on-the-fly implementation of the + Kupferman-Vardi construction (TCS'05) for generalized acceptance + conditions. + - tgba_safra_complement is an implementation of Safra's + complementation. This algorithm takes a degeneralized Büchi + automaton as input, but our implementation for the Streett->Büchi + step will produce a generalized automaton in the end. + * ltl2tgba has gained several options and the help text has been + reorganized. Please run src/tgbatest/ltl2tgba without arguments + for details. + * Automata using BDD-encoded transitions relation can now be pruned + for useless states symbolically using the delete_unaccepting_scc() + function. This is ltl2tgba's -R3b option. + * The SCC-based simplification (ltl2tgba's -R3 option) has been + rewritten and improved. + * More benchmarks: + - gspn-ssp/ some benchmarks published at ACSD'07, + - ltlcounter/ translation of a class of LTL formulae used by + Rozier & Vardi at SPIN'07 + - scc-stats/ SCC statistics after translation of LTL formulae + - split-product/ parallelizing gain after splitting LTL automata + * An experimental Kripke interface has been developed to simplify + the integration of third party tools that do not use acceptance + conditions, and that have label on states instead of transitions. + This interface has not been used yet. + * Experimental Interface with the Nips virtual machine. + It is not very useful as Spot isn't able to retrieve any property + information from the model. This will just check assertions. + * Distribution: + - The Boost C++ library is now required. + - Update to Autoconf 2.65, Automake 1.11.1, Libtool 2.2.6b, + Bison 2.4.1, and Swig 1.3.40. + - Thanks to the newest Automake, "make check" will now + run in parallel if you use "make -j2 check" or more. + * Bug fixes: + - Disable warnings from the garbage collection of BuDDy, it + could break the standard output of ltl2tgba. + - Fix several C++ constructs to ensure Spot will build with + GCC 4.3, 4.4, and older 3.x releases, as well as with Intel's + ICC compiler. + - A very old bug in the hash function for LTL formulae caused Spot + to sometimes (but very rarely) consider two different LTL formulae + as equal. New in spot 0.4 (2007-07-17): diff --git a/README b/README index f4b30f016..e00bd2430 100644 --- a/README +++ b/README @@ -1,3 +1,16 @@ +Keeping in touch +================ + +If you have questions regarding Spot, a bug reports, please send them +to . This is a public mailing list which you may +subscribe to at https://www.lrde.epita.fr/mailman/listinfo/spot but you +should feel free to post without subscribing. + +We also run an extremely low traffic list for announcements of +new releases of Spot. You may subscribe to that list at +https://www.lrde.epita.fr/mailman/listinfo/spot-announce + + Installation ============ diff --git a/bench/ltlcounter/README b/bench/ltlcounter/README index 83cc30f50..866cc4c61 100644 --- a/bench/ltlcounter/README +++ b/bench/ltlcounter/README @@ -1,6 +1,22 @@ +In the following paper by Rozier & Vardi, a class of LTL formula +describing counters was used to stress many translators. + +@InProceedings{ rozier.07.spin, + author = {Kristin Y. Rozier and Moshe Y. Vardi}, + title = {LTL Satisfiability Checking}, + booktitle = {Proc. the 12th International SPIN Workshop on + Model Checking of Software (SPIN'07)}, + pages = {149--167}, + year = {2007}, + volume = {4595}, + series = {LNCS}, + publisher = {Springer-Verlag} +} + This benchmark uses the ltlcounter scripts of Kristin Y. Rozier (See src/tgbatest/ltlcounter/) to plot the performance of the ltl2tgba_fm -algorithm. +algorithm. Studying the behaviour of ltl2tgba_fm on this class of +formulae helped us to improve the translation. Execute "./run" to compute the raw numbers, then execture "gnuplot plot.gnu" to plot the figures. diff --git a/configure.ac b/configure.ac index 5c789af93..ecff7c2a0 100644 --- a/configure.ac +++ b/configure.ac @@ -22,7 +22,7 @@ # 02111-1307, USA. AC_PREREQ([2.61]) -AC_INIT([spot], [0.4a]) +AC_INIT([spot], [0.4a], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnits nostdinc tar-ustar color-tests parallel-tests])