This maintenance release fixes a couple of translation bugs, and adds
several small utility features to the command-line and online tools.
Special thanks to Joachim Klein for some useful suggestions.
Unless some serious bugs are reported, this is likely to be the last
release of Spot 1.2. The current development version of Spot, which
will probably released as Spot 2.0 next year, is so much ahead of this
code base that maintaining this version is starting to be a burden.
By the way, I should probably issue a friendly warning to those using
Spot as a C++ library: the changes in version 2.0 will be big enough
so that there is no way to maintain compatibility with code written
for the current version. It will require changes to existing code,
the first of which being to switch to C++11. (Spot 1.2.5 should
compile fine with C++11, so you can already make that switch.)
You can download the new release here:
http://spot.lip6.fr/dl/spot-1.2.5.tar.gz
New in spot 1.2.5 (2014-08-21)
* New features:
- The online ltl2tgba translator will automatically attempt to
parse a formula using LBT's syntax if it cannot parse it using
the normal infix syntax. It also has an option to display
formulas using LBT's syntax.
- ltl2tgba and dstar2tgba have a new experimental option --hoaf to
output automata in the Hanoï Omega Automaton Format whose
current draft is at http://adl.github.io/hoaf/
The corresponding C++ function is spot::hoaf_reachable() in
tgbaalgos/hoaf.hh.
- 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'.
- ltlcross has a new option --save-bogus=FILENAME to save any
formula for which a problem (other than timeout) was detected
during translation or using the resulting automatas.
* Documentation:
- The man page for ltl2tgba has some new notes and references
about TGBA and about monitors.
* Bug fixes:
- Fix incorrect simplification of promises in the translation
of the M operator (you may suffer from the bug even if you do
not use this operator as some LTL patterns are automatically
reduced to it).
- Fix simplification of bounded repetition in SERE formulas.
- Fix incorrect translation of PSL formulas of the form !{f} where
f is unsatisifable. A similar bug was fixed for {f} in Spot
1.1.4, but for some reason it was not fixed for !{f}.
- Fix parsing of neverclaims produced by Modella.
- Fix a memory leak in the little-used conversion from
transition-based alternating automata to tgba.
- Fix a harmless uninitialized read in BuDDy.
- When writing to the terminal, ltlcross used to display each
formula in bright white, to make them stand out. It turns out
this was actually hiding the formulas for people using a
terminal with white background... This version displays formula
in bright blue instead.
- 'randltl -n -1 --seed 0' and 'randltl -n -1 --seed 1' used to
generate nearly the same list of formulas, shifted by one,
because the PRNG write reset with an incremented seed between
each output formula. The PRNG is now reset only once.
--
Alexandre Duret-Lutz
