FreeBSD Manual Pages
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 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 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 an- other 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/disjunc- tion 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 --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 col- umn 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] re- places 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 denoting the operator to count, or multiple letters to fuse sev- eral 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 Miscellaneous options: --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. REPORTING BUGS Report bugs to <spot@lrde.epita.fr>. COPYRIGHT Copyright (C) 2024 by the Spot authors, see the AUTHORS File for de- tails. 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.12.1 September 2024 LTLGRIND(1)
NAME | SYNOPSIS | DESCRIPTION | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlgrind&sektion=1&manpath=FreeBSD+Ports+14.3.quarterly>