We are pleased to announce the release of Spot 0.7.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 is a quick maintenance release mainly to fix some configuration problem if you already had a previous version of Spot installed, and to address a more serious bug in WDBA minimization.

We have also integrated some minor features that should ease comparisons with the Büchi Store. But beware: the Büchi Store (and Goal) uses right-associativity for operators "W", "U", and "R", while Spot applies left-associativity. A formula like "p W q U r" will be interpreted differently. We will probably switch to right-associativity in a future version in order to get closer to the PSL standard.

You can find the new release here:

http://spot.lip6.fr/dl/spot-0.7.1.tar.gz (14MB)

New in spot 0.7.1 (2001-02-07):

* The LTL parser will accept operator ~ (for not) as well as --> and <--> (for implication and equivalence), allowing formulae from the Büchi Store to be read directly. * The neverclaim parser will accept guards of the form :: !(...) -> goto ... instead of the more commonly used :: (!(...)) -> goto ... This makes it possible to read neverclaims provided by the Büchi Store. * A new ltl2tgba option, -kt, will count the number of "sub-transitions". I.e., a transition labelled by "true" counts for 4 "sub-transitions" if the automaton uses 2 atomic propositions. * Bugs fixed: - Fix segfault during WDBA minimization on automata with useless states. - Use the included BuDDy library if the one already installed is older than the one distributed with Spot 0.7. - Fix two typos in the code of the CGI scripts.