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

* NEWS: Update with recent fixes.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2011-10-24 06:56:02 +02:00
parent a4d1e18bf3
commit 8549eb9d16
2 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2011-10-24 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Update with recent fixes.
2011-10-23 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-10-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Safra: Fix usage of multiple acceptance conditions and fix text output. Safra: Fix usage of multiple acceptance conditions and fix text output.

21
NEWS
View file

@ -2,7 +2,6 @@ New in spot 0.7.1a:
* Major new features: * Major new features:
- Spot can read DiVinE models. See iface/dve2/README for details. - Spot can read DiVinE models. See iface/dve2/README for details.
- The experimental Nips interface has been removed.
- The genltl tool can now output 20 differents LTL formula families. - The genltl tool can now output 20 differents LTL formula families.
It also replace the LTLcounter Perl scripts. It also replace the LTLcounter Perl scripts.
* Major interface changes: * Major interface changes:
@ -10,22 +9,36 @@ New in spot 0.7.1a:
"delete some_state;" will cause an compile error and should be "delete some_state;" will cause an compile error and should be
updated to "some_state->destroy();". This new syntax is supported updated to "some_state->destroy();". This new syntax is supported
since version 0.7. since version 0.7.
- The experimental Nips interface has been removed.
* Minor changes: * Minor changes:
- The dotty_reachable() function has a new option "assume_sba" that - The dotty_reachable() function has a new option "assume_sba" that
can be used for rendering automata with state-based acceptance. can be used for rendering automata with state-based acceptance.
In that case, acceptance states are displayed with a double In that case, acceptance states are displayed with a double
circle. ltl2tgba (both command line and on-line) Use it to display circle. ltl2tgba (both command line and on-line) Use it to display
degeneralized automata. degeneralized automata.
- Identifiers used to name atomic proposition can contain dots.
E.g.: X.Y is now an atomic proposition, while it was understood
as X&Y in previous versions.
* Internal improvements: * Internal improvements:
- The on-line ltl2tgba CGI script uses a cache to produce faster - The on-line ltl2tgba CGI script uses a cache to produce faster
answers. answers.
- Better memory managementmanagment for the states of explicit - Better memory management for the states of explicit automata.
automata. Thanks to the aforementioned ->destroy() change, we Thanks to the aforementioned ->destroy() change, we can avoid
can avoid cloning explicit states. cloning explicit states.
- tgba_product has learned how to be faster when one of the operands - tgba_product has learned how to be faster when one of the operands
is a Kripke structure (15% speedup). is a Kripke structure (15% speedup).
- The reduction rule for "a M b" has been improved: it can be - The reduction rule for "a M b" has been improved: it can be
reduced to "a & b" if "a" is a pure eventuallity. reduced to "a & b" if "a" is a pure eventuallity.
- More useless acceptance conditions are removed by SCC simplifications.
* Bug fixes:
- Safra complementation has been fixed in cases where more than
one acceptance conditions where needed to convert the
deterministic Streett automaton as a TGBA.
- The degeneralization is now idempotent. Previously degeneralizing
an already degeneralized automaton could add some states.
- The degeneralization now has a deterministic behavior. Previously
it was possible to obtain different output depending on the
memory layout.
New in spot 0.7.1 (2001-02-07): New in spot 0.7.1 (2001-02-07):