ltlfilt − filter files or lists of LTL/PSL formulas
ltlfilt [OPTION...] [FILENAME[/COL]...]
Read a list of formulas and output them back after some optional processing.
−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
−−drop−errors
discard erroneous lines (default)
−−ignore−errors
do not report syntax errors
−−skip−errors
output erroneous lines as−is without processing
−−boolean−to−isop
rewrite Boolean subformulas as irredundant sum of products (implies at least −r1)
−−define[=FILENAME]
when used with −−relabel or −−relabel−bool, output the relabeling map using #define statements
−−exclusive−ap=AP,AP,...
if any of those APs occur in the formula, add a term ensuring two of them may not be true at the same time. Use this option multiple times to declare independent groups of exclusive propositions.
−−from−ltlf[=alive]
transform LTLf (finite LTL) to LTL by introducing some ’alive’ proposition
−−negate
negate each formula
−−nnf |
rewrite formulas in negative normal form |
−−relabel[=abc|pnn]
relabel all atomic propositions, alphabetically unless specified otherwise
−−relabel−bool[=abc|pnn]
relabel Boolean subexpressions, alphabetically unless specified otherwise
−−remove−wm
rewrite operators W and M using U and R (this is an alias for −−unabbreviate=WM)
−−remove−x
remove X operators (valid only for stutter−insensitive properties)
−r, −−simplify[=LEVEL]
simplify formulas according to LEVEL (see below); LEVEL is set to 3 if omitted
−−unabbreviate[=STR]
remove all occurrences of the operators specified by STR, which must be a substring of "eFGiMRW^", where ’e’, ’i’, and ’^’ stand respectively for <−>, −>, and xor. If no argument is passed, the subset "eFGiMW^" is used.
The simplification LEVEL may be set as follows.
0 |
No rewriting |
|||
1 |
basic rewritings and eventual/universal rules |
|||
2 |
additional syntactic implication rules |
|||
3 |
better implications using containment |
−−accept−word=WORD
keep formulas that accept WORD
−−ap=RANGE
match formulas with a number of atomic propositions in RANGE
−−boolean
match Boolean formulas
−−bsize=RANGE
match formulas with Boolean size in RANGE
−−equivalent−to=FORMULA
match formulas equivalent to FORMULA
−−eventual
match pure eventualities
−−guarantee
match guarantee formulas (even pathological)
−−implied−by=FORMULA
match formulas implied by FORMULA
−−imply=FORMULA
match formulas implying FORMULA
−−ltl |
match only LTL formulas (no PSL operator) |
−−obligation
match obligation formulas (even pathological)
−−reject−word=WORD
keep formulas that reject WORD
−−safety
match safety formulas (even pathological)
−−size=RANGE
match formulas with size in RANGE
−−stutter−insensitive, −−stutter−invariant
match stutter−insensitive LTL formulas
−−syntactic−guarantee
match syntactic−guarantee formulas
−−syntactic−obligation
match syntactic−obligation formulas
−−syntactic−persistence
match syntactic−persistence formulas
−−syntactic−recurrence
match syntactic−recurrence formulas
−−syntactic−safety
match syntactic−safety formulas
−−syntactic−stutter−invariant, −−nox
match stutter−invariant formulas syntactically (LTL−X or siPSL)
−−universal
match purely universal formulas
−u, −−unique
drop formulas that have already been output (not affected by −v)
−v, −−invert−match
select non−matching formulas
RANGE may have one of the following forms: ’INT’, ’INT..INT’, ’..INT’, or ’INT..’
WORD is lasso−shaped and written as ’BF;BF;...;BF;cycle{BF;...;BF}’ where BF are arbitrary Boolean formulas. The ’cycle{...}’ part is mandatory, but the prefix can be omitted.
−c, −−count
print only a count of matched formulas
−n, −−max−count=NUM
output at most NUM formulas
−q, −−quiet
suppress all normal output
−0, −−zero−terminated−output
separate output formulas with \0 instead of \n (for use with xargs −0)
−8, −−utf8
output using UTF−8 characters
−−format=FORMAT
specify how each line should be output (default: "%f")
−l, −−lbt
output in LBT’s syntax
−−latex
output using LaTeX macros
−o, −−output=FORMAT
send output to a file named FORMAT instead of standard output. The first formula sent to a file truncates it unless FORMAT starts with ’>>’.
−p, −−full−parentheses
output fully−parenthesized formulas
−s, −−spin
output in Spin’s syntax
−−spot |
output in Spot’s syntax (default) |
−−wring
output in Wring’s syntax
The FORMAT string passed to −−format may use the following interpreted sequences:
%< |
the part of the line before the formula if it comes from a column extracted from a CSV file | ||
%> |
the part of the line after the formula if it comes from a column extracted from a CSV file | ||
%% |
a single % | ||
%a |
number of atomic propositions used in the formula | ||
%b |
the Boolean−length of the formula (i.e., all Boolean subformulas count as 1) | ||
%f |
the formula (in the selected syntax) | ||
%F |
the name of the input file | ||
%L |
the original line number in the input file | ||
%s |
the length (or size) of the formula |
−−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.
0 |
if some formulas were output (skipped syntax errors do not count) | ||
1 |
if no formulas were output (no match) | ||
2 |
if any error has been reported |
If you would like to give a reference to this tool in an article, we suggest you cite the following paper:
• |
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA’13. LNCS 8172. |
The following papers describe algorithms used by ltlfilt:
• |
Kousha Etessami: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters 75(6): 261-263 (2000). |
Describes the transformation behind the −−remove−x option.
• |
Thibaud Michaud and Alexandre Duret-Lutz: Practical stutter-invariance checks for ω-regular languages. Proceedings of SPIN’15. LNCS 9232. |
Describes the algorithm used by −−stutter−insensitive option.
• |
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA’07. LNCS 4762. |
Describes the checks implemented by the −−safety, −−guarantee, and −−obligation options.
• |
Ivana Černá, Radek Pelánek: Relating Hierarchy of Temporal Properties to Model Checking. Proceedings of MFCS’03. LNCS 2747. |
Describes the syntactic LTL classes matched by the −−syntactic−safety, −−syntactic−guarantee, −−syntactic−obligation options, −−syntactic−persistence, and −−syntactic−recurrence options.
• |
Kousha Etessami, Gerard J. Holzmann: Optimizing Büchi Automata. Proceedings of CONCUR’00. LNCS 1877. |
Describe the syntactic LTL classes matched by −−eventual, and −−universal.
• |
Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. Proceedings of IJCAI’13. |
Describe the transformation implemented by −−from−ltlf to reduce LTLf model checking to LTL model checking.
Report bugs to <spot@lrde.epita.fr>.
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.