home | help 
LTLFILT(1)			  User Commands 		      LTLFILT(1)

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 process-
     ing.

   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 in-
	    teger, 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 con-
	    sidered 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.

     --from-ltlf[=alive]
	    transform  LTLf  (finite  LTL)  to	LTL  by introducing some 'alive'
	    proposition

     --ins=PROPS
	    comma-separated list of input atomic propositions to use with  --re-
	    label=io  or --save-part-file, interpreted as a regex if enclosed in
	    slashes

     --negate
	    negate each formula

     --nnf  rewrite formulas in negative normal form

     --outs=PROPS
	    comma-separated list of output atomic propositions to use with --re-
	    label=io or --save-part-file, interpreted as a regex if enclosed  in
	    slashes

     --part-file=FILENAME
	    file  containing  the  partition  of atomic propositions to use with
	    --relabel=io

     --relabel[=abc|pnn|io] relabel all atomic propositions, alphabetically
	    unless specified otherwise

     --relabel-bool[=abc|pnn]
	    relabel Boolean subexpressions that do  not  share	atomic	proposi-
	    tions, relabel alphabetically unless specified otherwise

     --relabel-overlapping-bool[=abc|pnn]
	    relabel  Boolean  subexpressions  even if they share atomic proposi-
	    tions, relabel alphabetically unless specified otherwise

     --remove-wm
	    rewrite operators W and M using U and R (this is an alias for  --un-
	    abbreviate=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

     --save-part-file[=FILENAME]
	    file containing the partition of atomic  propositions,  readable  by
	    --part-file

     --sonf[=PREFIX]
	    rewrite formulas in suffix operator normal form

     --sonf-aps[=FILENAME]
	    when  used	with --sonf, output the newly introduced atomic proposi-
	    tions

     --to-delta2
	    rewrite LTL formula in Ia-form

     --unabbreviate[=STR]
	    remove all occurrences of the operators specified by STR, which must
	    be a substring of "eFGiMRW^", where 'e', 'i', and '^' stand  respec-
	    tively  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

     --delta1
	    match Ia formulas

     --delta2
	    match Ia formulas

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

     --pi2  match I a formulas

     --recurrence
	    match recurrence formulas (even pathological)

     --reject-word=WORD
	    keep formulas that reject WORD

     --safety
	    match safety formulas (even pathological)

     --sigma2
	    match ILa formulas

     --size=RANGE
	    match formulas with size in RANGE

     --stutter-insensitive, --stutter-invariant
	    match stutter-insensitive LTL formulas

     --suspendable
	    synonym for --universal --eventual

     --syntactic-guarantee, --sigma1
	    match syntactic-guarantee (a.k.a. ILa) formulas

     --syntactic-obligation
	    match syntactic-obligation formulas

     --syntactic-persistence
	    match syntactic-persistence formulas

     --syntactic-recurrence
	    match syntactic-recurrence formulas

     --syntactic-safety, --pi1
	    match syntactic-safety (a.k.a. I a) 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:
     -0, --zero-terminated-output
	    separate  output  formulas with \0 instead of \n (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  se-
     quences:

     %<     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 ex-
	    tracted 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 serial number of the output formula

     %L     the original line number in the input file

     %[OP]n
	    the  nesting depth of operator OP.	OP should be a single letter de-
	    noting 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) dou-
	    ble-quotes with CSV-style escape, (p) between parentheses, any extra
	    non-alphanumeric character will be used to separate propositions

   Miscellaneous options:
     --help
	    print this help

     --version
	    print program version

     Mandatory	or  optional arguments to long options are also mandatory or op-
     tional 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  sug-
     gest 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-invari-
	    ance checks for I-regular languages.  Proceedings of SPIN'15.   LNCS
	    9232.

	    Describes the algorithm used by --stutter-insensitive option.

     *	    Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Pow-
	    erset Construction for Restricted Classes of I-Automata. Proceedings
	    of ATVA'07.  LNCS 4762.

	    Describes  the  checks implemented by the --safety, --guarantee, and
	    --obligation options.

     *	    Ivana AernA!, Radek PelA!nek: Relating Hierarchy of Temporal Proper-
	    ties to Model Checking.  Proceedings of MFCS'03.  LNCS 2747.

	    Describes  the  syntactic  LTL  classes  matched  by  the  --syntac-
	    tic-safety,  --syntactic-guarantee,  --syntactic-obligation options,
	    --syntactic-persistence, and --syntactic-recurrence options.

     *	    Kousha Etessami, Gerard J. Holzmann: Optimizing  BA1/4chi  Automata.
	    Proceedings of CONCUR'00.  LNCS 1877.

	    Describe the syntactic LTL classes matched by --eventual, and --uni-
	    versal.

     *	    Giuseppe  De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Lin-
	    ear 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.

REPORTING BUGS
     Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT
     Copyright	(C)  2025 by the Spot authors, see the AUTHORS File for details.
     License  GPLv3+:  GNU  GPL   version   3	or   later   <http://gnu.org/li-
     censes/gpl.html>.
     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)

ltlfilt (spot) 2.14.5		  January 2026			      LTLFILT(1)
home | help