From 8893f34da1b1d87fb2896ca854f7fa5849f1ca1d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 22 May 2012 13:43:34 +0200 Subject: [PATCH] * NEWS: Summarize recent changes. --- NEWS | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/NEWS b/NEWS index de0061a64..0b5a961ed 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,34 @@ New in spot 0.9a: + * The version of LBTT we distribute include a patch from Tomáš + Babiak to count the number of non-deterministic states, and the + number of deterministic automata produced. + See lbtt/NEWS for the list of other differences with the original + version of LBTT 1.2.1. + * The Couvreur/FM translator has learned two new tricks. These only + help to speedup the translation by not issuing states or + acceptance conditions that would be latter suppresed by other + optimizations. + - The translation rules used to translate subformulae of the G + operator have been adjusted not to produce useless loops + already implied by G. This generalizes the "GF" trick + presented in Couvreur's original FM'99 paper. + - Promises generated for formula of the form P(a U (b U c)) + are reduced into P(c), avoiding the introduction of many + promises that imply each other. * Bug fixes: - The random SERE generator was using the wrong operators for "and" and "or", mistaking And/Or with AndRat/OrRat. - The translation of !{r} was incorrect when this subformula was recurring (e.g. in G!{r}) and r had loops. - Correctly recognize ltl2tgba's option -rL. + - Using LTL simplification rules based on syntactic implication, + or based on language containment checks, caused BDD variables + to be allocated in an "unnatural" order, resulting in a slower + translation and a less optimal degeneralization. + - When ltl2tgba reads a neverclaim, it now considers the resulting + TGBA as a Büchi automaton, and will display double circles in + the dotty output. New in spot 0.9 (2012-05-09):