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.

Sacchan

Posted 2017-10-20T10:24:29.287

Reputation: 621

May we use ≤, ≥, and ≠ instead of <=, >=, and !=? – Adám – 2017-10-20T10:33:38.547

That is allowed. I will update the challenge accordingly. – Sacchan – 2017-10-20T10:35:15.347

3What is the "nesting depth"? – Peter Taylor – 2017-10-20T12:50:26.777

1Is everything in  evenly divided in terms of randomness? So these four ( + ) | ( - ) | ( * ) | ( / ) each have a chance of 1/260 to occur (and -128 through 127 also each has a 1/260 chance to occur)? – Kevin Cruijssen – 2017-10-20T13:35:32.187

@PeterTaylor I think (not sure) this refers to the maximum depth of . – Kevin Cruijssen – 2017-10-20T13:42:13.383

Hmm, I guess this also means that if the input is 0, the integer -128 through 127 have a 1/256 change of occurring for ; if the input is 1 it at first has first a 1/260 chance of occurring, and if it happens to be +-*/ (4/260 chance), the next time it randomly selects  it has a 1/256 chance again because we have reached our maximum nested depth. Am I understanding what you've meant with maximal nested depth correctly, @Sacchan? – Kevin Cruijssen – 2017-10-20T13:43:59.203

@KevinCruijssen The probabilities do not have to be equal. As I stated, every part just has to have a non-zero probability of occurring.

Nesting depth refers to the longest path in the syntax tree of the formula. If you have a depth of zero, you can only have a node without children (such as a constant or a variable). A nesting depth of 1 gives a unary or binary operator with the children having a nesting depth of at most 0. And so forth. – Sacchan – 2017-10-20T14:13:23.177

<l> cannot derive 55, as far as I can see. And the path in the syntax tree for True has length 2: <l> -> -> True – rici – 2017-10-20T17:34:11.660

It seems (from the examples) that we should read "maximal nesting depth of an LTL formula" liteally (i.e. it is the nesting depth of the resulting formula rather than that of the syntax tree path taken, as assumed by @rici above). Could you clarify this? – Jonathan Allan – 2017-10-21T15:12:50.007

Also, if I am correct, could you clarify whether the nesting depth of Fd would be zero or one? – Jonathan Allan – 2017-10-21T15:25:44.437

@rici: You are correct, 55 was an erroneous example. I have removed it. – Sacchan – 2017-10-22T10:29:20.427

@Jonathan Allan: You are correct. Fd would be a nesting depth of one (since the Tree would have F as root node and d as its child) – Sacchan – 2017-10-22T10:29:23.440

Answers

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!

Dom Hastings

Posted 2017-10-20T10:24:29.287

Reputation: 16 415

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!

TFeld

Posted 2017-10-20T10:24:29.287

Reputation: 19 246

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 – Sacchan – 2017-10-20T11:56:02.410

@Sacchan Ah, I returned either a bool or int when the level was 0. – TFeld – 2017-10-20T12:25:59.477

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)`

Kevin Cruijssen

Posted 2017-10-20T10:24:29.287

Reputation: 67 575

Generate random LTL Formulae

Answers

Perl 5, 251 bytes

Python 3, 298 293 283 279 bytes

Java 8, 456 423 bytes