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.
--gta Generalized Testing Automaton
--ta Testing Automaton
--tgta Transition-based Generalized Testing Automaton (default)
-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
--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
-8, --utf8 enable UTF-8 characters in output
-a, --any no preference, do not bother making it small or deterministic
-D, --deterministic prefer deterministic automata
--small prefer small automata (default)
--high all available optimizations (slow, default)
--low minimal optimizations (fast)
--medium moderate optimizations
-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.
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.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.