* NEWS: Summarize recent changes.

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):