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