randltl
This tool generates random formulas. By default, it will generate one random LTL formula using atomic propositions supplied on the command-line. It can be instructed to generate random Boolean or PSL formulas instead, but let us first focus on LTL generation.
For instance to obtain fave random LTL formula over the propositions
a, b, or c, use:
randltl -n5 a b c
0 0 R b F(XG(F!b M Fb) W (b R a)) F(a R !c) G(a | Fb) W (FGb R !b)
Note that the result does not always use all atomic propositions.
If you do not care about how the atomic propositions are named, you can give a nonnegative number instead:
randltl -n5 3
0 0 R p1 F(XG(F!p1 M Fp1) W (p1 R p0)) F(p0 R !p2) G(p0 | Fp1) W (FGp1 R !p1)
The syntax of the formula output can be changed using the common output options:
-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
When you select Spin's or Wring's syntax, operators W and M are
automatically rewritten using U and R (written V for Spin).
When you select LBT's syntax, you should name you atomic propositions
like p0, p1, etc… (Atomic proposition named differently will be
output by Spot in double-quotes, but this is not supported by LBT.)
randltl -l 12 randltl -8 12 randltl -s 12 randltl --wring 12
V X f W V G p5 p7 p10 ○(0) R ((□p5 R p7) W p10) X(false) V (p10 V (p10 || ([]p5 V p7))) (X((FALSE))) R ((p10=1) R ((p10=1) + ((G(p5=1)) R (p7=1))))
As you might guess from the above result, for a given set of atomic
propositions (and on the same computer) the generated formula will
always be the same. This is because each time randltl starts, it
initializes the seed of the random number generator to 0. This seed
can be changed using the --seed option. For instance the following
three commands:
randltl a b c d randltl --seed=4 a b c d randltl --seed=0 a b c d
Will give three formulas in which the first and last are identical:
Xb R ((Gb R c) W d) Gd Xb R ((Gb R c) W d)
When generating random formulas, we usually want large quantity of
them. Rather than running randltl several times with different
seeds, we can use the -n option to specify a number of formulas to
produce as seen in the very first example of this page.
By default, randltl will never output the same formula twice (this
can be changed with the --allow-dups option), so it may generate
more formulas internally than it eventually prints. To ensure
termination, for each output formula the number of ignored (because
duplicated) random formulas that are generated is limited to 100000.
Therefore, in some situations, most likely when generating small
formulas with few atomic propositions, you may see randltl stop
before the requested number of formulas has been output with an error
message.
If the integer passed to -n is negative, randltl will attempt to
generate as many formulas as it can. This is most useful when
randltl is piped to ltlfilt to select random formulas matching a
certain criterion, as we shall see later.
Besides the list of atomic propositions (a b c in our example) and
the seed, several other parameters control the generation of the
random formulas.
Initially, the random generator selects a tree size for the formula.
The default size is 15, but it can be changed using the --tree-size
option. For instance in the following, for each formula the tree size
will be chosen randomly in the range 22..30.
randltl -n 5 a b c --tree-size=22..30
c R (!Fa M Xc) !(FGc <-> (c <-> Ga)) -> ((Ga W Fa) M F(c W a)) G(((a xor Fc) W (G(a | b) R (b <-> !b))) <-> (b M 1)) 0 1
The tree size is just the number of nodes in the syntax tree of the
formula during its construction. However, because Spot automatically
applies some trivial simplifications during the construction of its
formulas (e.g., F(F(a) is reduced to F(a), a&0 to 0, etc.),
the actual size of the formula output may be smaller than the
tree size specified.
It is pretty common to obtain the formulas 0 or 1 among the first
formulas output, since many random formulas trivially simplify to
these. However, because duplicate formulas are suppressed by default,
they shall only occur once.
Stronger simplifications may be requested using the -r option, that
implements many rewritings that helps Spot translators algorithms (so
beware that using -r reduces the randomness of the output).
randltl -n 5 a b c --tree-size=22..30 -r
c R (G!a M Xc) Fa | (FGc & ((c & Ga) | (!c & F!a))) | (GF!c & ((c & F!a) | (!c & Ga))) G((Fb & G((a & G!c) | (!a & Fc))) | (G!b & F((a & Fc) | (!a & G!c)))) 0 1
The generator build the syntax tree recursively from its root, by
considering all operators that could be used for a given tree size (for
example a tree-size of 2 disables binary operators). A priority is
associated to each operator, and the probability of this operator
being selected is this priority over the sum of the priorities of all
considered operators. The default priorities for each operator can
be seen with --dump-priorities:
randltl a b c --dump-priorities
Use --ltl-priorities to set the following LTL priorities: ap 3 false 1 true 1 not 1 F 1 G 1 X 1 equiv 1 implies 1 xor 1 R 1 U 1 W 1 M 1 and 1 or 1
Where ap stands for atomic propositions (a, b, c). In this
example, when the generator builds a leaf of the syntax tree (i.e., a
subformula of tree-size 1), it must ignore all operators, and chose
between ap, false, or true, and the odds of choosing ap is
3/(3+1+1).
As indicated at the top of the output, these priorities can be changed
using the --ltl-priorities options. The most common scenario is to
disable some of the operators by giving them a null priority. The
following example disables 6 operators, and augments the priority of
U to 3 to favor its occurrence.
randltl -n 5 a b c --ltl-priorities 'xor=0,implies=0,equiv=0,W=0,M=0,X=0,U=3'
0 b 1 !F(1 U ((a U c) U b)) 1 U G!b
When using -r to simplify generated formulas, beware that these
rewritings may use operators that you disabled during the initial
random generation: you may obtain a formula that uses W even if W
has a null priority. (You can use ltlfilt to rewrite these
operators if that is a problem.)
If the --weak-fairness option is used, for each random formula
generated, a weak-fairness formula of the form GF(a) & GF(b) & GF(c)
is generated for a subset of the atomic propositions and "ANDed" to
the random formula. The --tree-size option has no influence on the
weak-fairness formula appended.
randltl -n 5 a b c --weak-fairness
0 (!Fb | !(X(0) <-> F!Fc)) & GFa & GFb & GFc GFa & GFb & GFc & F(a xor b) (a | b) & GFa & GFb & GFc & (Ga -> Gc) GFa & GFb & GFc & (GXb U (Fc U (Fc | (a R b))))
Boolean formulas may be output with the -B option:
randltl -B -n 5 a b c
!(b -> !c) c xor (b | c) !(a & (a xor b)) 0 !b -> c
In that case, priorities should be set with --boolean-priorities.
Finally, PSL formulas may be output using the -P option. However,
keep in mind that since LTL formulas are PSL formulas, generating
random PSL formula may produce many LTL formulas that do not use any
PSL operator (this is even more so the case when simplifications are
enabled with -r).
randltl -P -n 5 a b c
0
1
X(!(b -> !b) | ((b | !b | c) W !b))
{[*2..3]}
X(0)
As shown with the --dump-priorities output below, tweaking the
priorities used to generated PSL formulas requires three different
options:
randltl -P a b c --dump-priorities
Use --ltl-priorities to set the following LTL priorities: ap 3 false 1 true 1 not 1 F 1 G 1 X 1 Closure 1 equiv 1 implies 1 xor 1 R 1 U 1 W 1 M 1 and 1 or 1 EConcat 1 UConcat 1 Use --sere-priorities to set the following SERE priorities: eword 1 boolform 1 star 1 star_b 1 fstar 1 fstar_b 1 first_match 1 and 1 andNLM 1 or 1 concat 1 fusion 1 Use --boolean-priorities to set the following Boolean formula priorities: ap 3 false 1 true 1 not 1 equiv 1 implies 1 xor 1 and 1 or 1
The --ltl-priorities option we have seen previously now recognize
some new PSL-specific operators: Closure is the {sere} operator,
EConcat is the {sere}<>->f operator, and UConcat is the
{sere}[]->f operator. When these operators are selected, they
require a SERE argument which is generated according to the priorities
set by --sere-priorities: eword is the empty word, boolform is a
Boolean formula (generated using the priorities set by
--boolean-priorities), star is the unbounded Kleen star, while
star_b is the bounded version, and andNLM is the
non-length-matching variant of the and operator.