We are pleased to announce the release of Spot 0.9.
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.
You can find the new release here:
http://spot.lip6.fr/dl/spot-0.9.tar.gz (11MB)
The major news in this release are all related to the
logic-to-Büchi-automaton translation engine:
1. The linear-time fragment of PSL is supported.
This first implementation, enough to experiment with the
logic, shall be improved in future versions.
(Feedback most welcome.)
2. The LTL simplification code has been overhauled and
augmented with new rules.
3. A new simulation-based post-processing can be used
to simplify the TGBA constructed.
For more details about the first two points (supported operators, and
rewritings performed), please read the file doc/tl/tl.pdf included in
spot-0.9.tar.gz.
A consequence of the last two points is that Spot 0.9 is faster than
Spot 0.8.3 and can produce even smaller automata. For some
comparative benchmarks, please download
http://spot.lip6.fr/dl/bench-0.9.pdf
Please direct any feedback and questions to <spot(a)lrde.epita.fr>.
(Subscribe at https://www.lrde.epita.fr/mailman/listinfo/spot if you wish.)
A more detailed list of new features follows.
New in spot 0.9 (2012-05-09):
* New features:
- Operators from the linear fragment of PSL are supported. This
basically extends LTL with Sequential Extended Regulat
Expressions (SERE), and a couple of operators to bridge SERE and
LTL. See doc/tl/tl.pdf for the list of operators and their
semantics.
- Formula rewritings have been completely revamped, and augmented
with rules for PSL operators (and some new LTL rules as well).
See doc/tl/tl.pdf for the list of the rewritings implemented.
- Some of these rewritings that may produce larger formulas
(for instance to rewrite "{a;b;c}" into "a & X(b & Xc)")
may be explicitely disabled with a new option.
- The src/ltltest/randltl tool can now generate random SEREs
and random PSL formulae.
- Only one translator (ltl2tgba_fm) has been augmented to
translate the new SERE and PSL operators. The internal
translation from SERE to DFA is likely to be rewriten in a
future version.
- A new function, length_boolone(), computes the size of an
LTL/PSL formula while considering that any Boolean term has
length 1.
- The LTL/PSL parser recognizes some UTF-8 characters (like ◇ or
∧) as operators, and some output routines now have an UTF-8
output mode. Tools like randltl and ltl2tgba have gained an -8
option to enable such output. See doc/tl/tl.pdf for the list
of recognized codepoints.
- A new direct simulation reduction has been implemented. It
works directly on TGBAs. It is in src/tgbaalgos/simlation.hh,
and it can be tested via ltl2tgba's -RDS option.
- unabbreviate_wm() is a function that rewrites the W and M operators
of LTL formulae using R and U. This is called whenever we output
a formula in Spin syntax. By combining this with the aforementioned
PSL rewriting rules, many PSL formulae that use simple SERE can be
converted into LTL formulae that can be feed to tools that only
understand U and R. The web interface will let you do this.
- changes to the on-line translator:
+ SVG output is available
+ can display some properties of a formula
+ new options for direct simulation, larger rewritings, and
utf-8 output
- configure --without-included-lbtt will prevent LBTT from being
configured and built. This helps on systems (such as MinGW)
where LBTT cannot be built. The test-suite will skip any
LBTT-based test if LBTT is missing.
* Interface changes:
- Operators ->, <->, U, W, R, and M are now parsed as
right-associative to better match the PSL standard.
- The constructors for temporal formulae will perform some trivial
simplifications based on associativity, commutativity,
idempotence, and neutral elements. See doc/tl/tl.pdf for the
list of such simplifications.
- Formula instances now have many methods to inspect their
properties (membership to syntactic classes, absence of X
operator, etc...) in constant time.
- LTL/PSL formulae are now handled everywhere as 'const formula*'
and not just 'formula*'. This reflects the true nature of these
(immutable) formula objects, and cleanups a lot of code.
Unfortunately, it is a backward incompatible change: you may have
to add 'const' to a couple of lines in your code, and change
'ltl::const_vistitor' into 'ltl::visitor' if you have written a
custom visitor.
- The new entry point for LTL/PSL simplifications is the function
ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh.
The ltl_simplifier class implements a cache.
Functions such as reduce() or reduce_tau03() are deprecated.
- The old game-theory-based implementations for direct and delayed
simulation reductions have been removed. The old direct
simulation would only work on degeneralized automata, and yet
produce results inferior to the new direct simulation introduced
in this release. The implementation of delayed simulation was
unreliable. The function reduc_tgba_sim() has been kept
for compatibility (it calls the new direct simulation whatever
the type of simulation requested) and marked as deprecated.
ltl2tgba's options -Rd, -RD are gone. Options -R1t, -R1s,
-R2s, and -R2t are deprecated and all made equivalent to -RDS.
- The tgba_explicit hierarchy has been reorganized in order to
make room for sba_explicit classes that share most of the code.
The main consequence is that the tgba_explicit type no longuer
exists. However the tgba_explicit_number,
tgba_explicit_formula, and tgba_explicit_string still do.
