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

* NEWS: Document to_wring_string().

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-10-20 19:20:28 +02:00
parent 877082bfb0
commit 5f6c262ae5
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
NEWS
View file

@ -82,16 +82,19 @@ New in spot 0.9.2a:
simulations in a loop as long as it diminishes the size of the simulations in a loop as long as it diminishes the size of the
automaton. automaton.
- The enumerate_cycles class implements the Loizou-Thanisch algorithm - The enumerate_cycles class implements the Loizou-Thanisch
to enumerate the cycles of a SCC. As an example of use, the algorithm to enumerate the cycles of a SCC. As an example of
is_weak_scc() function will tell whether an SCC is weak (all use, the is_weak_scc() function will tell whether an SCC is weak
its cycles are accepting, or none of them are). (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.
to_lbt_string() can be used to print an LTL formula using this to_lbt_string() can be used to print an LTL formula using this
syntax. syntax.
- to_wring_string() can be used to print an LTL formula into
Wring's syntax.
- The LTL/PSL parser now has a lenient mode that can be usefull - The LTL/PSL parser now has a lenient mode that can be usefull
to interpret atomic proposition with language-specific constructs. to interpret atomic proposition with language-specific constructs.
In lenient mode, any (...) or {...} block that cannot be parsed In lenient mode, any (...) or {...} block that cannot be parsed