Automaton type:

--gta

Generalized Testing Automaton

--ta

Testing Automaton

--tgta

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

--lbt-input

read all formulas using LBT's prefix syntax

--lenient

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

Options for TA and GTA creation:

--multiple-init

do not create the fake initial state

--single-pass

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

--single-pass-lv

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

--small

prefer small automata (default)

Simplification level:

--high

all available optimizations (slow, default)

--low

minimal optimizations (fast)

--medium

moderate optimizations

Miscellaneous options:

-x, --extra-options=OPTS

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

--help

print this help

--version

print program version

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