randltl - generate random LTL/PSL formulas
randltl [OPTION...] N|PROP...
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 \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.
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 generates 10 random LTL formulas over the propositions a, b, and c, with the default tree-size, and all available operators.
% randltl -n10 a b c
If you do not mind about the name of the atomic propositions, just give a number instead:
% randltl -n10 3
You 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 c
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2024 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.