Commit graph

107 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
a2cbf0af3a sanity: also check the 80-column limit in bin
* tests/sanity/80columns.test: Check bin sources.
* bin/ltlsynt.cc: Fix it.
2017-09-26 21:46:42 +02:00
Alexandre Duret-Lutz
c473e4ca0b ltlsynt: handle --algo with XARGMATCH
* bin/ltlsynt.cc: Use XARGMATCH for better error handling.
2017-09-26 21:44:37 +02:00
Alexandre Duret-Lutz
69daf9c261 bin: make sure that all options are in a named section
This also fixes some empty lines and unsorted options
that appeared in some tools.

* tests/sanity/bin.test: Ensure this is done.
* bin/README: Add a new paragraph about this.
* bin/autcross.cc, bin/ltlcross.cc: Move the
output options in their own section.
* bin/common_color.cc: Assume color options are
in group -15.
* bin/common_finput.cc, bin/common_finput.hh:
Add a headless variant.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc,
bin/randaut.cc, bin/randltl.cc:  Do not force the
children groups, so that the options are correctly sorted.
* bin/ltlsynt.cc: Add missing groups.
2017-09-26 21:28:16 +02:00
Thibaud Michaud
d6ae7af5f5 ltlsynt: translate winning strategy to AIGER
* bin/ltlsynt.cc: Here.
* doc/org/ltlsynt.org: Document it.
* tests/core/ltlsynt.test: Test it.
2017-09-25 12:23:47 +02:00
Thibaud Michaud
601e1405de parity game: compute winning strategy
* spot/misc/game.cc, spot/misc/game.hh: Here.
* bin/ltlsynt.cc: Realizability is now done by checking if the winning
strategy contains the initial state.
2017-09-25 12:23:47 +02:00
Thibaud Michaud
f414e9f5f2 parity game: add Zielonka's recursive algorithm
* spot/misc/game.cc, spot/misc/game.hh: Implement it.
* bin/ltlsynt.cc: Use it.
* doc/org/ltlsynt.org: Document it.
2017-09-25 12:23:47 +02:00
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