alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/doc/org/tools.org
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

4.2 KiB
Raw Blame History

Command-line tools installed by Spot {{{SPOTVERSION}}}

This document introduces command-line tools that are installed with the Spot library. We give some examples to highlight possible use-cases but shall not attempt to cover all features exhaustively (please check the man pages for further inspiration).

Conventions

For technical reasons related to the way we generate these pages, we use the following convention when rendering shell commands. The commands issued to the shell are formatted like this with a cyan line on the left:

echo Hello World

And the output of such a command is formatted as follows, with a magenta line on the left:

Hello World

Parts of these documents (e.g., lists of options) are actually the results of shell commands and will be presented as above, even if the corresponding commands are hidden.

Documentation common to multiple tools

Command-line tools

  • randltl Generate random LTL/PSL formulas.
  • ltlfilt Filter, convert, and transform LTL/PSL formulas.
  • genltl Generate LTL formulas from scalable patterns.
  • ltl2tgba Translate LTL/PSL formulas into Büchi automata.
  • ltl2tgta Translate LTL/PSL formulas into Testing automata.
  • ltlcross Cross-compare LTL/PSL-to-automata translators.
  • ltlgrind List formulas similar to but simpler than a given LTL/PSL formula.
  • ltldo Run LTL/PSL formulas through other tools using common input and output interfaces.
  • ltlsynt Synthesize AIGER circuits from LTL/PSL specifications.
  • dstar2tgba Convert ω-automata with any acceptance into variants of Büchi automata.
  • randaut Generate random ω-automata.
  • genaut Generate ω-automata from scalable patterns.
  • autfilt Filter, convert, and transform ω-automata.
  • autcross Cross-compare tools that process automata.

Man pages

In addition to the above illustrated documentation, Spot also installs man pages for all these tools. These man pages are mostly generated automatically from the --help output of each tool, and often completed with additional text (like examples or bibliography). For convenience, you can browse their HTML versions:

autcross(1), autfilt(1), dstar2tgba(1), genaut(1), genltl(1), ltl2tgba(1), ltl2tgta(1), ltlcross(1), ltldo(1), ltlfilt(1), ltlgrind(1), ltlsynt(1), randaut(1), randltl(1), spot-x(7), spot(7).

Advanced use-cases

Citing

If some of these tools have played a significant role in a work that lead to some academic publication, please consider citing Spot. Our citing page has a list of papers you could cite.

Additionally, the man pages of these tools also contains additional references about the algorithms or data sources used.