NAME

spot - Command-line tools installed by Spot.

SYNOPSIS

Spot is a C++ library for ω-automata and LTL formulas manipulation. It also comes with Python bindings and a set of command-line tools that are listed below.

DESCRIPTION

Command-line tools installed by Spot.

Tools that output LTL/PSL formulas:

genltl: Generate LTL formulas from scalable patterns.
ltlfilt: Filter, convert, and transform LTL or PSL formulas.
ltlgrind: Mutate LTL or PSL formulas to generate similar but simpler ones. Use this when looking for shorter formula to reproduce a bug.
randltl: Generate random LTL or PSL formulas.

Tools that output automata or circuits:

autfilt: Filter, convert, and transform ω-automata.
dstar2tgba: Convert ω-automata into variants of Transition-based Büchi automata.
genaut: Generate ω-automata from scalable patterns.
ltl2tgba: Convert LTL or PSL into variants of Transition-based Generalized Büchi Automata, and to other types of automata.
ltl2tgta: Convert LTL or PSL into variants of Transition-based Generalized Testing Automata.
ltlsynt: Synthesize AIGER circuits from LTL/PSL specifications.
randaut: Generate random ω-automata.

Tools that run other tools:

autcross: Cross-compare tools processing ω-automata, watch for bugs, and generate statistics.
ltlcross: Cross-compare translators of LTL or PSL formulas into ω-automata, watch for bugs, and generate statistics.
ltldo: Wrap any tool that inputs LTL or PSL formulas and possibly outputs ω-automata; provides Spot's I/O interface.

REPORTING BUGS

Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT

Copyright © 2022 Laboratoire de Recherche et Développement de l'Epita. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.