From aadef1fd87ea5e803dc3b61476e4e5ffe9e0668f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 13 Dec 2010 19:28:48 +0100 Subject: [PATCH] * NEWS: Update the news about minimization. --- ChangeLog | 4 ++++ NEWS | 21 ++++++++++++++------- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6f455bdd1..52abddf55 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2010-12-13 Alexandre Duret-Lutz + + * NEWS: Update the news about minimization. + 2010-11-26 Alexandre Duret-Lutz Speed up wdba.test, it was too slow for our buildfarm. diff --git a/NEWS b/NEWS index 61ef064b3..69da36042 100644 --- a/NEWS +++ b/NEWS @@ -6,34 +6,41 @@ New in spot 0.6a: 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 + 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 + * 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 + 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. + * An implementation of Dax et al.'s paper for minimizing obligation + formulae has been integrated. Use ltl2tgba -Rm to enable this + optimization; it will have no effect if the property is not an + obligation. * 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 + 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). + -Rn: Minimize automata for obligation formulae. + -M: Build a deterministic monitor. + -O: Tell whether an automaton is a safety automaton. * 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. + - The formula simplification based on universality and eventuallity + had a quadratic run-time. New in spot 0.6 (16-04-2010):