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

NAME
     ltlgrind - list mutations of a formula.

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

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

   Mutation rules (all enabled unless those options are used):
     --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  be-
	    comes 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 mu-
	    tation.  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

     --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 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 (0-based)

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

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

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
     ltlcross(1)

ltlgrind (spot) 2.14.5		  January 2026			     LTLGRIND(1)
home | help