Generate random temporal logic formulas.
The formulas are built over the atomic propositions named by PROPS... or, if N is a nonnegative number, using N arbitrary names.
-B, --boolean generate Boolean formulas
-L, --ltl generate LTL formulas (default)
-P, --psl generate PSL formulas
-S, --sere generate SERE
--allow-dups allow duplicate formulas to be output
-n, --formulas=\,INT\/ number of formulas to output (1) use a negative value for unbounded generation
-r, --simplify[=\,LEVEL\/] simplify formulas according to LEVEL (see below); LEVEL is set to 3 if omitted
--seed=\,INT\/ seed for the random number generator (0)
--tree-size=\,RANGE\/ tree size of the formulas generated, before mandatory trivial simplifications (15)
--weak-fairness append some weak-fairness conditions
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.
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
--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
--sere-priorities=\,STRING\/ set priorities for SERE 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 \e0 instead of \en (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
%[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.
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172.
If you do not mind about the name of the atomic propositions, just give a number instead:
% randltl -n10 3You can disable or favor certain operators by changing their priority. The following disables xor, implies, and equiv, and multiply the probability of X to occur by 10.
% randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b cThis is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.