From d573eb9b8da04eea7f73b8f10372fb057a01a0ab Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Nov 2011 18:47:45 +0100 Subject: [PATCH] * NEWS: Add an entry for the previous fix. --- ChangeLog | 4 ++++ NEWS | 12 ++++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5e47e7a10..c88b473c2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2011-11-17 Alexandre Duret-Lutz + + * NEWS: Add an entry for the previous fix. + 2011-11-16 Alexandre Duret-Lutz Fully quote guards used by neverclaims. diff --git a/NEWS b/NEWS index a99d7abcf..059590511 100644 --- a/NEWS +++ b/NEWS @@ -3,7 +3,7 @@ New in spot 0.7.1a: * Major new features: - Spot can read DiVinE models. See iface/dve2/README for details. - The genltl tool can now output 20 differents LTL formula families. - It also replace the LTLcounter Perl scripts. + It also replaces the LTLcounter Perl scripts. * Major interface changes: - The destructor of all states is now private. Any code that looks like "delete some_state;" will cause an compile error and should be @@ -34,11 +34,19 @@ New in spot 0.7.1a: - Safra complementation has been fixed in cases where more than one acceptance conditions where needed to convert the deterministic Streett automaton as a TGBA. - - The degeneralization is now idempotent. Previously degeneralizing + - The degeneralization is now idempotent. Previously, degeneralizing an already degeneralized automaton could add some states. - The degeneralization now has a deterministic behavior. Previously it was possible to obtain different output depending on the memory layout. + - Spot now outputs neverclaims with fully parenthesized guards. + I.e., instead of + (!x && y) -> goto S1 + it now outputs + ((!(x)) && (y)) -> goto S1 + This prevents problems when the model defines `x' as + #define x flag==0 + because !x then evaluated to (!flag)==0 instead of !(flag==0). New in spot 0.7.1 (2001-02-07):