From 2ac37ad58f34b827587f6f0e561fc99d3c972309 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 12 Dec 2010 11:17:20 +0100 Subject: [PATCH] * NEWS: Summarize recent changes. --- ChangeLog | 4 ++++ NEWS | 35 ++++++++++++++++++++++++++++++++++- 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index 7bf978c93..23cd7210b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2010-12-12 Alexandre Duret-Lutz + + * NEWS: Summarize recent changes. + 2010-12-11 Alexandre Duret-Lutz Merge transitions in tgba_tba_proxy. diff --git a/NEWS b/NEWS index d3b4692aa..61ef064b3 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,39 @@ New in spot 0.6a: - Nothing yet. + * Spot is now able to read an automaton expressed as a Spin neverclaim. + * The "experimental" Kripke structure introduced in Spot 0.5 has + been rewritten, and is no longer experimental. We have a + developement version of checkpn using it, and it should be + released shortly after Spot 0.7. + * The function to_spin_string(), used to output an LTL formula using + Spin's syntax, now takes an optional argument to request full + parenthesis. + * src/ltltest/genltl is a new tool that generates some interesting + families of LTL formulae, for testing purpose. + * bench/ltlclasses/ uses the above tool to conduct the same benchmark + as in the DepCoS'09 paper by Cichón et al. The resulting benchmark + completes in 12min, while it tooks days (or crashed) when the paper + was written (using Spot 0.4). + * Degeneralization has again been improved in two ways: + - It will merge the degeneralized transitions that can be merged. + - It uses a cache to speed up the improvement introduced in 0.6. + * New ltl2tgba options: + -XN: read an input automaton as a neverclaim. + -C, -CR: Compute (and display) a counterexample after running the + emptiness check. With -CR, the counterexample will be + replayed on the automaton to ensure it is correct + (previous version would always compute a replay a + counterexample when emptiness-check was enabled) + -ks: traverse the automaton to compute its number of states and + transitions (this is faster than -k whichi will also count + SCCs and paths). + * Bug fixes: + - Location of the errors messages in the TGBA parser where inaccurate. + - Various warning fixes for different versions of GCC and Clang. + - The neverclaim output with ltl2tgba -N or -NN used to ignore any + automaton simplification performed after degeneralization. + - The formula simplification based on universality and eventuallity + had a quadratic run-time. New in spot 0.6 (16-04-2010):