UP | HOME

LTLFILT

Table of Contents

NAME

ltlfilt − filter files or lists of LTL/PSL formulas

SYNOPSIS

ltlfilt [OPTION...] [FILENAME[/COL]...]

DESCRIPTION

Read a list of formulas and output them back after some optional processing.

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

Error handling:

−−drop−errors

discard erroneous lines (default)

−−ignore−errors

do not report syntax errors

−−skip−errors

output erroneous lines as−is without processing

Transformation options:

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

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

Filtering options (matching is done after transformation):

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

Output options:

−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

−−csv−escape

quote the formula for use in a CSV file

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

%f

the formula (in the selected syntax)

%F

the name of the input file

%L

the original line number in the input file

Miscellaneous options:

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

Exit status:

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

BIBLIOGRAPHY

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.

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

randltl(1), ltldo(1)