# sequential loops program so that
# the second loop depends on the first
# both are probabilistic loops

def f():
    var x, y, r
    assume y >= 10

    while x - y > 2:
        r = unif(1, 3)
        y = y + r
        tick 3
    while y > 9:
        prob(2,1):
            y = y - 10
        else:
            y = y - 0
        tick 1