18 Jul
2015
18 Jul
'15
8:11 a.m.
We are happy to announce the release of Spot 1.99.2.
This maintenance release fixes some bugs that have been reported
(or not) against 1.99.1, and speeds up a couple of things.
You can download the new release from
http://www.lrde.epita.fr/dload/spot/spot-1.99.2.tar.gz
See https://spot.lrde.epita.fr/ for documentation
and installation instructions. Please report any problem
and questions to spot(a)lrde.epita.fr
New in spot 1.99.2 (2015-07-18)
* The scc_info object, used to build a map of SCCs while gathering
additional information, has been simplified and speed up. One
test case where ltlcross would take more than 13min (to check the
translation of one PSL formula) now takes only 75s.
* streett_to_generalized_buchi() is a new function that implements
what its name suggests, with some SCC-based optimizations over the
naive definition. It is used by the to_generalized_buchi() and
remove_fin() functions when the input automaton is a Streett
automaton with more than 3 pairs (this threeshold can be changed
via the SPOT_STREETT_CONV_MIN environment variable -- see the
spot-x(7) man page for details).
This is mainly useful to ltlcross, which has to get rid of "Fin"
acceptance to perform its checks. As an example, the Streett
automaton generatated by ltl2dstar (configured with ltl2tgba) for
the formula
!((GFa -> GFb) & (GFc -> GFd))
has 4307 states and 14 acceptance sets. The new algorithm can
translate it into a TGBA with 9754 states and 7 acceptance sets,
while the default approch used for converting any acceptance
to TGBA would produce 250967 states and 7 acceptance sets.
* Bugs fixed:
- p[+][:*2] was not detected as belonging to siPSL.
- scc_filter() would incorrectly remove Fin marks from
rejecting SCCs.
- the libspotltsmin library is installed.
- ltlcross and ltldo did not properly quote atomic propositions
and temporary file names containing a single-quote.
- a missing Python.h is now diagnosed at ./configure time, with
the suggestion to either install python3-devel, or run
./configure --disable-python.
- Debian packages for libraries have been split from
the main Spot package, as per Debian guidelines.
--
Alexandre Duret-Lutz