Spot 0.5 has been released - Spot-announce

1 Feb 2010

We're pleased to announce the release of Spot 0.5.

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 includes more than two year of work, with contributions
from Damien Lefortier, Guillaume Sadegh, Félix Abecassis, and
Alexandre Duret-Lutz.  We would also like to thank Akim Demaille,
Denis Poitrenaud, and Kristin Y. Rozier for their bug reports and
help.

You can find the new release here:

  http://spot.lip6.fr/dl/spot-0.5.tar.gz

Before listing what is new in this release, let me mention that we
have setup two mailing lists so you can stay informed, or discuss spot:

  - &lt;spot-announce(a)lrde.epita.fr&gt; is read-only and will be used to
    announce new releases.  You may subscribe at
    https://www.lrde.epita.fr/mailman/listinfo/spot-announce

  - &lt;spot(a)lrde.epita.fr&gt; can be used to discuss anything related to
    Spot.  You may subscribe at
    https://www.lrde.epita.fr/mailman/listinfo/spot-announce

What is new in spot 0.5 (2010-02-01):

  * Two new LTL translations have been implemented:
    - eltl_to_tgba_lacim() is a symbolic translation for ELTL based on
      Couvreur's LaCIM'00 paper.  For this translation (available with
      ltl2tgba's option -le), all operators are described as finite
      automata.  A default set of operators is provided for LTL
      (option -lo) and user may add more automaton operators.
    - ltl_to_taa() is a translation based on Tauriainen's PhD thesis.
      LTL is translated to "self-loop" alternating automata
      and then to Transition-based Generalized Automata.  (ltl2tgba's
      option -taa).
    The "Couvreur/FM" translation remains the best LTL translation
    available in Spot.
  * The data structures used to represent LTL formulae have been
    overhauled, and it resulted in a big performence improvement
    (in time and memory consumption) for the LTL translation.
  * Two complementation algorithms for state-based Büchi automata
    have been implemented:
    - tgba_kv_complement is an on-the-fly implementation of the
      Kupferman-Vardi construction (TCS'05) for generalized acceptance
      conditions.
    - tgba_safra_complement is an implementation of Safra's
      complementation.  This algorithm takes a degeneralized Büchi
      automaton as input, but our implementation for the Streett->Büchi
      step will produce a generalized automaton in the end.
  * ltl2tgba has gained several options and the help text has been
    reorganized.  Please run src/tgbatest/ltl2tgba without arguments
    for details.  Couvreur/FM is now the default translation.
  * The ltl2tgba.py CGI script can now run standalone.  It also offers
    the Tauriainen/TAA translation, and some options for SCC-based
    reductions.
  * Automata using BDD-encoded transitions relation can now be pruned
    for useless states symbolically using the delete_unaccepting_scc()
    function.  This is ltl2tgba's -R3b option.
  * The SCC-based simplification (ltl2tgba's -R3 option) has been
    rewritten and improved.
  * The "*" symbol, previously parsed as a synonym for "&" is no
    longer recognized.  This makes room for an upcoming support of
    rational operators.
  * More benchmarks in the bench/ directory:
    - gspn-ssp/    some benchmarks published at ACSD'07,
    - ltlcounter/  translation of a class of LTL formulae used by
                     Rozier & Vardi at SPIN'07
    - scc-stats/   SCC statistics after translation of LTL formulae
    - split-product/ parallelizing gain after splitting LTL automata
  * An experimental Kripke interface has been developed to simplify
    the integration of third party tools that do not use acceptance
    conditions and that have label on states instead of transitions.
    This interface has not been used yet.
  * Experimental interface with the Nips virtual machine.
    It is not very useful as Spot isn't able to retrieve any property
    information from the model.  This will just check assertions.
  * Distribution:
    - The Boost C++ library is now required.
    - Update to Autoconf 2.65, Automake 1.11.1, Libtool 2.2.6b,
      Bison 2.4.1, and Swig 1.3.40.
    - Thanks to the newest Automake, "make check" will now
      run in parallel if you use "make -j2 check" or more.
  * Bug fixes:
    - Disable warnings from the garbage collection of BuDDy, it
      could break the standard output of ltl2tgba.
    - Fix several C++ constructs to ensure Spot will build with
      GCC 4.3, 4.4, and older 3.x releases, as well as with Intel's
      ICC compiler.
    - A very old bug in the hash function for LTL formulae caused Spot
      to sometimes (but very rarely) consider two different LTL formulae
      as equal.

-- 
Alexandre Duret-Lutz