Table of Contents


ltl2tgta - translate LTL/PSL formulas into Testing Automata


ltl2tgta [OPTION...] [FORMULA...]


Translate linear-time formulas (LTL/PSL) into Testing Automata.

By default it outputs a transition-based generalized Testing Automaton the smallest Transition-based Generalized Büchi Automata, in GraphViz’s format. The input formula is assumed to be stuttering-insensitive.

Automaton type:


Generalized Testing Automaton


Testing Automaton


Transition-based Generalized Testing Automaton (default)

Input options:

-f, --formula=STRING

process the formula STRING

-F, --file=FILENAME[/COL]

process each line of FILENAME as a formula; if COL is a positive integer, assume a CSV file and read column COL; use a negative COL to drop the first line of the CSV file


read all formulas using LBT’s prefix syntax


parenthesized blocks that cannot be parsed as subformulas are considered as atomic properties

Options for TA and GTA creation:


do not create the fake initial state


create a single-pass (G)TA without artificial livelock state


add an artificial livelock state to obtain a single-pass (G)TA

Output options:

-8, --utf8

enable UTF-8 characters in output

Simplification goal:

-a, --any

no preference, do not bother making it small or deterministic

-D, --deterministic

prefer deterministic automata


prefer small automata (default)

Simplification level:


all available optimizations (slow, default)


minimal optimizations (fast)


moderate optimizations

Miscellaneous options:

-x, --extra-options=OPTS

fine-tuning options (see spot-x (7))


print this help


print program version

Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options.


If you would like to give a reference to this tool in an article, we suggest you cite the following paper:

Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon: Model checking using generalized testing automata. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI), 7400:94-112, 2012.


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.