We are pleased to announce the release of Spot 1.0.1.
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 maintainance release mainly addresses a couple of minor bugs
uncovered in the last three months, and prunes some old code. The
main change is probably that LBTT has been removed from the
distribution, as promised in the previous release notes.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.0.1.tar.gz
A summary of the changes follows. Please report any issue
to <spot(a)lrde.epita.fr>.
New in spot 1.0.1 (2013-01-23):
* Bug fixes:
- Two executions of the simulation reductions could produce
two isomorphic automata, but with transitions in a different
order.
- ltlcross did not diagnose write errors to temporary files,
and certain versions of g++ would warn about it.
- "P0.init" is parsed as an atomic even without the double quotes,
but it was always output with double quotes. This version will
not quote this atomic proposition anymore.
- "U", "W", "M", "R" were correctly parsed as atomic propositions
(instead of binary operators) when placed in double quotes, but
on output they were output without quotes, making the result
unparsable.
- the to_lbt_string() functions would always output a trailing space.
This is not the case anymore.
- tgba_product::transition_annotation() would segfault when
called in a product against a Kripke structure.
* Minor improvements:
- Four new LTL simplifications rules:
GF(a|Xb) = GF(a|b)
GF(a|Fb) = GF(a|b)
FG(a&Xb) = FG(a&b)
FG(a&Gb) = FG(a&b)
- The on-line version of ltl2tgba now displays edge and
transition counts, just as the ltlcross tool.
- ltlcross will display the number of timeouts at the end
of its execution.
- ltlcross will diagnose tools with missing input or
output %-sequence before attempting to run any of them.
- The parser for LBT's prefix-style LTL formulas will now
read atomic propositions that are not of the form p1, p2...
This makes it possible to process formulas written in
ltl2dstar's syntax.
* Pruning:
- lbtt has been removed from the distribution. A copy of the last
version we distributed is still available at
http://spot.lip6.fr/dl/lbtt-1.2.1a.tar.gz
and our test suite will use it if it is installed, but the same
tests are already performed by ltlcross.
- the bench/ltl2tgba/ benchmark, that used lbtt to compare various
LTL-to-Büchi translators, has been updated to use ltlcross. It
now output summary tables in LaTeX. Support for Modella (no
longer available online), and Wring (requires a too old Perl
version) have been dropped.
- the half-baked and underdocumented "Event TGBA" support in
src/evtgba*/ has been removed, as it was last worked on in 2004.
