UP | HOME

SPOT

Table of Contents

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 © 2023 Laboratoire de Recherche de l’Epita (LRE) License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.

SEE ALSO

autfilt(1) autcross(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)
The Spot web page.