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
−−csv−escape
quote the formula for use in a CSV file
−−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 % |
|||
%f |
the formula (in the selected syntax) |
|||
%L |
the (serial) number of the formula |
−−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.
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
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. |
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2016 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.