You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
182 lines
7.9 KiB
182 lines
7.9 KiB
import stormpy
|
|
import stormpy.simulator
|
|
|
|
#householdWaitCounter = [0,0]
|
|
householdWaitCounter = [0,0,0]
|
|
cumulativeDraw = 0
|
|
cumulativeRevenue = 0
|
|
maxWaitingTime = -1
|
|
|
|
def frame(i, observation, propertyForScheduling,labels):
|
|
global cumulativeDraw
|
|
global cumulativeRevenue
|
|
global maxWaitingTime
|
|
energyPrice = int(str(observation['energy_price']))
|
|
totalDraw = int(str(observation['power_draw1'])) + int(str(observation['power_draw2']))
|
|
rejected1 = str(observation["job_rejected1"]) == ("true")
|
|
rejected2 = str(observation["job_rejected2"]) == ("true")
|
|
scheduled1 = str(observation["job_scheduled1"]) == ("true")
|
|
scheduled2 = str(observation["job_scheduled2"]) == ("true")
|
|
executing1 = str(observation["job_executed1"]) == ("true")
|
|
executing2 = str(observation["job_executed2"]) == ("true")
|
|
|
|
cumulativeDraw += totalDraw
|
|
|
|
if rejected1:
|
|
householdWaitCounter[0] += 1
|
|
if maxWaitingTime < householdWaitCounter[0]:
|
|
maxWaitingTime = householdWaitCounter[0]
|
|
elif executing1:
|
|
householdWaitCounter[0] = 0
|
|
cumulativeRevenue += energyPrice
|
|
if rejected2:
|
|
householdWaitCounter[1] += 1
|
|
if maxWaitingTime < householdWaitCounter[1]:
|
|
maxWaitingTime = householdWaitCounter[1]
|
|
elif executing2:
|
|
householdWaitCounter[1] = 0
|
|
cumulativeRevenue += energyPrice
|
|
|
|
|
|
header = f" Timestep {i:03} Scheduler: {propertyForScheduling} ".center(80, '#')
|
|
return f"""
|
|
{header}
|
|
# #
|
|
# Current Draw : {totalDraw:02} Current Price : {energyPrice:02}{'#'.rjust(41)}
|
|
# Current Draw : {str('x'*totalDraw).ljust(20)}{'#'.rjust(42)}
|
|
# Current Price : {str('x'*energyPrice).ljust(20)}{'#'.rjust(42)}
|
|
{"Household 1:".ljust(30)}Household 2:
|
|
|
|
{"Scheduled".ljust(30) if scheduled1 else " ".ljust(30)} {"Scheduled".ljust(30) if scheduled2 else " ".ljust(30)}
|
|
{"Rejected".ljust(30) if rejected1 else " ".ljust(30)} {"Rejected".ljust(30) if rejected2 else " ".ljust(30)}
|
|
{"Executing".ljust(30) if executing1 else " ".ljust(30)} {"Executing".ljust(30) if executing2 else " ".ljust(30)}
|
|
Waiting Time: {str(householdWaitCounter[0]).ljust(15)} Waiting Time: {householdWaitCounter[1]}
|
|
|
|
Maximum Waiting Time : {maxWaitingTime}
|
|
Average Draw : {(cumulativeDraw / i):1.5f}
|
|
Revenue : {str(cumulativeRevenue).rjust(15)} Average Revenue per Timestep : {(cumulativeRevenue/i):1.5f}
|
|
|
|
# #
|
|
################################################################################
|
|
"""
|
|
|
|
def frame3(i, observation, propertyForScheduling,labels):
|
|
global cumulativeDraw
|
|
global cumulativeRevenue
|
|
global maxWaitingTime
|
|
energyPrice = int(str(observation['energy_price']))
|
|
totalDraw = int(str(observation['power_draw1'])) + int(str(observation['power_draw2'])) + int(str(observation['power_draw3']))
|
|
rejected1 = str(observation["job_rejected1"]) == ("true")
|
|
rejected2 = str(observation["job_rejected2"]) == ("true")
|
|
scheduled1 = str(observation["job_scheduled1"]) == ("true")
|
|
scheduled2 = str(observation["job_scheduled2"]) == ("true")
|
|
executing1 = str(observation["job_executed1"]) == ("true")
|
|
executing2 = str(observation["job_executed2"]) == ("true")
|
|
rejected3 = str(observation["job_rejected3"]) == ("true")
|
|
scheduled3 = str(observation["job_scheduled3"]) == ("true")
|
|
executing3 = str(observation["job_executed3"]) == ("true")
|
|
|
|
cumulativeDraw += totalDraw
|
|
|
|
if rejected1:
|
|
householdWaitCounter[0] += 1
|
|
if maxWaitingTime < householdWaitCounter[0]:
|
|
maxWaitingTime = householdWaitCounter[0]
|
|
elif executing1:
|
|
householdWaitCounter[0] = 0
|
|
cumulativeRevenue += energyPrice
|
|
if rejected2:
|
|
householdWaitCounter[1] += 1
|
|
if maxWaitingTime < householdWaitCounter[1]:
|
|
maxWaitingTime = householdWaitCounter[1]
|
|
elif executing2:
|
|
householdWaitCounter[1] = 0
|
|
cumulativeRevenue += energyPrice
|
|
if rejected3:
|
|
householdWaitCounter[2] += 1
|
|
if maxWaitingTime < householdWaitCounter[2]:
|
|
maxWaitingTime = householdWaitCounter[2]
|
|
elif executing3:
|
|
householdWaitCounter[2] = 0
|
|
cumulativeRevenue += energyPrice
|
|
|
|
|
|
header = f" Timestep {i:03} Scheduler: {propertyForScheduling} ".center(80, '#')
|
|
return f"""
|
|
{header}
|
|
# #
|
|
# Current Draw : {totalDraw:02} Current Price : {energyPrice:02}{'#'.rjust(41)}
|
|
# Current Draw : {str('x'*totalDraw).ljust(20)}{'#'.rjust(42)}
|
|
# Current Price : {str('x'*energyPrice).ljust(20)}{'#'.rjust(42)}
|
|
{"Household 1:".ljust(20)}{"Household 2:".ljust(20)}Household 3:
|
|
|
|
{"Scheduled".ljust(20) if scheduled1 else " ".ljust(20)} {"Scheduled".ljust(20) if scheduled2 else " ".ljust(20)} {"Scheduled".ljust(20) if scheduled3 else " ".ljust(20)}
|
|
{"Rejected".ljust(20) if rejected1 else " ".ljust(20)} {"Rejected".ljust(20) if rejected2 else " ".ljust(20)} {"Rejected".ljust(20) if rejected3 else " ".ljust(20)}
|
|
{"Executing".ljust(20) if executing1 else " ".ljust(20)} {"Executing".ljust(20) if executing2 else " ".ljust(20)} {"Executing".ljust(20) if executing3 else " ".ljust(20)}
|
|
Waiting Time: {str(householdWaitCounter[0]).ljust(15)} Waiting Time: {householdWaitCounter[1]}
|
|
|
|
Maximum Waiting Time : {maxWaitingTime}
|
|
Average Draw : {(cumulativeDraw / i):1.5f}
|
|
Revenue : {str(cumulativeRevenue).rjust(15)} Average Revenue per Timestep : {(cumulativeRevenue/i):1.5f}
|
|
|
|
# #
|
|
################################################################################
|
|
"""
|
|
|
|
|
|
def mdp():
|
|
global cumulativeDraw
|
|
global cumulativeRevenue
|
|
global maxWaitingTime
|
|
prism_program = stormpy.parse_prism_program("/media/mgm.prism")
|
|
|
|
# TODO: Add more properties here
|
|
formula_str = "R{\"energyPriceAndSatisfaction\"}max=? [ LRA ];"
|
|
formula_str += "Pmax=? [ G (totalDraw < 5) ];"
|
|
formula_str += "P=? [ F (job_rejected2 & job_rejected1) ];"
|
|
formulas = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
|
|
options = stormpy.BuilderOptions([p.raw_formula for p in formulas])
|
|
options.set_build_state_valuations(True)
|
|
options.set_build_choice_labels(True)
|
|
options.set_build_all_labels()
|
|
|
|
print(stormpy.build_model(prism_program))
|
|
model = stormpy.build_sparse_model_with_options(prism_program, options)
|
|
initial_state = model.initial_states[0]
|
|
assert initial_state == 0
|
|
# TODO: Adapt here to change to different scheduling
|
|
propertyForScheduling = formulas[0]
|
|
result = stormpy.model_checking(model, propertyForScheduling, extract_scheduler=True)
|
|
print("Result: {}".format(result.at(initial_state)))
|
|
assert result.has_scheduler
|
|
scheduler = result.scheduler
|
|
assert scheduler.memoryless
|
|
assert scheduler.deterministic
|
|
|
|
dtmc = model.apply_scheduler(scheduler)
|
|
# TODO: Add more calls to 'stormpy.model_checking(dtmc, ...)' here to check multiple properties
|
|
result = stormpy.model_checking(dtmc, formulas[-1])
|
|
print(dtmc)
|
|
print("Probability to reject both: {} (in induced Markov Chain)".format(result.at(initial_state)))
|
|
simulator = stormpy.simulator.create_simulator(dtmc)
|
|
simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL)
|
|
|
|
input("Hit enter to start the simulation.")
|
|
while True:
|
|
i=0
|
|
while i < 5000:
|
|
i += 1
|
|
observation, reward, labels = simulator.step()
|
|
print(frame3(i,observation,propertyForScheduling.raw_formula,labels))
|
|
input("Hit Enter to reset and start new run.")
|
|
simulator.restart()
|
|
householdWaitCounter = [0,0]
|
|
cumulativeDraw = 0
|
|
cumulativeRevenue = 0
|
|
maxWaitingTime = -1
|
|
|
|
|
|
|
|
|
|
if __name__ == '__main__':
|
|
mdp()
|