Generate random LTL Formulae [closed]

Question

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.

Answer 1

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!

Answer 2

Python 3, 298 293 283 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!

Answer 3

Java 8, 456 423 bytes

n->{int r=(int)(Math.random()*9);return r>4?(r<8?"FGX!".charAt(r-5):"")+b(n):"("+b(n)+"UWR&|".charAt(r)+b(n)+")";}String b(int n){int r=(int)(Math.random()*9);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=(int)(Math.random()*(n>0?256:261))-128;return r>131?"wxyz".charAt((r+130)%4)+"":r>127?"("+i(--n)+"+-*/".charAt(r-128)+i(n)+")":r+"";}

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 bytes instead (and is explained below):

n->{int r=(int)(Math.random()*10);return r>4?(r<9?"FGX!".charAt(r-5):"")+b(n):"("+b(n)+"UWR&|".charAt(r)+b(n)+")";}String b(int n){int r=(int)(Math.random()*9);return r>7?"abcd".charAt((int)(Math.random()*4))+"":r>6?"True":r>5?"False":n>0?"("+i(n)+"<≤>≥=≠".charAt(r)+i(n)+")":b(n);}String i(int n){int r=(int)(Math.random()*(n>0?256:261))-128;return r>131?"wxyz".charAt((int)(Math.random()*4))+"":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=(int)(Math.random()*10); 
                         //  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=(int)(Math.random()*9); 
                         //  Random integer [0,8]
  return r>7?            //  Is it 8:
     "abcd".charAt((int)(Math.random()*4))+""
                         //   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=(int)(Math.random()*(n>0?256:261))-128;
                         //  Random integer in range [-128,128]
                         //  OR [-128,132] if the input is larger than 0
  return r>131?          //  If it is 132:
     "wxyz".charAt((int)(Math.random()*4))+""
                         //   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)`