UP | HOME

RANDLTL

Table of Contents

NAME

randltl − generate random LTL/PSL formulas

SYNOPSIS

randltl [OPTION...] N|PROP...

DESCRIPTION

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

Generation:

−−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

Adjusting probabilities:

−−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.

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

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

Miscellaneous options:

−−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.

EXAMPLES

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

BIBLIOGRAPHY

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.

REPORTING BUGS

Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT

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.

SEE ALSO

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