Table of Contents


ltlgrind - list mutations of a formula.


ltlgrind [OPTION...] [FILENAME[/COL]...]


List formulas that are similar to but simpler than a given formula.

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


read all formulas using LBT’s prefix syntax


parenthesized blocks that cannot be parsed as subformulas are considered as atomic properties

Mutation rules (all enabled unless those options are used):


atomic propositions are replaced with true/false


remove one operand from multops


all occurrences of an atomic proposition are replaced with another atomic proposition used in the formula


replace unary/binary operators with one of their operands


rewrite operators that have a semantically simpler form: a U b becomes a W b, etc.


on a bounded unary operator, decrement one of the bounds, or set min to 0 or max to unbounded


when an operator can be expressed as a conjunction/disjunction using simpler operators, each term of the conjunction/disjunction is a mutation. e.g. a <-> b can be written as ((a & b) | (!a & !b)) or as ((a -> b) & (b -> a)) so those four terms can be a mutation of a <-> b

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

--format=FORMAT, --stats=FORMAT

specify how each line should be output (default: "%f")

-l, --lbt

output in LBT’s syntax


output using LaTeX macros

-m, --mutations=NUM

number of mutations to apply to the formulae (default: 1)

-n, --max-count=NUM

maximum number of mutations to output

-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


sort the result by formula size

-s, --spin

output in Spin’s syntax


output in Spot’s syntax (default)


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 %


the Boolean-length of the formula (i.e., all Boolean subformulas count as 1)


the formula (in the selected syntax)


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)


the serial number of the output formula (0-based)


the original line number in the input file


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.


the length (or size) of the formula


number of atomic propositions used in the


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

Miscellaneous options:


print this help


print program version

Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options.


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


Copyright © 2024 by the Spot authors, see the AUTHORS File for details. 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.