Commit graph

5 commits

Author SHA1 Message Date
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
Alexandre Duret-Lutz
0cf250d839 bin: introduce autcross
Fixes #252.

* NEWS: Mention it.
* bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
files.
* bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
doc/Makefile.am: Add them.
* bin/autfilt.cc: Use is_universal() instead of is_deterministic().
* bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
ltlcross, ltldo and autcross.
* tests/core/autcross.test, tests/core/autcross2.test: New files.
* tests/Makefile.am: Add them.
* tests/core/dra2dba.test, tests/core/sbacc.test,
tests/core/streett.test: Use autcross.
2017-07-28 10:33:14 +02:00
Thomas Medioni
0c69649ba1 * bin/.gitignore: Ignore genaut binary. 2017-04-28 12:17:44 +02:00
Alexandre Duret-Lutz
e2b4d38ade more file to ignore
* bin/.gitignore, doc/org/.gitignore: Here.
2016-10-03 16:15:35 +02:00
Alexandre Duret-Lutz
134dfc73de move spot/bin/ and spot/tests/ up by one level
* spot/bin/: Move...
* bin/: ... here.
* spot/tests/: Move...
* tests/: ... here.
* Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
Adjust.
2015-12-27 20:10:59 +01:00
Renamed from spot/bin/.gitignore (Browse further)