From 26bd13702006d8cb2959ceeefd53cf115057409d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 14 Apr 2010 18:58:40 +0200 Subject: [PATCH] * NEWS: Mention W and M. --- ChangeLog | 4 ++++ NEWS | 12 ++++++++++++ 2 files changed, 16 insertions(+) diff --git a/ChangeLog b/ChangeLog index 7321157a5..c16065095 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2010-04-14 Alexandre Duret-Lutz + + * NEWS: Mention W and M. + 2010-04-14 Alexandre Duret-Lutz More LTL reductions for W and M. diff --git a/NEWS b/NEWS index 14ddd9117..0250fa5f3 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,18 @@ New in spot 0.5a - 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 LTL operators: W (weak until) and its dual M (strong release) + - Weak until allows many LTL specification to be specified more + compactly. + - All LTL translation algorithms have been updated to + support these operators. + - Although they do not add any expressive power, translating + "a W b" is more efficient (read smaller output automaton) than + translating the equivalent form using the U operator. + - Basic syntactic rewriting rules will automatically rewrite "a U + (b | G(a))" and "(a U b)|G(a)" as "a W b", so you will benefit + from the new operators even if you do not use them. Similar + rewriting rules exist for R and M, although they are less used. * New options have been added to the CGI script for - SVG output - SCC simplifications