diff --git a/NEWS b/NEWS index 6c9dfab6b..7a7e4c11a 100644 --- a/NEWS +++ b/NEWS @@ -14,7 +14,7 @@ New in spot 0.8.3a: with rules for PSL operators (and some new LTL rules as well). See doc/tl/tl.pdf for the list of the rewritings implemented. - Some of these rewritings that may produce larger formulas - (For instance to rewrite "{a;b;c}" as "a & X(b & Xc)".) + (for instance to rewrite "{a;b;c}" into "a & X(b & Xc)") may be explicitely disabled with a new option. - The src/ltltest/randltl tool can now generate random SEREs and random PSL formulae. @@ -23,21 +23,27 @@ New in spot 0.8.3a: translation from SERE to DFA is likely to be rewriten in a future version. - A new function, length_boolone(), computes the size of an - LTL/PSL formula while considering that any Boolean term - has length 1. + LTL/PSL formula while considering that any Boolean term has + length 1. + - The LTL/PSL parser recognizes some UTF-8 characters (like ◇ or + ∧) as operators, and some output routines now have an UTF-8 + output mode. Tools like randltl and ltl2tgba have gained an -8 + option to enable such output. See doc/tl/tl.pdf for the list + of recognized codepoints. - A new direct simulation reduction has been implemented. It works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, and it can be tested via ltl2tgba's -RDS option. - changes to the on-line translator: + SVG output is available + can display some properties of a formula - + new options for direct simulation and larger rewritings + + new options for direct simulation, larger rewritings, and + utf-8 output - configure --without-included-lbtt will prevent LBTT from being configured and built. This helps on systems (such as MinGW) where LBTT cannot be built. The test-suite will skip any LBTT-based test if LBTT is missing. * Interface changes: - - Operators ->, <->, U, W, R, and M are no parsed as + - Operators ->, <->, U, W, R, and M are now parsed as right-associative to better match the PSL standard. - The new entry point for LTL/PSL simplifications is the function ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh.