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

* NEWS: Mention W and M.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2010-04-14 18:58:40 +02:00
parent 28094c87da
commit 26bd137020
2 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-04-14 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Mention W and M.
2010-04-14 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-14 Alexandre Duret-Lutz <adl@lrde.epita.fr>
More LTL reductions for W and M. More LTL reductions for W and M.

12
NEWS
View file

@ -16,6 +16,18 @@ New in spot 0.5a
- The syntactic simplification rule for F(a&GF(b)) = F(a)&GF(b) has - The syntactic simplification rule for F(a&GF(b)) = F(a)&GF(b) has
be disabled because the latter formula is in fact harder to translate be disabled because the latter formula is in fact harder to translate
efficiently. efficiently.
* New LTL operators: W (weak until) and its dual M (strong release)
- Weak until allows many LTL specification to be specified more
compactly.
- All LTL translation algorithms have been updated to
support these operators.
- Although they do not add any expressive power, translating
"a W b" is more efficient (read smaller output automaton) than
translating the equivalent form using the U operator.
- Basic syntactic rewriting rules will automatically rewrite "a U
(b | G(a))" and "(a U b)|G(a)" as "a W b", so you will benefit
from the new operators even if you do not use them. Similar
rewriting rules exist for R and M, although they are less used.
* New options have been added to the CGI script for * New options have been added to the CGI script for
- SVG output - SVG output
- SCC simplifications - SCC simplifications