FreeBSD Manual Pages
LTLFILT(1) User Commands LTLFILT(1) NAME ltlfilt - filter files or lists of LTL/PSL formulas SYNOPSIS ltlfilt [OPTION...] [FILENAME[/COL]...] DESCRIPTION Read a list of formulas and output them back after some optional pro- cessing. 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 Error handling: --drop-errors discard erroneous lines (default) --ignore-errors do not report syntax errors --skip-errors output erroneous lines as-is without processing Transformation options: --boolean-to-isop rewrite Boolean subformulas as irredundant sum of products (im- plies at least -r1) --define[=FILENAME] when used with --relabel or --relabel-bool, output the relabel- ing map using #define statements --exclusive-ap=AP,AP,... if any of those APs occur in the formula, add a term ensuring two of them may not be true at the same time. Use this option multiple times to declare independent groups of exclusive propo- sitions. --from-ltlf[=alive] transform LTLf (finite LTL) to LTL by introducing some 'alive' proposition --negate negate each formula --nnf rewrite formulas in negative normal form --relabel[=abc|pnn] relabel all atomic propositions, alphabetically unless specified otherwise --relabel-bool[=abc|pnn] relabel Boolean subexpressions that do not share atomic proposi- tions, relabel alphabetically unless specified otherwise --relabel-overlapping-bool[=abc|pnn] relabel Boolean subexpressions even if they share atomic propo- sitions, relabel alphabetically unless specified otherwise --remove-wm rewrite operators W and M using U and R (this is an alias for --unabbreviate=WM) --remove-x remove X operators (valid only for stutter-insensitive proper- ties) -r, --simplify[=LEVEL] simplify formulas according to LEVEL (see below); LEVEL is set to 3 if omitted --sonf[=PREFIX] rewrite formulas in suffix operator normal form --sonf-aps[=FILENAME] when used with --sonf, output the newly introduced atomic propo- sitions --unabbreviate[=STR] remove all occurrences of the operators specified by STR, which must be a substring of "eFGiMRW^", where 'e', 'i', and '^' stand respectively for <->, ->, and xor. If no argument is passed, the subset "eFGiMW^" is used. The simplification LEVEL may be set as follows. 0 No rewriting 1 basic rewritings and eventual/universal rules 2 additional syntactic implication rules 3 better implications using containment Filtering options (matching is done after transformation): --accept-word=WORD keep formulas that accept WORD --ap=RANGE match formulas with a number of atomic propositions in RANGE --boolean match Boolean formulas --bsize=RANGE match formulas with Boolean size in RANGE --equivalent-to=FORMULA match formulas equivalent to FORMULA --eventual match pure eventualities --guarantee match guarantee formulas (even pathological) --implied-by=FORMULA match formulas implied by FORMULA --imply=FORMULA match formulas implying FORMULA --liveness match liveness properties --ltl match only LTL formulas (no PSL operator) -N, --nth=RANGE assuming input formulas are numbered from 1, keep only those in RANGE --obligation match obligation formulas (even pathological) --persistence match persistence formulas (even pathological) --recurrence match recurrence formulas (even pathological) --reject-word=WORD keep formulas that reject WORD --safety match safety formulas (even pathological) --size=RANGE match formulas with size in RANGE --stutter-insensitive, --stutter-invariant match stutter-insensitive LTL formulas --suspendable synonym for --universal --eventual --syntactic-guarantee match syntactic-guarantee formulas --syntactic-obligation match syntactic-obligation formulas --syntactic-persistence match syntactic-persistence formulas --syntactic-recurrence match syntactic-recurrence formulas --syntactic-safety match syntactic-safety formulas --syntactic-stutter-invariant, --nox match stutter-invariant formulas syntactically (LTL-X or siPSL) --universal match purely universal formulas -u, --unique drop formulas that have already been output (not affected by -v) -v, --invert-match select non-matching formulas RANGE may have one of the following forms: 'INT', 'INT..INT', '..INT', or 'INT..' WORD is lasso-shaped and written as 'BF;BF;...;BF;cycle{BF;...;BF}' where BF are arbitrary Boolean formulas. The 'cycle{...}' part is mandatory, but the prefix can be omitted. 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 -c, --count print only a count of matched formulas --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 -n, --max-count=NUM output at most NUM formulas -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 -q, --quiet suppress all normal output -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 %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. %r wall-clock time elapsed in seconds (excluding parsing) %R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add LETTERS to re- strict to (u) user time, (s) system time, (p) parent process, or (c) children processes. %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. Exit status: 0 if some formulas were output (skipped syntax errors do not count) 1 if no formulas were output (no match) 2 if any error has been reported BIBLIOGRAPHY If you would like to give a reference to this tool in an article, we suggest you cite the following paper: • Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. The following papers describe algorithms used by ltlfilt: • Kousha Etessami: A note on a question of Peled and Wilke regard- ing stutter-invariant LTL. Information Processing Letters 75(6): 261-263 (2000). Describes the transformation behind the --remove-x option. • Thibaud Michaud and Alexandre Duret-Lutz: Practical stutter-in- variance checks for -regular languages. Proceedings of SPIN'15. LNCS 9232. Describes the algorithm used by --stutter-insensitive option. • Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of -Automata. Pro- ceedings of ATVA'07. LNCS 4762. Describes the checks implemented by the --safety, --guarantee, and --obligation options. • Ivana ern, Radek Pelnek: Relating Hierarchy of Temporal Proper- ties to Model Checking. Proceedings of MFCS'03. LNCS 2747. Describes the syntactic LTL classes matched by the --syntac- tic-safety, --syntactic-guarantee, --syntactic-obligation op- tions, --syntactic-persistence, and --syntactic-recurrence op- tions. • Kousha Etessami, Gerard J. Holzmann: Optimizing Bchi Automata. Proceedings of CONCUR'00. LNCS 1877. Describe the syntactic LTL classes matched by --eventual, and --universal. • Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. Proceedings of IJCAI'13. Describe the transformation implemented by --from-ltlf to reduce LTLf model checking to LTL model checking. 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 randltl(1), ltldo(1) ltlfilt (spot) 2.12.1 September 2024 LTLFILT(1)
NAME | SYNOPSIS | DESCRIPTION | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlfilt&sektion=1&manpath=FreeBSD+Ports+14.3.quarterly>