FreeBSD Manual Pages
LTLMIX(1) User Commands LTLMIX(1) NAME ltlmix - combine formulas selected randomly SYNOPSIS ltlmix [OPTION...] [FILENAME[/COL]...] DESCRIPTION Combine formulas taken randomly from an input set. The input set is specified using FILENAME, -F FILENAME, or -f formula. By default this generates a Boolean pattern of size 5, for instance "(Ia & Ia) | Ia", where each Ia<micro>c is randomly taken from the input set. The size and nature of the pattern can be changed using generation parameters. Additionally, it is possible to rename the atomic propositions in each Ia<micro>c using -A or -P. 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 Generation parameters: --allow-dups allow duplicate formulas to be output -A, --ap-count=N[,M] rename the atomic propositions in each selected formula by drawing randomly from N atomic propositions (the rewriting is bijective if N is larger than the original set). If M is specified, two sets of atomic propositions are used to represent inputs and outputs, and options --ins/--outs can be used to classify the original proposi- tions. -B, --boolean generate Boolean combinations of formulas (default) -C, --random-conjuncts=N generate random-conjunctions of N conjuncts; shorthand for --tree-size {2N-1} -B --boolean-priorities=[disable everything but 'and'] --ins=PROPS comma-separated list of atomic propositions to consider as input, interpreted as a regex if enclosed in slashes -L, --ltl generate LTL combinations of subformulas -n, --formulas=INT number of formulas to generate (default: 1); use a negative value for unbounded generation --outs=PROPS comma-separated list of atomic propositions to consider as output, interpreted as a regex if enclosed in slashes --part-file=FILENAME read the I/O partition of atomic propositions from FILENAME -P, --polarized-ap=N[,M] similar to -A, but randomize the polarity of the new atomic proposi- tions --seed=INT seed for the random number generator (default: 0) --tree-size=RANGE tree size of main pattern generated (default: 5); input formulas count as size 1. RANGE may have one of the following forms: 'INT', 'INT..INT', or '..INT'. In the latter case, the missing number is assumed to be 1. Adjusting probabilities: --boolean-priorities=STRING set priorities for Boolean formulas --dump-priorities show current priorities, do not generate any formula --ltl-priorities=STRING set priorities for LTL formulas STRING should be a comma-separated list of assignments, assigning integer priorities to the tokens listed by --dump-priorities. 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 -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 -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: %% a single % %b the Boolean-length of the formula (i.e., all Boolean subformulas count as 1) %f the formula (in the selected syntax) %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 formula (0-based) %L the (serial) number of the formula (1-based) %[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. Example: Generates 10 random Boolean combinations of terms of the form GFa, with 'a' picked from a set of 5 atomic propositions: % ltlmix -f GFa -n10 -A5 Build a single LTL formula over subformulas taken randomly from the list of 55 patterns by Dwyer et al., using a choice of 10 atomic propositions to relabel subformulas: % genltl --dac | ltlmix -L -A10 Build 5 random positive Boolean combination of GFa and GFb: % ltlmix -f GFa -f GFb --boolean-prio=not=0,xor=0,implies=0,equiv=0 -n5 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 randltl(1), genltl(1) ltlmix (spot) 2.14.5 January 2026 LTLMIX(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=ltlmix&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>