From bc6d574ed6f8df9efb7ef6f28aff25ee326e2bd5 Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 17 Jun 2024 16:44:03 +0200 Subject: [PATCH] added files for HW9 --- car_pedestrian_mdp.prism | 59 ++++++++++++++++++ car_pedestrian_simulator.py | 64 +++++++++++++++++++ task_scheduling.prism | 118 +++++++++++++++++++++++++++++++++++ task_scheduling_simulator.py | 71 +++++++++++++++++++++ 4 files changed, 312 insertions(+) create mode 100644 car_pedestrian_mdp.prism create mode 100644 car_pedestrian_simulator.py create mode 100644 task_scheduling.prism create mode 100644 task_scheduling_simulator.py diff --git a/car_pedestrian_mdp.prism b/car_pedestrian_mdp.prism new file mode 100644 index 0000000..43951e6 --- /dev/null +++ b/car_pedestrian_mdp.prism @@ -0,0 +1,59 @@ +mdp + +const int lanes = 5; // Counting the sidewalks as lanes +const int streetLength = 20; + +const int maxVelocity = 3; +const int minVelocity = 1; + +const int carLaneInit = 2; +const double probFalling = 2/9; + +global move : [0..1] init 0; // 0: car 1: pedestrian + +formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = streetLength; + +formula car_at_end = car_street_pos = streetLength; + +// check ped within [car_pos-velocity..car_pos], same lane +formula crash_straight = (car_lane_pos=ped_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); +// check ped street pos within [car_street_pos-velocity..car_street_pos], ped lane pos within [car_lane_pos-1..car_lane_pos] +formula crash_left = (switched_left & ped_lane_pos>=car_lane_pos-1 & ped_lane_pos<=car_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); +// check ped street pos within [car_street_pos-velocity..car_street_pos], ped lane pos within [car_lane_pos+1..car_lane_pos] +formula crash_right = (switched_right & ped_lane_pos>=car_lane_pos+1 & ped_lane_pos<=car_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); + +label "crashed" = crash_straight | crash_left | crash_right; +label "maxedOut" = velocity=maxVelocity; +label "pedCrossed" = ped_lane_pos=lanes; + +module car + +switched_right : bool init false; +switched_left : bool init false; + +car_street_pos : [0..streetLength] init 0; +car_lane_pos : [2..lanes-1] init carLaneInit; +velocity : [minVelocity..maxVelocity] init minVelocity; + +// TODO + +endmodule + + +module pedestrian + +ped_street_pos : [0..streetLength] init floor(streetLength/4); +ped_lane_pos : [1..lanes] init 1; +fell_down : [0..2] init 0; // 1-2: getting up + +[move] move=1 & fell_down=0 -> ((1-probFalling)/4): (ped_lane_pos'=min(lanes,ped_lane_pos+1)) & (move'=0) + + ((1-probFalling)/4): (ped_lane_pos'=max(1,ped_lane_pos-1)) & (move'=0) + + ((1-probFalling)/4): (ped_street_pos'=min(lanes,ped_street_pos+1)) & (move'=0) + + ((1-probFalling)/4): (ped_street_pos'=max(1,ped_street_pos-1)) & (move'=0) + + (probFalling/4): (ped_lane_pos'=min(lanes,ped_lane_pos+1)) & (fell_down'=2) & (move'=0) + + (probFalling/4): (ped_lane_pos'=max(1,ped_lane_pos-1)) & (fell_down'=2) & (move'=0) + + (probFalling/4): (ped_street_pos'=min(lanes,ped_street_pos+1)) & (fell_down'=2) & (move'=0) + + (probFalling/4): (ped_street_pos'=max(1,ped_street_pos-1)) & (fell_down'=2) & (move'=0); +[getUp] move=1 & fell_down>0 -> 1: (fell_down'=fell_down-1) & (move'=0); + +endmodule diff --git a/car_pedestrian_simulator.py b/car_pedestrian_simulator.py new file mode 100644 index 0000000..d982f01 --- /dev/null +++ b/car_pedestrian_simulator.py @@ -0,0 +1,64 @@ +import stormpy +import stormpy.simulator + +newline = "\n" + +def printFrame(streetLength, lanes, carPos, pedPos): + sidewalk = "#" * (streetLength+1) + frame = list(sidewalk + (lanes-2)*("_"*(streetLength+1)) + sidewalk) + + frame[(int(carPos[0])-1)*(streetLength+1)+int(carPos[1])+1] = "C" + frame[(int(pedPos[0])-1)*(streetLength+1)+int(pedPos[1])+1] = "P" + for i in range(lanes): + frame[i*(streetLength+1)] = newline + return "".join(frame) + +def mdp(): + options = stormpy.BuilderOptions([]) + options.set_build_state_valuations(True) + options.set_build_choice_labels(True) + options.set_build_all_labels() + prism_program = stormpy.parse_prism_program("/media/car_pedestrian_mdp.prism") + + streetLength = int(str(prism_program.get_constant("streetLength").definition)) + lanes = int(str(prism_program.get_constant("lanes").definition)) + formula_str = "Pmax=? [G !\"crashed\" ];" + #formula_str = "Pmax=? [F \"crashed\" ];" + + print(stormpy.build_model(prism_program)) + formulas = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + model = stormpy.build_sparse_model_with_options(prism_program, options) + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + assert result.has_scheduler + scheduler = result.scheduler + assert scheduler.memoryless + assert scheduler.deterministic + + dtmc = model.apply_scheduler(scheduler) + print(dtmc) + simulator = stormpy.simulator.create_simulator(dtmc, seed=42) + simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) + + i=0 + while True: + observation, reward, labels = simulator.step() + print(observation, labels) + frame = printFrame(int(streetLength), int(lanes), (observation["car_lane_pos"], observation["car_street_pos"]), (observation["ped_lane_pos"], observation["ped_street_pos"])) + print(frame) + if simulator.is_done() or "pedCrossed" in labels: + print("Pedestrian arrived on the other side!") + break + input("") + with open(f"/media/frame{i:03}.txt", "w") as text_file: + text_file.write(frame) + i+=1 + if "crashed" in labels: + print("Pedestrian did not arrive on the other side!") + break + + + +if __name__ == '__main__': + mdp() diff --git a/task_scheduling.prism b/task_scheduling.prism new file mode 100644 index 0000000..5014cd4 --- /dev/null +++ b/task_scheduling.prism @@ -0,0 +1,118 @@ +mdp + +const int MULT_DUR_1 = 8; +const int ADD_DUR_1 = 4; +const double P1_SUCCESS = 1.0; +const int MULT_DUR_2 = 3; +const int ADD_DUR_2 = 3; +const double P2_SUCCESS = 0.8; + +// target state (all tasks complete) +label "tasks_complete" = (task6=3); +label "no_P1_mult" = (mult_tick_1=0); +label "no_P2_mult" = (mult_tick_2=0); + +// reward structure: elapsed time +rewards "time" + task6!=3 : 1; +endrewards + +// reward structures: energy consumption +rewards "energy" + p1=0 : 10/1000; // processor 1 idle + p1>0 : 100/1000; // processor 1 working + p2=0 : 10/1000; // processor 2 idle + p2>0 : 100/1000; // processor 2 working +endrewards + +module scheduler + +//┌t1─┐ ┌t3─────┐ ┌t5───────┐ +//│A+B│-->│Cx(A+B)│-->│DxCx(A+B)│--. ┌t6─────────────────────┐ +//└───┘\ └───────┘ └─────────┘ \___\│DxCx(A+B)+((A+B)+(CxD))│ +//┌t2─┐ \ ┌t4─────────┐ / /└───────────────────────┘ +//│CxD│-->│(A+B)+(CxD)│------------° +//└───┘ └───────────┘ + +task1 : [0..3]; // A+B, add +task2 : [0..3]; // CxD, mult +task3 : [0..3]; // Cx(A+B), mult +task4 : [0..3]; // (A+B)+(CxD), add +task5 : [0..3]; // DxCx(A+B), mult +task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)), add + +p1_idle : bool init true; +p2_idle : bool init true; + +// task status: +// 0 - not started +// 1 - running on processor 1 +// 2 - running on processor 2 +// 3 - task complete + +// start task 1 +[t1p1] task1=0 & p1_idle-> (task1'=1) & (p1_idle'=false); +[t1p2] task1=0 & p2_idle-> (task1'=2) & (p2_idle'=false); + +// start task 2 +[t2p1] task2=0 & p1_idle-> (task2'=1) & (p1_idle'=false); +[t2p2] task2=0 & p2_idle-> (task2'=2) & (p2_idle'=false); + +// start task 3 (must wait for task 1 to complete) +[t3p1] task3=0 & task1=3 & p1_idle-> (task3'=1) & (p1_idle'=false); +[t3p2] task3=0 & task1=3 & p2_idle-> (task3'=2) & (p2_idle'=false); + +// start task 4 (must wait for tasks 1 and 2 to complete) +[t4p1] task4=0 & task1=3 & task2=3 & p1_idle-> (task4'=1) & (p1_idle'=false); +[t4p2] task4=0 & task1=3 & task2=3 & p2_idle-> (task4'=2) & (p2_idle'=false); + +// start task 5 (must wait for task 3 to complete) +[t5p1] task5=0 & task3=3 & p1_idle-> (task5'=1) & (p1_idle'=false); +[t5p2] task5=0 & task3=3 & p2_idle-> (task5'=2) & (p2_idle'=false); + +// start task 6 (must wait for tasks 4 and 5 to complete) +[t6p1] task6=0 & task4=3 & task5=3 & p1_idle -> (task6'=1) & (p1_idle'=false); +[t6p2] task6=0 & task4=3 & task5=3 & p2_idle -> (task6'=2) & (p2_idle'=false); + +// a task finishes on processor 1 +[p1_done] task1=1 & p1=3 -> (task1'=3) & (p1_idle'=true); +[p1_done] task2=1 & p1=3 -> (task2'=3) & (p1_idle'=true); +[p1_done] task3=1 & p1=3 -> (task3'=3) & (p1_idle'=true); +[p1_done] task4=1 & p1=3 -> (task4'=3) & (p1_idle'=true); +[p1_done] task5=1 & p1=3 -> (task5'=3) & (p1_idle'=true); +[p1_done] task6=1 & p1=3 -> (task6'=3) & (p1_idle'=true); + +// a task finishes on processor 2 +[p2_done] task1=2 & p2=3 -> (task1'=3) & (p2_idle'=true); +[p2_done] task2=2 & p2=3 -> (task2'=3) & (p2_idle'=true); +[p2_done] task3=2 & p2=3 -> (task3'=3) & (p2_idle'=true); +[p2_done] task4=2 & p2=3 -> (task4'=3) & (p2_idle'=true); +[p2_done] task5=2 & p2=3 -> (task5'=3) & (p2_idle'=true); +[p2_done] task6=2 & p2=3 -> (task6'=3) & (p2_idle'=true); + +[] task6=3 -> 1 : true; +[] task6=3 -> 1 : true; + +endmodule + +// processor 1 +module P1 + p1 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done + mult_tick_1 : ; + add_tick_1 : ; + + [p1_done] p1=3 -> 1: (p1'=0) & (mult_tick_1'=0) & (add_tick_1'=0); // finished task + +endmodule + +// processor 2 +// Note: You may also use module renaming to define processor 2 +module P2 + p2 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done + mult_tick_2 : ; + add_tick_2 : ; + + + [p2_done] p2=3 -> 1: (p2'=0) & (mult_tick_2'=0) & (add_tick_2'=0); // finished task + +endmodule diff --git a/task_scheduling_simulator.py b/task_scheduling_simulator.py new file mode 100644 index 0000000..2aa089a --- /dev/null +++ b/task_scheduling_simulator.py @@ -0,0 +1,71 @@ +import stormpy +import stormpy.simulator + + +def mdp(): + options = stormpy.BuilderOptions([]) + options.set_build_state_valuations(True) + options.set_build_choice_labels(True) + options.set_build_all_labels() + options.set_build_all_reward_models() + + program = stormpy.parse_prism_program("/media/task_graph_scheduling.prism") + formula_str = "R{\"time\"}min=? [ F \"tasks_complete\" ];" + formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + model = stormpy.build_sparse_model_with_options(program, options) + print(model) + + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + assert result.has_scheduler + scheduler = result.scheduler + assert scheduler.memoryless + assert scheduler.deterministic + + dtmc = model.apply_scheduler(scheduler) + print(dtmc) + simulator = stormpy.simulator.create_simulator(dtmc, seed=42) + simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) + + step_counter = 0 + busy1_counter = 0 + busy2_counter = 0 + print(""" + ┌t1─┐ ┌t3─────┐ ┌t5───────┐ + │A+B│-->│Cx(A+B)│-->│DxCx(A+B)│--. ┌t6─────────────────────┐ + └───┘\ └───────┘ └─────────┘ \___\│DxCx(A+B)+((A+B)+(CxD))│ + ┌t2─┐ \ ┌t4─────────┐ / /└───────────────────────┘ + │CxD│-->│(A+B)+(CxD)│------------° + └───┘ └───────────┘ + """) + print(" " * 32 + "[+,x,x,+,x,+]") + while True: + if simulator.is_done(): + print(f"Tasks complete! Ratio: (approx.): {busy1_counter/(busy1_counter+busy2_counter):1.4f}/{busy2_counter/(busy1_counter+busy2_counter):1.4f}, Steps needed (approx.): {step_counter}") + break + observation, reward, labels = simulator.step() + #input("") + busy1 = str(observation["p1_idle"]) != ("true") + busy2 = str(observation["p2_idle"]) != ("true") + if busy1: busy1_counter += 1 + if busy2: busy2_counter += 1 + tasks = [str(observation[f"task{i}"]) for i in range(1,7)] + print(f"Step {step_counter:3}: P1/2:{'busy' if busy1 else 'idle'}/{'busy' if busy2 else 'idle'} tasks: [{','.join(tasks)}], {str(observation['add_tick_1'])},{str(observation['mult_tick_1'])},{str(observation['add_tick_2'])},{str(observation['mult_tick_2'])},labels: {labels if len(labels) != 0 else ''}, ") + step_counter += 1 + try: + with open("/media/induced_scheduling_dtmc.dot", "w") as text_file: + text_file.write(dtmc.to_dot()) + except Exception as e: + print(e) + print("Could not write to file.") + input("Hit enter to evaluate: 'P=? [ F<={i} \"tasks_complete\" ]' on the DTMC:") + print(dtmc) + + for i in range(30,61): + formula_str = f"P=? [ F<={i} \"tasks_complete\" ]" + formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + result = stormpy.model_checking(dtmc, formulas[0]) + print(f"Probability to finish within {i} timesteps : {result.at(dtmc.initial_states[0]):>1.12f}") +if __name__ == '__main__': + mdp()