LTL2TGTA

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:

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:

--medium

moderate optimizations

Miscellaneous options:

-x, --extra-options=OPTS

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

--version

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:

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

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.

spot-x(7)