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

* NEWS: Summarize recent noteworthy changes.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2010-04-08 15:41:42 +02:00
parent bbd526ac81
commit f282338e1c
2 changed files with 32 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,7 @@
2010-04-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Summarize recent noteworthy changes.
2010-04-07 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Modernize Bison parsers. Modernize Bison parsers.
@ -89,7 +93,7 @@
Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b).
* src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace
the FG(a)|FG(b) == FG(a|b) rule by the above more generic one. the FG(a)|FG(b) == F(Ga|Gb) rule by the above more generic one.
Add the dual rule for G(a)&G(b), as we had none (this one won't Add the dual rule for G(a)&G(b), as we had none (this one won't
improve anything in the translation, but it is more symmetric improve anything in the translation, but it is more symmetric
this way). Also simplify some pointer checks. this way). Also simplify some pointer checks.

28
NEWS
View file

@ -1,6 +1,32 @@
New in spot 0.5a New in spot 0.5a
* Nothing yet. * Several optimizations to improve some auxiliary steps
of the LTL translation (not the core of the translation):
- Better degeneralization
- SCC simplifications has been tuned for degeneralization
(ltl2tgba now has two options -R3 and -R3f: the latter will
remove every acceptance condition that used to be removed
in Spot 0.5 while the former will leave useless acceptance conditions
going to accepting SCC. Experience shows that -R3 is more
favorable to degeneralization).
- ltl2tgba will perform SCC optimizations before degeneralization
and not the converse
- We added a syntactic simplification rule to rewrite F(a)|F(b) as F(a|b).
We only had a rule for the more specific FG(a)|FG(b) = F(Ga|Gb).
- 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
efficiently.
* New options have been added to the CGI script for
- SVG output
- SCC simplifications
* Bug fixes:
- The precedence of the "->" and "<->" Boolean operators has been
adjusted to better match other tools.
Spot <= 0.5 used to parse "a & b -> c & d" as "a & (b -> c) & d";
Spot >= 0.5.1 will parse it as "(a & b) -> (c & d)".
- The random graph generator was fixed (again!) not to produce
dead states as documented.
- Locations in the error messages of the LTL parser were off by one.
New in spot 0.5 (2010-02-01): New in spot 0.5 (2010-02-01):