ltlgrind - list mutations of a formula.
ltlgrind [OPTION...] [FILENAME[/COL]...]
List formulas that are similar to but simpler than a given formula.
-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
--ap-to-const
atomic propositions are replaced with true/false
--remove-multop-operands
remove one operand from multops
--remove-one-ap
all occurrences of an atomic proposition are replaced with another atomic proposition used in the formula
--remove-ops
replace unary/binary operators with one of their operands
--rewrite-ops
rewrite operators that have a semantically simpler form: a U b becomes a W b, etc.
--simplify-bounds
on a bounded unary operator, decrement one of the bounds, or set min to 0 or max to unbounded
--split-ops
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
-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
--latex
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 |
sort the result by formula size |
-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. | ||
|
%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.
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2023 Laboratoire de Recherche de l’Epita (LRE)
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.
ltlcross(1)