We are pleased to announce the release of Spot 0.6.
Spot is a model-checking library developed collaboratively by LRDE and
LIP6. It provides algorithms and data structures to implement the
automata-theoretic approach to LTL model checking.
This release adds support for W (weak until) and M (strong release)
LTL operators, it also improves LTL rewriting rules as well as the
degeneralization algorithm. The result is that a lot of LTL formulae
from our benchmark are translated to smaller automata, and the
reduction is even more important when producing never claims.
You can find the new release here:
http://spot.lip6.fr/dl/spot-0.6.tar.gz
New in spot 0.6 (16-04-2010):
* Several optimizations to improve some auxiliary steps
of the LTL translation (not the core of the translation):
- Better degeneralization
- SCC simplifications has been tuned for degeneralization
(ltl2tgba now has two options -R3 and -R3f: the latter will
remove every acceptance condition that used to be removed
in Spot 0.5 while the former will leave useless acceptance conditions
going to accepting SCC. Experience shows that -R3 is more
favorable to degeneralization).
- ltl2tgba will perform SCC optimizations before degeneralization
and not the converse
- We added a syntactic simplification rule to rewrite F(a)|F(b) as F(a|b).
We only had a rule for the more specific FG(a)|FG(b) = F(Ga|Gb).
- The syntactic simplification rule for F(a&GF(b)) = F(a)&GF(b) has
be disabled because the latter formula is in fact harder to translate
efficiently.
* New LTL operators: W (weak until) and its dual M (strong release)
- Weak until allows many LTL specification to be specified more
compactly.
- All LTL translation algorithms have been updated to
support these operators.
- Although they do not add any expressive power, translating
"a W b" is more efficient (read smaller output automaton) than
translating the equivalent form using the U operator.
- Basic syntactic rewriting rules will automatically rewrite "a U
(b | G(a))" and "(a U b)|G(a)" as "a W b", so you will benefit
from the new operators even if you do not use them. Similar
rewriting rules exist for R and M, although they are less used.
* New options have been added to the CGI script for
- SVG output
- SCC simplifications
* Bug fixes:
- The precedence of the "->" and "<->" Boolean operators has been
adjusted to better match other tools.
Spot <= 0.5 used to parse "a & b -> c & d" as "a & (b -> c) & d";
Spot >= 0.6 will parse it as "(a & b) -> (c & d)".
- The random graph generator was fixed (again!) not to produce
dead states as documented.
- Locations in the error messages of the LTL parser were off by one.
--
Alexandre Duret-Lutz
We're pleased to announce the release of Spot 0.5.
Spot is a model-checking library developed collaboratively
by LRDE and LIP6. It provides algorithms and data structures
to implement the automata-theoretic approach to LTL model
checking.
This release includes more than two year of work, with contributions
from Damien Lefortier, Guillaume Sadegh, Félix Abecassis, and
Alexandre Duret-Lutz. We would also like to thank Akim Demaille,
Denis Poitrenaud, and Kristin Y. Rozier for their bug reports and
help.
You can find the new release here:
http://spot.lip6.fr/dl/spot-0.5.tar.gz
Before listing what is new in this release, let me mention that we
have setup two mailing lists so you can stay informed, or discuss spot:
- <spot-announce(a)lrde.epita.fr> is read-only and will be used to
announce new releases. You may subscribe at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
- <spot(a)lrde.epita.fr> can be used to discuss anything related to
Spot. You may subscribe at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
What is new in spot 0.5 (2010-02-01):
* 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 (available with
ltl2tgba's option -le), all operators are described as finite
automata. A default set of operators is provided for LTL
(option -lo) 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. (ltl2tgba's
option -taa).
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_kv_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. Couvreur/FM is now the default translation.
* The ltl2tgba.py CGI script can now run standalone. It also offers
the Tauriainen/TAA translation, and some options for SCC-based
reductions.
* 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.
* The "*" symbol, previously parsed as a synonym for "&" is no
longer recognized. This makes room for an upcoming support of
rational operators.
* More benchmarks in the bench/ directory:
- 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.
--
Alexandre Duret-Lutz
