Release Spot 1.1
* configure.ac, doc/org/tools.org: Bump version number. * NEWS: Likewise, plus some missing entries.
This commit is contained in:
parent
c5225a8295
commit
556ba6df9e
3 changed files with 27 additions and 17 deletions
40
NEWS
40
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
|
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
|
acceptance conditions in a few tricky situations that were not
|
||||||
simplified previously. (See SPIN'13 paper.)
|
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
|
- An experimental "don't care" (direct) simulation has been
|
||||||
implemented. This simulations consider the acceptance
|
implemented. This simulations consider the acceptance
|
||||||
of out-of-SCC transitions as "don't care". It is not
|
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
|
from the command-line using ltlfilt's --stutter-insensitive
|
||||||
option.
|
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
|
- Several functions have been introduced to check the
|
||||||
strength of an SCC.
|
strength of an SCC.
|
||||||
is_inherently_weak_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
|
is distributed in doc/org/. The resulting html files are also
|
||||||
in doc/userdoc/.
|
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:
|
* Bug fixes:
|
||||||
|
|
||||||
- There was a memory leak in the LTL simplification code, that could
|
- There was a memory leak in the LTL simplification code, that could
|
||||||
only be triggered when disabling advanced simplifications.
|
only be triggered when disabling advanced simplifications.
|
||||||
|
|
||||||
- The translation of the PSL formula !{xxx} was incorrect when xxx
|
- The translation of the PSL formula !{xxx} was incorrect when xxx
|
||||||
simplified to false.
|
simplified to false.
|
||||||
|
|
||||||
- Various warnings triggered by new compilers.
|
- Various warnings triggered by new compilers.
|
||||||
|
|
||||||
New in spot 1.0.2 (2013-03-06):
|
New in spot 1.0.2 (2013-03-06):
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -20,7 +20,7 @@
|
||||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
AC_PREREQ([2.61])
|
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_AUX_DIR([tools])
|
||||||
AC_CONFIG_MACRO_DIR([m4])
|
AC_CONFIG_MACRO_DIR([m4])
|
||||||
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
|
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
|
||||||
|
|
|
||||||
|
|
@ -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
|
#+EMAIL spot@lrde.epita.fr
|
||||||
#+OPTIONS: H:2 num:nil toc:t
|
#+OPTIONS: H:2 num:nil toc:t
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue