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
--liveness match liveness properties
--ltl match only LTL formulas (no PSL operator)
-N, --nth=\,RANGE\/ assuming input formulas are numbered from 1, keep only those in RANGE
--obligation match obligation formulas (even pathological)
--persistence match persistence formulas (even pathological)
--recurrence match recurrence 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
--suspendable synonym for --universal --eventual
--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.
-0, --zero-terminated-output separate output formulas with \e0 instead of \en (for use with xargs -0)
-8, --utf8 output using UTF-8 characters
-c, --count print only a count of matched formulas
--format=\,FORMAT\/, --stats=\,FORMAT\/ specify how each line should be output (default: "%f")
-l, --lbt output in LBT's syntax
--latex output using LaTeX macros
-n, --max-count=\,NUM\/ output at most NUM formulas
-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
-q, --quiet suppress all normal output
-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 %
%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
%h, %[vw]h the class of the formula is the Manna-Pnueli hierarchy ([v] replaces abbreviations by class names, [w] for all compatible classes)
%L the original line number in the input file
%[OP]n the nesting depth of operator OP. OP should be a single letter denoting the operator to count, or multiple letters to fuse several operators during depth evaluation. Add '~' to rewrite the formula in negative normal form before counting.
%r wall-clock time elapsed in seconds (excluding parsing)
%R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add LETTERS to restrict to (u) user time, (s) system time, (p) parent process, or (c) children processes.
%s the length (or size) of the formula
%x, %[LETTERS]X, %[LETTERS]x number of atomic propositions used in the
formula; add LETTERS to list atomic propositions
with (n) no quoting, (s) occasional double-quotes with C-style escape, (d) double-quotes with C-style escape, (c) double-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions
--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
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.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.