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

* NEWS: Reorganize entries for next release.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2018-08-10 14:05:37 +02:00
parent ff19c0620f
commit 042591a986
1 changed files with 17 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

30
NEWS
View file

@ -1,5 +1,22 @@
New in spot 2.6.1.dev (not yet released) 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 - 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 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, 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, with arbitrary acceptance condition into a parity automaton,
based on a last-appearance record (LAR) construction. 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) New in spot 2.6.1 (2018-08-04)
Command-line tools: Command-line tools: