Spot 0.9.1 released - Spot-announce

23 May 2012


      We are pleased to announce the release of Spot 0.9.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 maintenance release fixes a couple of bugs, and improves the
speed of the translation slightly.
You can find the new release here:
http://spot.lip6.fr/dl/spot-0.9.1.tar.gz
An updated version of the translation benchmark has been put here:
http://spot.lip6.fr/dl/bench-0.9.1.pdf
New in spot 0.9.1 (2012-05-23):
* The version of LBTT we distribute includes a patch from Tomáš
    Babiak to count the number of non-deterministic states, and the
    number of deterministic automata produced.
    See lbtt/NEWS for the list of other differences with the original
    version of LBTT 1.2.1.
  * The Couvreur/FM translator has learned two new tricks.  These only
    help to speedup the translation by not issuing states or
    acceptance conditions that would be latter suppresed by other
    optimizations.
    - The translation rules used to translate subformulae of the G
      operator have been adjusted not to produce useless loops
      already implied by G.  This generalizes the "GF" trick
      presented in Couvreur's original FM'99 paper.
    - Promises generated for formula of the form P(a U (b U c))
      are reduced into P(c), avoiding the introduction of many
      promises that imply each other.
  * The tgba_parse() function is now available via the Python
    bindings.
  * Bug fixes:
    - The random SERE generator was using the wrong operators
      for "and" and "or", mistaking And/Or with AndRat/OrRat.
    - The translation of !{r} was incorrect when this subformula
      was recurring (e.g. in G!{r}) and r had loops.
    - Correctly recognize ltl2tgba's option -rL.
    - Using LTL simplification rules based on syntactic implication,
      or based on language containment checks, caused BDD variables
      to be allocated in an "unnatural" order, resulting in a slower
      translation and a less optimal degeneralization.
    - When ltl2tgba reads a neverclaim, it now considers the resulting
      TGBA as a Büchi automaton, and will display double circles in
      the dotty output.