# a complex expected polynomial bound program
# it involves sequential and nested loops
# and different types of probabilistic commands
def f():
var x, y, w, N, M, r
assume M >= 0 and y >= 0
x = 0
while x < N:
r = unif(0,1)
x = x + r
y = y + 3*M
r = bin(3,1,2)
y = y + r
while y > 0:
while w > 0:
w = w - 1
tick 1
prob(2,1):
y = y - 1
else:
y = y + 1
tick 1