16 Apr
2010
16 Apr
'10
2:05 p.m.
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