# Generate random LTL Formulae [closed]

An LTL Formula l is defined by the following grammar (where <x> describes the non-terminal symbol x):

<l> ::= <b> | F <l> | G <l> | X <l> | (<l> U <l>) | (<l> W <l>) | (<l> R <l>)
| (<l> & <l>) | (<l> \| <l>) | !<l>
<b> ::= BVar | True | False | (<i> < <i>) | (<i> <= <i>) | (<i> > <i>) | (<i> >= <i>)
| (<i> = <i>) | (<i> != <i>)
<i> ::= IVar | -128 | -127 | ... | 127 | (<i> + <i>) | (<i> - <i>)
| (<i> * <i>) | (<i> / <i>)


(I escaped a pipe to denote boolean or. You should not print that backslash in your output)

BVar and IVar represent variables of boolean and integral types respectively. Each must be one of four possible single character variable names, and there may by no overlap between BVar and IVar. For instance, you may choose a,b,c,d for BVar and w,x,y,z for IVar

Note that all binary operators must have parentheses around them and that no other parentheses are allowed.

Your task is to write a function that takes one input encoding the maximal nesting depth of an LTL formula and prints a random formula limited by that depth (but not necessarily exactly that depth). The distribution does not have to be uniformly random, but each possible formula has to have a non-zero chance of being generated.

You may use ≤, ≥, and ≠ instead of <=, >=, and !=.

You may add or remove whitespace as you see fit. Even no whitespace at all is allowed.

Examples:

f(0) -> True
f(0) -> d
f(1) -> (a&b)
f(1) -> Fd
f(1) -> (x<y)
f(3) -> (G(x!=y)|Fb)
f(3) -> (x<(w+(y+z)))


Standard loopholes are forbidden.

This is code-golf, so the shortest code in bytes wins.

• May we use ≤, ≥, and ≠ instead of <=, >=, and !=?
Oct 20, 2017 at 10:33
• That is allowed. I will update the challenge accordingly. Oct 20, 2017 at 10:35
• What is the "nesting depth"? Oct 20, 2017 at 12:50
• Is everything in <i> evenly divided in terms of randomness? So these four (<i> + <i>) | (<i> - <i>) | (<i> * <i>) | (<i> / <i>) each have a chance of 1/260 to occur (and -128 through 127 also each has a 1/260 chance to occur)? Oct 20, 2017 at 13:35
• @PeterTaylor I think (not sure) this refers to the maximum depth of <i>. Oct 20, 2017 at 13:42

## Perl 5, 251 bytes

249 bytes code + 2 for -pa.

$d=I;sub a{map"($d$_$d)",@_}@I=(w..z,-128..127,a qw{+ - * /});@L=(@B=(a..d,True,False,a qw{< <= > >= = !=}),B,FL,GL,XL,"!".($d=L),a qw{U W R & |});$_=$L[rand@L];0while s/L|B|I/@{$&}[rand@{$&}]/e;$;=$_;s/[^()]//g;0while s/\)\(//g;$_=y/(//>"@F"?redo:\$


Try it online!

# Python 3, 298293283 279 bytes

def f(n,t=1):s,*X=c([[(c(V[t>1]),)],[('%s',0),(c('FGX!')+'%s',1)]][t&1]+[(f"(%s{c('<U+≤W->R*≥&/=|+≠'[t::3])}%s)",*[2-(t&1)]*2)]);return n and s%tuple(f(n-1,x)for x in X)or c(V[t>1])
from random import*
c=choice
V=['True','False',*'abcd'],[*map(str,range(-128,128)),*'wxyz']


Try it online!

• Generated "(XF((dW-91)U(46|21))&c)" for me, and (46|21) is not a valid subformula, same for (dW-91). You use integers where you have to have bools Oct 20, 2017 at 11:56
• @Sacchan Ah, I returned either a bool or int when the level was 0. Oct 20, 2017 at 12:25

# Java 8, 456423419 407 bytes

n->{int r=9;r*=Math.random();return r>4?(r<8?"FGX!".charAt(r-5):"")+b(n):"("+b(n)+"UWR&|".charAt(r)+b(n)+")";};String b(int n){int r=9;r*=Math.random();return r>7?"abcd".charAt(r%4)+"":r>6?"True":r>5?"False":n>0?"("+i(n)+"<≤>≥=≠".charAt(r)+i(n)+")":b(n);}String i(int n){int r=n>0?256:261;r*=Math.random();return(r-=128)>131?"wxyz".charAt(r+2&3)+"":r>127?"("+i(--n)+"+-*/".charAt(r-128)+i(n)+")":r+"";}


-4 bytes thanks to @ceilingcat.

Try it here.

NOTE: Due to the rule "The distribution does not have to be uniformly random", I've been able to golf some parts by using modulo-4 on the input or random integer for the characters "abcd" or "wxyz", and change Math.random()*10 to Math.random()*9 and change the ternary a bit. Personally I prefer to have the randomness equally divided for each method, which is 456 441 bytes instead (and is explained below):

n->{int r=10;r*=Math.random();return r>4?(r<9?"FGX!".charAt(r-5):"")+b(n):"("+b(n)+"UWR&|".charAt(r)+b(n)+")";};String b(int n){int r=9,t=4;r*=Math.random();return r>7?"abcd".charAt(t*=Math.random())+"":r>6?"True":r>5?"False":n>0?"("+i(n)+"<≤>≥=≠".charAt(r)+i(n)+")":b(n);}String i(int n){int r=n>0?256:261,t=4;r*=Math.random();return(r-=128)>131?"wxyz".charAt(t*=Math.random())+"":r>127?"("+i(--n)+"+-*/".charAt(r-128)+i(n)+")":r+"";}


Try it here.

Explanation:

n->{                     // Method with integer parameter and String return-type
int r=10;r*=Math.random();
//  Random integer [0,9]
return r>4?            //  Is it [5,9]:
(r<9?                //   Is it [5,8]:
"FGX!".charAt(r-5) //    Return a leading character
:                   //   Else (it's 9):
"")                //    Return nothing
+b(n)                //   + call to method b(n)
:                     //  Else (it's [0-4]):
"("                  //   Return opening parenthesis
+b(n)                //   + call to method b(n)
+"UWR&|".charAt(r)   //   + middle character
+b(n)                //   + another call to method b(n)
+")";                //   + closing parenthesis
}                        // End of method

String b(int n){         // Method b(n) with integer parameter and String return-type
int r=9,t=4;r*=Math.random();
//  Random integer [0,8]
return r>7?            //  Is it 8:
"abcd".charAt(t*=Math.random())+""
//   Return random from "abcd"
:r>6?                 //  Else-if it's 7:
"True"               //   Return literal "True"
:r>5?                 //  Else-if it's 6:
"False"              //   Return literal "False"
:n>0?                 //  Else-if it's [0-5] AND the input is larger than 0:
"("                  //   Return opening parenthesis
+i(n)                //   + call to method i(n)
+"<≤>≥=≠".charAt(r)  //   + middle character
+i(n)                //   + another call to method i(n)
+")"                 //   + closing parenthesis
:                     //  Else (it's [0-5] and the input is 0):
b(n);                //   Call itself again, hoping for random [6-8]
}                        // End of method b(n)

String i(int n){         // Method i(n) with integer parameter and String return-type
int r=n>0?256:261,t=4;r*=Math.random();return(r-=128)
//  Random integer in range [-128,128]
//  OR [-128,132] if the input is larger than 0
>131?                  //  If it is 132:
"wxyz".charAt(t*=Math.random())+""
//   Return random from "wxyz"
:r>127?               //  Else-if it's [128,131]:
"("                  //   Return opening parenthesis
+i(--n)              //   + call to i(n-1)
+"+-*/".charAt(r-128)//   + middle character
+i(n)                //   + another call to i(n-1)
+")"                 //   + closing parenthesis
:                     //  Else:
r+"";                //   Return the random integer [-128,127]
}                        // End of method i(n)