FreeBSD Manual Pages
RANDLTL(1) User Commands RANDLTL(1) 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 sim- plifications (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, --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 The FORMAT string passed to --format may use the following interpreted se- quences: %% 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 (0-based) %L the (serial) number of the formula (1-based) %[OP]n the nesting depth of operator OP. OP should be a single letter de- noting 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. %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) dou- ble-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions Miscellaneous options: --help print this help --version print program version Mandatory or optional arguments to long options are also mandatory or op- tional for any corresponding short options. BIBLIOGRAPHY If you would like to give a reference to this tool in an article, we sug- gest you cite the following paper: * Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. 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 REPORTING BUGS Report bugs to <spot@lrde.epita.fr>. COPYRIGHT Copyright (C) 2025 by the Spot authors, see the AUTHORS File for details. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/li- censes/gpl.html>. This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. SEE ALSO genaut(1), genltl(1), ltlfilt(1), randaut(1) ltlmix(1) randltl (spot) 2.14.5 January 2026 RANDLTL(1)
NAME | SYNOPSIS | DESCRIPTION | BIBLIOGRAPHY | EXAMPLES | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=randltl&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>