From 556ba6df9ed6bb266a5e2d99a572aabb7bbf423e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 28 Apr 2013 13:00:17 +0200 Subject: [PATCH] Release Spot 1.1 * configure.ac, doc/org/tools.org: Bump version number. * NEWS: Likewise, plus some missing entries. --- NEWS | 40 +++++++++++++++++++++++++--------------- configure.ac | 2 +- doc/org/tools.org | 2 +- 3 files changed, 27 insertions(+), 17 deletions(-) diff --git a/NEWS b/NEWS index 7064685b9..6261ae0eb 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 1.0.2a (not released): +New in spot 1.1 (2013-04-28): Several of the new features described below are discribed in @@ -31,6 +31,15 @@ New in spot 1.0.2a (not released): acceptance conditions in a few tricky situations that were not simplified previously. (See SPIN'13 paper.) + - A new translation, called compsusp(), for "Compositional + Suspension" is implemented on top of ltl_to_tgba_fm(). + (See SPIN'13 paper.) + + - Some experimental LTL rewriting rules that trie to gather + suspendable formulas are implemented and can be activated + with the favor_event_univ option of ltl_simplifier. As + always please check doc/tl/tl.tex for the list of rules. + - An experimental "don't care" (direct) simulation has been implemented. This simulations consider the acceptance of out-of-SCC transitions as "don't care". It is not @@ -47,15 +56,6 @@ New in spot 1.0.2a (not released): from the command-line using ltlfilt's --stutter-insensitive option. - - A new translation, called compsusp(), for "Compositional - Suspension" is implemented on top of ltl_to_tgba_fm(). - (See SPIN'13 paper.) - - - Some experimental LTL rewriting rules that trie to gather - suspendable formulas are implemented and can be activated - with the favor_event_univ option of ltl_simplifier. As - always please check doc/tl/tl.tex for the list of rules. - - Several functions have been introduced to check the strength of an SCC. is_inherently_weak_scc() @@ -93,15 +93,25 @@ New in spot 1.0.2a (not released): is distributed in doc/org/. The resulting html files are also in doc/userdoc/. + * Web interface: + + - A new "Compositional Suspension" tab has been added to experiment + with compositional suspension. + + * Benchmarks: + + - See bench/spin13/README for instructions to reproduce our Spin'13 + benchmark for the compositional suspension. + * Bug fixes: - - There was a memory leak in the LTL simplification code, that could - only be triggered when disabling advanced simplifications. + - There was a memory leak in the LTL simplification code, that could + only be triggered when disabling advanced simplifications. - - The translation of the PSL formula !{xxx} was incorrect when xxx - simplified to false. + - The translation of the PSL formula !{xxx} was incorrect when xxx + simplified to false. - - Various warnings triggered by new compilers. + - Various warnings triggered by new compilers. New in spot 1.0.2 (2013-03-06): diff --git a/configure.ac b/configure.ac index 06593ec1d..8e5082e15 100644 --- a/configure.ac +++ b/configure.ac @@ -20,7 +20,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [1.0.2a], [spot@lrde.epita.fr]) +AC_INIT([spot], [1.1], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/tools.org b/doc/org/tools.org index 8e56a2dba..332f47acc 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,4 +1,4 @@ -#+TITLE: Command-line tools installed by Spot 1.0.2 +#+TITLE: Command-line tools installed by Spot 1.1 #+EMAIL spot@lrde.epita.fr #+OPTIONS: H:2 num:nil toc:t