From f282338e1ccf017b5a5f1f1cc17464185e0eef96 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Apr 2010 15:41:42 +0200 Subject: [PATCH] * NEWS: Summarize recent noteworthy changes. --- ChangeLog | 6 +++++- NEWS | 28 +++++++++++++++++++++++++++- 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0020bd13c..85e14322d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2010-04-08 Alexandre Duret-Lutz + + * NEWS: Summarize recent noteworthy changes. + 2010-04-07 Alexandre Duret-Lutz Modernize Bison parsers. @@ -89,7 +93,7 @@ Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace - the FG(a)|FG(b) == FG(a|b) rule by the above more generic one. + the FG(a)|FG(b) == F(Ga|Gb) rule by the above more generic one. Add the dual rule for G(a)&G(b), as we had none (this one won't improve anything in the translation, but it is more symmetric this way). Also simplify some pointer checks. diff --git a/NEWS b/NEWS index 90abe5200..14ddd9117 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,32 @@ New in spot 0.5a - * Nothing yet. + * Several optimizations to improve some auxiliary steps + of the LTL translation (not the core of the translation): + - Better degeneralization + - SCC simplifications has been tuned for degeneralization + (ltl2tgba now has two options -R3 and -R3f: the latter will + remove every acceptance condition that used to be removed + in Spot 0.5 while the former will leave useless acceptance conditions + going to accepting SCC. Experience shows that -R3 is more + favorable to degeneralization). + - ltl2tgba will perform SCC optimizations before degeneralization + and not the converse + - We added a syntactic simplification rule to rewrite F(a)|F(b) as F(a|b). + We only had a rule for the more specific FG(a)|FG(b) = F(Ga|Gb). + - The syntactic simplification rule for F(a&GF(b)) = F(a)&GF(b) has + be disabled because the latter formula is in fact harder to translate + efficiently. + * New options have been added to the CGI script for + - SVG output + - SCC simplifications + * Bug fixes: + - The precedence of the "->" and "<->" Boolean operators has been + adjusted to better match other tools. + Spot <= 0.5 used to parse "a & b -> c & d" as "a & (b -> c) & d"; + Spot >= 0.5.1 will parse it as "(a & b) -> (c & d)". + - The random graph generator was fixed (again!) not to produce + dead states as documented. + - Locations in the error messages of the LTL parser were off by one. New in spot 0.5 (2010-02-01):