Spot 1.1.4 has been released.
This maintenance release fixes a couple of bugs reported over the
last weeks. These include a regression preventing 1.1.3 to parse
neverclaims produced by ltl2ba or ltl3ba, and a bug in the
interpretation of the closure of some SERE.
You can download the new release here:
http://spot.lip6.fr/dl/spot-1.1.4.tar.gz
New in spot 1.1.4 (2013-07-29)
* Bug fixes:
- The parser for neverclaim, updated in 1.1.3, would fail to
parse guards of the form (a) || (b) output by ltl2ba or
ltl3ba, and would only understand ((a) || (b)).
- When used from ltlcross, the same parser would fail to
parse further neverclaims after the first failure.
- Add a missing newline in some error message of ltlcross.
- Expressions like {SERE} were wrongly translated and simplified
for SEREs that accept the empty word: they were wrongly reduced
to true. Simplification and translation rules have been fixed,
and the doc/tl/tl.pdf specifications have been updated to better
explain that {SERE} has the semantics of a closure operator that
is not exactly what one could expect after reading the PSL
standard.
- Various typos.
--
Alexandre Duret-Lutz (off for three weeks)
I'm pleased to announce the release of Spot 1.1.3.
This maintenance release fixes a couple of bugs reported over the
last month, and add support for reading the new neverclaims output by
Spin 6.24+ (they can be parsed by ltlcross, for instance).
You can download the new release here:
http://spot.lip6.fr/dl/spot-1.1.3.tar.gz
New in spot 1.1.3 (2013-07-09)
* New feature:
- The neverclaim parser now understands the new style of output
used by Spin 6.24 and later.
* Bug fixes:
- The scc_filter() function could abort with a BDD error. If all
the acceptance sets of an SCC but the first one were useless.
- The script in bench/spin13/ would not work on MacOS X because
of some non-portable command.
- A memory corruption in ltlcross.
--
Alexandre Duret-Lutz