Table of Contents


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.

Type of formula to generate:

-B, --boolean

generate Boolean formulas

-L, --ltl

generate LTL formulas (default)

-P, --psl

generate PSL formulas

-S, --sere

generate SERE



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 for the random number generator (0)


tree size of the formulas generated, before mandatory trivial simplifications (15)


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.


No rewriting


basic rewritings and eventual/universal rules


additional syntactic implication rules


better implications using containment

Adjusting probabilities:


set priorities for Boolean formulas


show current priorities, do not generate any formula


set priorities for LTL formulas


set priorities for SERE formulas

STRING should be a comma-separated list of assignments, assigning integer priorities to the tokens listed by --dump-priorities.

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


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


output in Spot’s syntax (default)


output in Wring’s syntax

The FORMAT string passed to --format may use the following interpreted sequences:


a single %


the Boolean-length of the formula (i.e., all Boolean subformulas count as 1)


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)


the (serial) number of the formula


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.


the length (or size) of the formula


number of atomic propositions used in the


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

Miscellaneous options:


print this help


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 © 2018 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.


genaut(1), genltl(1), ltlfilt(1), randaut(1)