diff --git a/NEWS b/NEWS index d91b6925c..f385ac8b6 100644 --- a/NEWS +++ b/NEWS @@ -19,11 +19,11 @@ New in spot 0.9.2a: - ltlfilt: Filter lists of formulas according to several criteria (e.g., match only safety formulas that are larger than - some given size). Besides being used as a "grep" tool - for formulas, this can also be used to convert - files of formulas between different syntaxes, apply - some simplifications, check whether to formulas are - equivalent, ... + some given size). Besides being used as a "grep" tool + for formulas, this can also be used to convert + files of formulas between different syntaxes, apply + some simplifications, check whether to formulas are + equivalent, ... - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, 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 source tree. The old version of ltl2tgba with its gazillion 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: @@ -85,9 +87,10 @@ New in spot 0.9.2a: automaton. - The enumerate_cycles class implements the Loizou-Thanisch - algorithm to enumerate the cycles of a SCC. As an example of - use, the is_weak_scc() function will tell whether an SCC is weak - (all its cycles are accepting, or none of them are). + algorithm to enumerate elementary cycles in a SCC. As an + example of use, is_weak_scc() will tell whether an SCC is + inherently weak (all its cycles are accepting, or none of them + are). - parse_lbt() will parse an LTL formula expressed in the prefix syntax used (at least) by LBT, LBTT and Scheck.