UP | HOME

LTL2TGTA

Table of Contents

NAME

ltl2tgta − translate LTL/PSL formulas into Testing Automata

SYNOPSIS

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

DESCRIPTION

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:

−−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.

BIBLIOGRAPHY

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.

REPORTING BUGS

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

COPYRIGHT

Copyright © 2016 Laboratoire de Recherche et Développement de l’Epita. 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

spot-x(7)