spot - Command-line tools installed by Spot.
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.
Command-line tools installed by Spot.
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.
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.
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. |
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2024 by the Spot authors, see the AUTHORS File for
details. 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.
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.