# 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