alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* NEWS: Mention utf-8 output.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-04-29 19:51:36 +02:00
parent 6ea88efddc
commit e64a1bf565
1 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
NEWS
View file

@ -14,7 +14,7 @@ New in spot 0.8.3a:
with rules for PSL operators (and some new LTL rules as well). with rules for PSL operators (and some new LTL rules as well).
See doc/tl/tl.pdf for the list of the rewritings implemented. See doc/tl/tl.pdf for the list of the rewritings implemented.
- Some of these rewritings that may produce larger formulas - 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. may be explicitely disabled with a new option.
- The src/ltltest/randltl tool can now generate random SEREs - The src/ltltest/randltl tool can now generate random SEREs
and random PSL formulae. 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 translation from SERE to DFA is likely to be rewriten in a
future version. future version.
- A new function, length_boolone(), computes the size of an - A new function, length_boolone(), computes the size of an
LTL/PSL formula while considering that any Boolean term LTL/PSL formula while considering that any Boolean term has
has length 1. 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 - A new direct simulation reduction has been implemented. It
works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, works directly on TGBAs. It is in src/tgbaalgos/simlation.hh,
and it can be tested via ltl2tgba's -RDS option. and it can be tested via ltl2tgba's -RDS option.
- changes to the on-line translator: - changes to the on-line translator:
+ SVG output is available + SVG output is available
+ can display some properties of a formula + 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 - configure --without-included-lbtt will prevent LBTT from being
configured and built. This helps on systems (such as MinGW) configured and built. This helps on systems (such as MinGW)
where LBTT cannot be built. The test-suite will skip any where LBTT cannot be built. The test-suite will skip any
LBTT-based test if LBTT is missing. LBTT-based test if LBTT is missing.
* Interface changes: * 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. right-associative to better match the PSL standard.
- The new entry point for LTL/PSL simplifications is the function - The new entry point for LTL/PSL simplifications is the function
ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh.