Commit c00a80a2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
* Report bugs to
parent 7d5f493f
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.
* Report bugs to
2010-01-29 Alexandre Duret-Lutz <>
Rename wrap/python/cgi/ as wrap/python/cgi-bin/.
......@@ -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
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
- <> can be used to discusse anything related
to Spot. You may subscribe at
* 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
- 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):
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 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
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. 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.
......@@ -22,7 +22,7 @@
# 02111-1307, USA.
AC_INIT([spot], [0.4a])
AC_INIT([spot], [0.4a], [])
AM_INIT_AUTOMAKE([1.11 gnits nostdinc tar-ustar color-tests parallel-tests])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment