From 736003057c2047ba655fcf9f795a9f39d7ad88d5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Aug 2016 12:23:46 +0200 Subject: [PATCH] * NEWS: Minor typos and reorganization. --- NEWS | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 6f73f4f12..72e459f4e 100644 --- a/NEWS +++ b/NEWS @@ -33,17 +33,34 @@ New in spot 2.0.3a (not yet released) * ltlcross and ltldo learned to bypass the shell when executing simple commands (with support for single or double-quoted - argument, and redicretion of stdin and stdout, but nothing more). + arguments, and redirection of stdin and stdout, but nothing more). + + * ltlcross and ltldo learned a new syntax to specify that an input + formula should be written in some given syntax after rewriting + some operators away. For instance the defaults arguments passed + to ltl2dstar have been changed from + --output-format=hoa %L %O + into + --output-format=hoa %[WM]L %O + where [WM] specifies that operators W and M should be rewritten + away. As a consequence running + ltldo ltl2dstar -f 'a M b' + will now work and call ltl2dstar on the equivalent formula + 'b U (a & b)' instead. The operators that can be listed between + brackets are the same as those of ltlfilt --unabbreviate option. + + * ltlcross learned to show some counterexamples when diagnosing + failures of cross-comparison checks against random state spaces. * autfilt learned to filter automata by count of SCCs (--sccs=RANGE) or by type of SCCs (--accepting-sccs=RANGE, --rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE, --weak-sccs=RANGE, --inherently-weak-sccs=RANGE). - * autfilt learned --remove-unused-ap to remove atomic proposition + * autfilt learned --remove-unused-ap to remove atomic propositions that are declared in the input automaton, but not actually used. This of course makes sense only for input/output formats that - declare atomic proposition (HOA & DSTAR). + declare atomic propositions (HOA & DSTAR). * autfilt learned two options to filter automata by count of used or unused atomic propositions: --used-ap=RANGE --unused-ap=RANGE. @@ -65,23 +82,6 @@ New in spot 2.0.3a (not yet released) --highlight-word=[NUM,]WORD option. However currently this only work on automata with Fin-less acceptance. - * ltlcross and ltldo learned a new syntax to specify that an input - formula should be written in some given syntax after rewriting - some operators away. For instance the defaults arguments passed - to ltl2dstar have been changed from - --output-format=hoa %L %O - into - --output-format=hoa %[WM]L %O - where [WM] specifies that operators W and M should be rewritten - away. As a consequence running - ltldo ltl2dstar -f 'a M b' - will now work and call ltl2dstar on the equivalent formula - 'b U (a & b)' instead. The operators that can be listed between - brackets are the same as those of ltlfilt --unabbreviate option. - - * ltlcross learned to show some counterexamples when diagnosing - failures of cross-comparison checks against random state spaces. - * genltl learned three new families: --dac-patterns=1..45, --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options these do not output scalable patterns, but simply a list of formulas @@ -196,7 +196,7 @@ New in spot 2.0.3a (not yet released) exploring automata in C++. https://spot.lrde.epita.fr/tut50.html * Another new page shows how to implement an on-the-fly Kripke - structure to implement a custom state space. + structure for a custom state space. https://spot.lrde.epita.fr/tut51.html * The concepts.html page now lists all named properties