GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages
LTLGRIND(1) User Commands LTLGRIND(1)

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 © 2022 Laboratoire de Recherche et Développement de l'Epita. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.

ltlcross(1)
February 2022 ltlgrind (spot) 2.10.4

Search for    or go to Top of page |  Section 1 |  Main Index

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.