# probabilistic cooling system
# every time interval, the system uses a sensor to measure the room temperature
# and decreases it if it is higher than the setting one
# decreasing each temperature unit consumes 1 resource unit
# compute the expected number of consumed resource units
# mt : measured temperature of the room
# st : desired setting temperature
# ti : time interval = 5
# t : time of operation
# each time interval, the room temperature increases randomly from 1 to 3 degrees,
# with probability 1 : 1/10, 2 : 7/10, 3 : 2/10
# modeled as a uniform distribution
# the sensor for measuring the temperature has some error modeling as a uniform
# distribution from -1 to 1
# exact value : max(0, mt - st) + (2/5)max(0, t + 5)
# max(0, mt - st) : the cost for the first time of execution the inner loop
# max(0, t + 5) : the bound on expected number of outer loop iterations
# 2/5 : cost for each iteration
def f():
var mt, st, t, r
while t >= 0:
# decrease the room temperature if needed
while mt > st:
mt = mt - 1
# consume 1 resource unit
tick 1
# the room temperature increases randomly
assume mt >= st and st >= mt
prob(1,9):
mt = mt + 1
else:
prob(7,2):
mt = mt + 2
else:
mt = mt + 3
# error of sensor
r = unif(0,2)
mt = mt + (r - 1)
# advance to the next time interval
t = t - 5