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

* NEWS: rephrase some items

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-10-26 07:56:47 +02:00
parent 301ad1ebf0
commit e2ed5f6b98
1 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

21
NEWS
View file

@ -19,11 +19,11 @@ New in spot 0.9.2a:
- ltlfilt: Filter lists of formulas according to several criteria - ltlfilt: Filter lists of formulas according to several criteria
(e.g., match only safety formulas that are larger than (e.g., match only safety formulas that are larger than
some given size). Besides being used as a "grep" tool some given size). Besides being used as a "grep" tool
for formulas, this can also be used to convert for formulas, this can also be used to convert
files of formulas between different syntaxes, apply files of formulas between different syntaxes, apply
some simplifications, check whether to formulas are some simplifications, check whether to formulas are
equivalent, ... equivalent, ...
- ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA,
BA, or Monitor). A fondamental change to the BA, or Monitor). A fondamental change to the
@ -43,7 +43,9 @@ New in spot 0.9.2a:
test versions of genltl and randltl have been removed from the test versions of genltl and randltl have been removed from the
source tree. The old version of ltl2tgba with its gazillion source tree. The old version of ltl2tgba with its gazillion
options is still is src/tgbatest/ and is meant to be used for options is still is src/tgbatest/ and is meant to be used for
testing only. testing only. Although ltlcross is meant to replace LBTT, we
are still using both tools in this release, but this is likely
the last time we redistribute LBTT.
* New features in the Spot library: * New features in the Spot library:
@ -85,9 +87,10 @@ New in spot 0.9.2a:
automaton. automaton.
- The enumerate_cycles class implements the Loizou-Thanisch - The enumerate_cycles class implements the Loizou-Thanisch
algorithm to enumerate the cycles of a SCC. As an example of algorithm to enumerate elementary cycles in a SCC. As an
use, the is_weak_scc() function will tell whether an SCC is weak example of use, is_weak_scc() will tell whether an SCC is
(all its cycles are accepting, or none of them are). inherently weak (all its cycles are accepting, or none of them
are).
- parse_lbt() will parse an LTL formula expressed in the prefix - parse_lbt() will parse an LTL formula expressed in the prefix
syntax used (at least) by LBT, LBTT and Scheck. syntax used (at least) by LBT, LBTT and Scheck.