0821c97eb8
For now, ltlsynt only handles LTL realizability. It uses a reduction to parity game followed by Calude et al.'s reduction from parity game to reachability game. * bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x, bin/man/Makefile.am, bin/.gitignore: New binary. * doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org, doc/org/ltlsynt.org: Document it. * spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity game wrapper for parity automata + reachability game interface from Calude et al.'s paper.
20 lines
146 B
Text
20 lines
146 B
Text
autcross
|
|
autfilt
|
|
dstar2tgba
|
|
genaut
|
|
genltl
|
|
ltl2tgba
|
|
ltl2tgta
|
|
ltlcross
|
|
ltldo
|
|
ltlfilt
|
|
ltlgrind
|
|
ltlsynt
|
|
randaut
|
|
randltl
|
|
spot
|
|
spot-x
|
|
*.a
|
|
*.1
|
|
*.7
|
|
lck-*
|