prseq-2.imp

# 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 > 0:
        r = unif(1, 3)
        y = y + r
        tick 3
    while y > 0:
        prob(2,1):
            y = y - 10
        else:
            y = y - 0
        tick 1