diff --git a/NEWS b/NEWS index a09a8ca8c..5f0660bff 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,22 @@ New in spot 2.6.1.dev (not yet released) + Command-line tools: + + - ltlsynt now has three algorithms for synthesis: + --algo=sd is the historical one. The automaton of the formula + is split to separate inputs and outputs, then + determinized (with Safra construction). + --algo=ds the automaton of the formula is determinized (Safra), + then split to separate inputs and outputs. + --alog=lar translate the formula to a deterministic automaton + with an arbitrary acceptance condition, then turn it + into a parity automaton using LAR, and split it. + In all three cases, the obtained parity game is solved using + Zielonka algorithm. Calude's quasi-polynomial time algorithm has + been dropped as it was not used. + + Library: + - The LTL parser learned syntactic sugar for nested ranges of X using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These correspond to the next!, next_e!, and next_a! operators of PSL, @@ -31,19 +48,6 @@ New in spot 2.6.1.dev (not yet released) with arbitrary acceptance condition into a parity automaton, based on a last-appearance record (LAR) construction. - - ltlsynt now has three algorithms for synthesis: - --algo=sd is the historical one. The automaton of the formula - is split to separate inputs and outputs, then - determinized (with Safra construction). - --algo=ds the automaton of the formula is determinized (Safra), - then split to separate inputs and outputs. - --alog=lar translate the formula to a deterministic automaton - with an arbitrary acceptance condition, then turn it - into a parity automaton using LAR, and split it. - In all three cases, the obtained parity game is solved using - Zielonka algorithm. Calude's quasi-polynomial time algorithm has - been dropped as it was not used. - New in spot 2.6.1 (2018-08-04) Command-line tools: