ltlmix - combine formulas selected randomly
ltlmix [OPTION...] [FILENAME[/COL]...]
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 "(φ₁ & φ₂) | φ₃", where each φᵢ 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 φᵢ using -A or -P.
-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
--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 propositions.
-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 propositions
--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.
--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.
-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 sequences:
|
%% |
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 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.
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
% ltlmix -f GFa -f GFb --boolean-prio=not=0,xor=0,implies=0,equiv=0 -n5
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2025 by the Spot authors, see the AUTHORS File for
details. License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and
redistribute it. There is NO WARRANTY, to the extent
permitted by law.