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

SEE ALSO

spot-x(7)