spot/bin/man/ltlsynt.x at 75550112a7d6e08d64a63a94303db0605149472c - alarsyo/spot - Personal Forge

alarsyo/spot

Thibaud Michaud 0821c97eb8 add ltlsynt executable

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.

2017-09-25 12:23:47 +02:00

3 lines

94 B

Text

Raw Blame History

	`.\" -- coding: utf-8 --`
	`[NAME]`
	`ltlsynt \- synthesize AIGER circuits from LTL specifications`