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
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 |
|||
%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
© 2017 Laboratoire de Recherche et Développement
de l’Epita. 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.