diff --git a/first_try.prism b/first_try.prism index ac112f8..d960fba 100644 --- a/first_try.prism +++ b/first_try.prism @@ -3,7 +3,7 @@ mdp const int initY = 40; const int initX = 80; -const int maxY = 560; +const int maxY = 180; const int minX = 4; const int maxX = 144; @@ -43,34 +43,34 @@ module skier passed_gate_4 : bool init false; passed_gate_5 : bool init false; - [g1_left] !passed_gate_1 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); - [g1_right] !passed_gate_1 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); - [g1_noop] !passed_gate_1 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + [left] !passed_gate_1 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + [right] !passed_gate_1 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + [noop] !passed_gate_1 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); - [g2_left] !passed_gate_2 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); - [g2_right] !passed_gate_2 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); - [g2_noop] !passed_gate_2 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + [left] !passed_gate_2 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + [right] !passed_gate_2 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + [noop] !passed_gate_2 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); - [g3_left] !passed_gate_3 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); - [g3_right] !passed_gate_3 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); - [g3_noop] !passed_gate_3 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + [left] !passed_gate_3 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + [right] !passed_gate_3 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + [noop] !passed_gate_3 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); - [g4_left] !passed_gate_4 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); - [g4_right] !passed_gate_4 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); - [g4_noop] !passed_gate_4 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + [left] !passed_gate_4 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + [right] !passed_gate_4 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + [noop] !passed_gate_4 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); - [g5_left] !passed_gate_5 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); - [g5_right] !passed_gate_5 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); - [g5_noop] !passed_gate_5 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + [left] !passed_gate_5 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + [right] !passed_gate_5 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + [noop] !passed_gate_5 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); [left] !done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); [right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); [noop] !done & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate)); - [left] done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); - [right] done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1); - [noop] done & move=0 -> (move'=1); - + //[left] done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); + //[right] done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1); + //[noop] done & move=0 -> (move'=1); + [done] done -> true; endmodule module updateY @@ -103,25 +103,25 @@ module updateX endmodule rewards - [g1_left] !passed_gate_1 & Passed_Gate_1: 100; - [g1_right] !passed_gate_1 & Passed_Gate_1: 100; - [g1_noop] !passed_gate_1 & Passed_Gate_1: 100; + [left] !passed_gate_1 & Passed_Gate_1: 100; + [right] !passed_gate_1 & Passed_Gate_1: 100; + [noop] !passed_gate_1 & Passed_Gate_1: 100; - [g2_left] !passed_gate_2 & Passed_Gate_2: 100; - [g2_right] !passed_gate_2 & Passed_Gate_2: 100; - [g2_noop] !passed_gate_2 & Passed_Gate_2: 100; + [left] !passed_gate_2 & Passed_Gate_2: 100; + [right] !passed_gate_2 & Passed_Gate_2: 100; + [noop] !passed_gate_2 & Passed_Gate_2: 100; - [g3_left] !passed_gate_3 & Passed_Gate_3: 100; - [g3_right] !passed_gate_3 & Passed_Gate_3: 100; - [g3_noop] !passed_gate_3 & Passed_Gate_3: 100; + [left] !passed_gate_3 & Passed_Gate_3: 100; + [right] !passed_gate_3 & Passed_Gate_3: 100; + [noop] !passed_gate_3 & Passed_Gate_3: 100; - [g4_left] !passed_gate_4 & Passed_Gate_4: 100; - [g4_right] !passed_gate_4 & Passed_Gate_4: 100; - [g4_noop] !passed_gate_4 & Passed_Gate_4: 100; + [left] !passed_gate_4 & Passed_Gate_4: 100; + [right] !passed_gate_4 & Passed_Gate_4: 100; + [noop] !passed_gate_4 & Passed_Gate_4: 100; - [g5_left] !passed_gate_5 & Passed_Gate_5: 100; - [g5_right] !passed_gate_5 & Passed_Gate_5: 100; - [g5_noop] !passed_gate_5 & Passed_Gate_5: 100; + [left] !passed_gate_5 & Passed_Gate_5: 100; + [right] !passed_gate_5 & Passed_Gate_5: 100; + [noop] !passed_gate_5 & Passed_Gate_5: 100; [left] !done & (Hit_Tree) : -100; [right] !done & (Hit_Tree) : -100; diff --git a/rom_evaluate.py b/rom_evaluate.py index e5d9c64..28e287e 100644 --- a/rom_evaluate.py +++ b/rom_evaluate.py @@ -25,14 +25,17 @@ from query_sample_factory_checkpoint import SampleFactoryNNQueryWrapper import time tempest_binary = "/home/spranger/projects/tempest-devel/ranking_release/bin/storm" -mdp_file = "simplified.prism" rom_file = "/home/spranger/research/Skiing/env/lib/python3.8/site-packages/AutoROM/roms/skiing.bin" + + class Verdict(Enum): INCONCLUSIVE = 1 GOOD = 2 BAD = 3 +verdict_to_color_map = {Verdict.BAD: "200,0,0", Verdict.INCONCLUSIVE: "40,40,200", Verdict.GOOD: "00,200,100"} + def convert(tuples): return dict(tuples) @@ -101,7 +104,7 @@ def drawImportantStates(important_states): ski_position_counter = {1: (Action.LEFT, 40), 2: (Action.LEFT, 35), 3: (Action.LEFT, 30), 4: (Action.LEFT, 10), 5: (Action.NOOP, 1), 6: (Action.RIGHT, 10), 7: (Action.RIGHT, 30), 8: (Action.RIGHT, 40) } def run_single_test(ale, nn_wrapper, x,y,ski_position, duration=200): - print(f"Running Test from x: {x:04}, y: {y:04}, ski_position: {ski_position}", end="") + #print(f"Running Test from x: {x:04}, y: {y:04}, ski_position: {ski_position}", end="") for i, r in enumerate(ramDICT[y]): ale.setRAM(i,r) ski_position_setting = ski_position_counter[ski_position] @@ -130,13 +133,13 @@ def run_single_test(ale, nn_wrapper, x,y,ski_position, duration=200): speed_list.append(ale.getRAM()[14]) if len(speed_list) > 15 and sum(speed_list[-6:-1]) == 0: return (Verdict.BAD, first_action) - time.sleep(0.005) + #time.sleep(0.005) return (Verdict.INCONCLUSIVE, first_action) def optimalAction(choices): return max(choices.items(), key=operator.itemgetter(1))[0] -def computeStateRanking(): +def computeStateRanking(mdp_file): command = f"{tempest_binary} --prism {mdp_file} --buildchoicelab --buildstateval --prop 'Rmax=? [C <= 1000]'" exec(command) @@ -160,18 +163,49 @@ def fillStateRanking(file_name, match=""): return state_ranking except EnvironmentError: - print("TODO file not available. Exiting.") + print("Ranking file not available. Exiting.") sys.exit(1) -computeStateRanking() -ranking = fillStateRanking("action_ranking") -sorted_ranking = sorted(ranking.items(), key=lambda x: x[1].ranking) + +fixed_left_states = list() +fixed_right_states = list() +fixed_noop_states = list() + +def populate_fixed_actions(state, action): + if action == Action.LEFT: + fixed_left_states.append(state) + if action == Action.RIGHT: + fixed_right_states.append(state) + if action == Action.NOOP: + fixed_noop_states.append(state) + +def update_prism_file(old_prism_file, new_prism_file): + fixed_left_formula = "formula Fixed_Left = false " + fixed_right_formula = "formula Fixed_Right = false " + fixed_noop_formula = "formula Fixed_Noop = false " + for state in fixed_left_states: + fixed_left_formula += f" | (x={state.x}&y={state.y}&ski_position={state.ski_position}) " + for state in fixed_right_states: + fixed_right_formula += f" | (x={state.x}&y={state.y}&ski_position={state.ski_position}) " + for state in fixed_noop_states: + fixed_noop_formula += f" | (x={state.x}&y={state.y}&ski_position={state.ski_position}) " + fixed_left_formula += ";\n" + fixed_right_formula += ";\n" + fixed_noop_formula += ";\n" + with open(f'{old_prism_file}', 'r') as file : + filedata = file.read() + if len(fixed_left_states) > 0: filedata = re.sub(r"^formula Fixed_Left =.*$", fixed_left_formula, filedata, flags=re.MULTILINE) + if len(fixed_right_states) > 0: filedata = re.sub(r"^formula Fixed_Right =.*$", fixed_right_formula, filedata, flags=re.MULTILINE) + if len(fixed_noop_states) > 0: filedata = re.sub(r"^formula Fixed_Noop =.*$", fixed_noop_formula, filedata, flags=re.MULTILINE) + with open(f'{new_prism_file}', 'w') as file: + file.write(filedata) + ale = ALEInterface() -if SDL_SUPPORT: - ale.setBool("sound", True) - ale.setBool("display_screen", True) +#if SDL_SUPPORT: +# ale.setBool("sound", True) +# ale.setBool("display_screen", True) # Load the ROM file ale.loadROM(rom_file) @@ -184,16 +218,34 @@ x = 70 nn_wrapper = SampleFactoryNNQueryWrapper() -exec("cp testing_1.png /dev/shm/testing.png") -for important_state in sorted_ranking[-100:-1]: - optimal_choice = optimalAction(important_state[1].choices) - #print(important_state[1].choices, f"\t\tOptimal: {optimal_choice}") - x = important_state[0].x - y = important_state[0].y - ski_pos = model_to_actual(important_state[0].ski_position) - action_taken = run_single_test(ale,nn_wrapper,x,y,ski_pos, duration=50) - print(f".... {action_taken}") - markerSize = 1 - marker = f"-fill 'rgba(255,204,0,{important_state[1].ranking})' -draw 'point {x},{y} '" - command = f"convert /dev/shm/testing.png {marker} /dev/shm/testing.png" - exec(command, verbose=False) +iteration = 0 +id = int(time.time()) +init_mdp = "velocity" +exec(f"mkdir -p images/testing_{id}") +exec(f"cp 1_full_scaled_down.png images/testing_{id}/testing_0000.png") +exec(f"cp {init_mdp}.prism {init_mdp}_000.prism") + +markerSize = 1 +markerList = {1: list(), 2:list(), 3:list(), 4:list(), 5:list(), 6:list(), 7:list(), 8:list()} + +while True: + computeStateRanking(f"{init_mdp}_{iteration:03}.prism") + ranking = fillStateRanking("action_ranking") + sorted_ranking = sorted(ranking.items(), key=lambda x: x[1].ranking) + for important_state in sorted_ranking[-100:-1]: + optimal_choice = optimalAction(important_state[1].choices) + #print(important_state[1].choices, f"\t\tOptimal: {optimal_choice}") + x = important_state[0].x + y = important_state[0].y + ski_pos = model_to_actual(important_state[0].ski_position) + result = run_single_test(ale,nn_wrapper,x,y,ski_pos, duration=50) + #print(f".... {result}") + marker = f"-fill 'rgba({verdict_to_color_map[result[0]],0.7})' -draw 'rectangle {x-markerSize},{y-markerSize} {x+markerSize},{y+markerSize} '" + markerList[ski_pos].append(marker) + populate_fixed_actions(important_state[0], result[1]) + for pos, marker in markerList.items(): + command = f"convert images/testing_{id}/testing_0000.png {' '.join(marker)} images/testing_{id}/testing_{iteration+1:03}_{pos:02}.png" + exec(command, verbose=False) + exec(f"montage images/testing_{id}/testing_{iteration+1:03}_*png -geometry +0+0 -tile x1 images/testing_{id}/{iteration+1:03}.png", verbose=False) + iteration += 1 + update_prism_file(f"{init_mdp}_{iteration-1:03}.prism", f"{init_mdp}_{iteration:03}.prism") diff --git a/simplified.prism b/simplified.prism index 06bccc6..c429c1d 100644 --- a/simplified.prism +++ b/simplified.prism @@ -3,12 +3,12 @@ mdp const int initY = 40; const int initX = 80; -const int maxY = 600; +const int maxY = 210; const int minX = 4; const int maxX = 144; -formula Gate_1 = ((x=41 | x=73) & y=168); +formula Gate_1 = ((42361; formula Left_Gate_4 = y>454; formula Left_Gate_5 = y>546; -formula Tree_1 = ((x>=124 & x<=134) & (y>=190 & y<=200)); +formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200)); formula Tree_2 = ((x>=32 & x<=42) & (y>=287 & y<=297)); formula Tree_3 = ((x>=28 & x<=38) & (y>=317 & y<=327)); formula Tree_4 = ((x>=12 & x<=22) & (y>=408 & y<=418)); @@ -37,32 +37,42 @@ formula Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5; formula Passed_Gate = Passed_Gate_1 | Passed_Gate_2 | Passed_Gate_3 | Passed_Gate_4 | Passed_Gate_5; formula Left_Gate = Left_Gate_1 | Left_Gate_2 | Left_Gate_3 | Left_Gate_4 | Left_Gate_5; +init + move=0 & !done & !passed_gate & standstill=0 +endinit -global move : [0..3] init 0; + +global move : [0..3]; + +formula Fixed_Left = false; +formula Fixed_Right = false; +formula Fixed_Noop = false; +formula Fixed = Fixed_Left | Fixed_Right | Fixed_Noop; module skier - ski_position : [1..14] init 8; - done : bool init false; + ski_position : [1..14] ; + done : bool ; + + passed_gate : bool ; - passed_gate : bool init false; + [left] !Fixed & !passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); + [right] !Fixed & !passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); + [noop] !Fixed & !passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); - [left] !passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); - [right] !passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); - [noop] !passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); + [left] !Fixed & passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [right] !Fixed & passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [noop] !Fixed & passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); - [left] passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); - [right] passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); - [noop] passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [left] Fixed_Left & move=0 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [right] Fixed_Right & move=0 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [noop] Fixed_Noop & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); - //[left] done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); - //[right] done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1); - //[noop] done & move=0 -> (move'=1); [done] done -> true; endmodule module updateY - y : [initY..maxY] init initY; - standstill : [0..8] init 0; + y : [initY..maxY] ; + standstill : [0..8] ; [update_y] move=1 & (ski_position=1 | ski_position = 14) & standstill>=5 -> (y'=y) & (standstill'=min(8,standstill+1)) & (move'=2); [update_y] move=1 & (ski_position=1 | ski_position = 14) & standstill<5 -> (y'=min(maxY,y+4)) & (standstill'=min(8,standstill+1)) & (move'=2); [update_y] move=1 & (ski_position=2 | ski_position = 3 | ski_position = 12 | ski_position = 13) -> (y'=min(maxY,y+8)) & (standstill'=0) & (move'=2); @@ -71,7 +81,7 @@ module updateY endmodule module updateX - x : [minX..maxX] init initX; + x : [minX..maxX] ; [update_x] move=2 & standstill>=8 -> (move'=0); [update_x] move=2 & standstill<8 & (ski_position=7 | ski_position=8) -> (move'=0); diff --git a/test_model.py b/test_model.py index 36d1135..284d747 100644 --- a/test_model.py +++ b/test_model.py @@ -5,20 +5,31 @@ from os import listdir, system from os.path import isfile, join, getctime from dataclasses import dataclass, field -ski_position_to_rgb_map = {1: "230, 138, 0", - 2: "255,153,0", - 3: "255, 184, 77", - 4: "255, 194, 100", - 5: "255, 194, 120", - 6: "255, 210, 130", - 7: "255, 210, 140", - 8: "230, 204, 255", - 9: "204, 153, 255", - 10: "255, 102, 179", - 11: "255, 51, 153", - 12: "255, 0, 255", - 13: "179, 0, 179", - 14: "102, 0, 102"} +ski_position_to_rgb_map = {1: "230, 138, 0", 2: "255,153,0", 3: "255, 184, 77", 4: "255, 194, 100", 5: "255, 194, 120", 6: "255, 210, 130", 7: "255, 210, 140", 8: "230, 204, 255", 9: "204, 153, 255", 10: "255, 102, 179", 11: "255, 51, 153", 12: "255, 0, 255", 13: "179, 0, 179", 14: "102, 0, 102"} + +def importance_color(ranking_value): + low = 0x00ff00 + high = 0xff0000 + result = int(ranking_value * high + (1-ranking_value) * low) + return f"#{result:06x}" + +def model_to_actual(ski_position): + if ski_position == 1: + return 1 + elif ski_position in [2,3]: + return 2 + elif ski_position in [4,5]: + return 3 + elif ski_position in [6,7]: + return 4 + elif ski_position in [8,9]: + return 5 + elif ski_position in [10,11]: + return 6 + elif ski_position in [12,13]: + return 7 + elif ski_position == 14: + return 8 def convert(tuples): return dict(tuples) @@ -35,8 +46,8 @@ def default_value(): class StateValue: ranking: float choices: dict = field(default_factory=default_value) -def exec(command): - print(f"Executing {command}") +def exec(command, verbose=True): + if verbose: print(f"Executing {command}") system(f"echo {command} >> list_of_exec") return system(command) @@ -62,17 +73,27 @@ def fillStateRanking(file_name, match=""): print("TODO file not available. Exiting.") sys.exit(1) -ranking = fillStateRanking("action_ranking") +ranking = fillStateRanking("action_ranking_simplified") sorted_ranking = sorted(ranking.items(), key=lambda x: x[1].ranking) -draw_commands = list() - -for state in sorted_ranking[-20:-1]: - print(state) +draw_commands = {1: list(), 2:list(), 3:list(), 4:list(), 5:list(), 6:list(), 7:list(), 8:list()} +exec(f"cp images/empty_scaled_down.png full_first_try_safety.png") +markerSize = 1 +for state in sorted_ranking[-500000:-1]: + if state[1].ranking < 0.09: continue x = state[0].x y = state[0].y - markerSize = 2 - print(state[0].ski_position) - draw_commands.append(f"-fill 'rgba({ski_position_to_rgb_map[state[0].ski_position]},0.7)' -draw 'rectangle {x-markerSize},{y-markerSize} {x+markerSize},{y+markerSize} '") -command = f"convert init.png {' '.join(draw_commands)} first_try.png" -exec(command) + ski_position = state[0].ski_position + draw_commands[ski_position].append(f"-fill '{importance_color(state[1].ranking)}' -draw 'rectangle {x-markerSize},{y-markerSize} {x+markerSize},{y+markerSize}'") # {state[1].ranking} +for pos, marker in draw_commands.items(): + destination = f"first_try_{pos:02}.png" + exec(f"cp images/empty_scaled_down.png {destination}") + i=0 + while i < len(marker): + batch = marker[i:i+1000] + command = f"convert {destination} {' '.join(batch)} {destination}" + exec(command, verbose=False) + command = f"convert full_first_try_safety.png {' '.join(batch)} full_first_try_safety.png" + exec(command, verbose=False) + i = i+1000 +exec(f"montage first_try*.png -geometry +0+0 -tile x1 tiled_first_try.png") diff --git a/velocity.prism b/velocity.prism index f40366f..c4fb6c2 100644 --- a/velocity.prism +++ b/velocity.prism @@ -3,22 +3,23 @@ mdp const int initY = 40; const int initX = 80; -const int maxY = 210; -const int minX = 4; +const int maxY = 580; +const int minX = 10; const int maxX = 144; -formula Gate_1 = ((4241 & x<73) & (y>160 & y<176)); //(y=168)); -formula Passed_Gate_2 = ((x>71 & x<104) & (y>253 & y<269)); //(y=261)); -formula Passed_Gate_3 = ((x>81 & x<113) & (y>345 & y<361)); //(y=353)); -formula Passed_Gate_4 = ((x>55 & x<88) & (y>438 & y<454)); //(y=446)); -formula Passed_Gate_5 = ((x>79 & x<110) & (y>530 & y<546)); //(y=538)); + +formula Passed_Gate_1 = ((x>46 & x<78) & (y>160 & y<176)); //(y=168)); +formula Passed_Gate_2 = ((x>76 & x<108) & (y>253 & y<269)); //(y=261)); +formula Passed_Gate_3 = ((x>84 & x<116) & (y>345 & y<361)); //(y=353)); +formula Passed_Gate_4 = ((x>58 & x<92) & (y>438 & y<454)); //(y=446)); +formula Passed_Gate_5 = ((x>84 & x<116) & (y>530 & y<546)); //(y=538)); formula Left_Gate_1 = y>176; formula Left_Gate_2 = y>269; formula Left_Gate_3 = y>361; @@ -26,11 +27,11 @@ formula Left_Gate_4 = y>454; formula Left_Gate_5 = y>546; formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200)); -formula Tree_2 = ((x>=32 & x<=42) & (y>=287 & y<=297)); -formula Tree_3 = ((x>=28 & x<=38) & (y>=317 & y<=327)); -formula Tree_4 = ((x>=12 & x<=22) & (y>=408 & y<=418)); -formula Tree_5 = ((x>=129 & x<=139) & (y>=468 & y<=480)); -formula Tree_6 = ((x>=140 & x<=144) & (y>=496 & y<=510)); +formula Tree_2 = ((x>=32 & x<=49) & (y>=284 & y<=295)); +formula Tree_3 = ((x>=30 & x<=49) & (y>=317 & y<=327)); +formula Tree_4 = ((x>=12 & x<=30) & (y>=408 & y<=418)); +formula Tree_5 = ((x>=129 & x<=146) & (y>=468 & y<=480)); +formula Tree_6 = ((x>=140 & x<=152) & (y>=496 & y<=510)); formula Hit_Tree = Tree_1 | Tree_2 | Tree_3 | Tree_4 | Tree_5 | Tree_6; formula Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5; @@ -47,17 +48,17 @@ formula Fixed_Noop = false; formula Fixed = Fixed_Left | Fixed_Right | Fixed_Noop; module skier - ski_position : [1..14] ; + ski_position : [1..8] ; done : bool ; passed_gate : bool ; [left] !Fixed & !passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); - [right] !Fixed & !passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); + [right] !Fixed & !passed_gate & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); [noop] !Fixed & !passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate)); [left] !Fixed & passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); - [right] !Fixed & passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); + [right] !Fixed & passed_gate & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); [noop] !Fixed & passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); [left] Fixed_Left & move=0 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate)); @@ -75,36 +76,33 @@ module updateY [update_y] move=1 & standstill>=5 -> (y'=y) & (move'=2); [update_y] move=1 & standstill<5 -> (y'=min(maxY,y+velocity)) & (move'=2); - [update_y] move=2 & (ski_position=1 | ski_position = 14) & standstill>=5 -> (standstill'=min(8,standstill+1)) & (move'=3); - [update_y] move=2 & (ski_position=1 | ski_position = 14) & standstill<5 -> (velocity'=max(0,velocity-4)) &(move'=3); - [update_y] move=2 & (ski_position=2 | ski_position = 3 | ski_position = 12 | ski_position = 13) -> (velocity'=max(0 ,velocity-2)) & (standstill'=0) & (move'=3); - [update_y] move=2 & (ski_position=4 | ski_position = 5 | ski_position = 10 | ski_position = 11) -> (velocity'=min(16,velocity+2)) & (standstill'=0) & (move'=3); - [update_y] move=2 & (ski_position=6 | ski_position = 7 | ski_position = 8 | ski_position = 9) -> (velocity'=min(16,velocity+4)) & (standstill'=0) & (move'=3); + [update_y] move=2 & (ski_position=1 | ski_position = 8) & standstill>=5 -> (standstill'=min(8,standstill+1)) & (move'=3); + [update_y] move=2 & (ski_position=1 | ski_position = 8) & standstill<5 -> (velocity'=max(0,velocity-4)) &(move'=3); + [update_y] move=2 & (ski_position=2 | ski_position = 7) -> (velocity'=max(0 ,velocity-2)) & (standstill'=0) & (move'=3); + [update_y] move=2 & (ski_position=3 | ski_position = 6) -> (velocity'=min(8,velocity+2)) & (standstill'=0) & (move'=3); + [update_y] move=2 & (ski_position=4 | ski_position = 5) -> (velocity'=min(8,velocity+4)) & (standstill'=0) & (move'=3); endmodule module updateX x : [minX..maxX] ; [update_x] move=3 & standstill>=8 -> (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=7 | ski_position=8) -> (move'=0); - - [update_x] move=3 & standstill<8 & ski_position=6 -> 0.1: (x'=max(minX,x-2)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-6)) & (move'=0); - [update_x] move=3 & standstill<8 & ski_position=9 -> 0.1: (x'=min(maxX,x+2)) + 0.7: (x'=min(maxX,x+4)) + 0.2: (x'=min(maxX,x+6)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=4 | ski_position=5) -> (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=4 | ski_position=5) -> 0.1: (x'=max(minX,x-4)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-8)) & (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=10 | ski_position=11) -> 0.1: (x'=min(maxX,x+4)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+8)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=3) -> 0.4: (x'=max(minX,x-0)) & (move'=0) + 0.6: (x'=max(minX,x-1)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=6) -> 0.4: (x'=min(maxX,x+0)) & (move'=0) + 0.6: (x'=min(maxX,x+1)) & (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=2 | ski_position=3) -> 0.1: (x'=max(minX,x-4)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-8)) & (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=12 | ski_position=13) -> 0.1: (x'=min(maxX,x+4)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+8)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=2) -> 0.3: (x'=max(minX,x-0)) & (move'=0) + 0.7: (x'=max(minX,x-1)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=7) -> 0.3: (x'=min(maxX,x+0)) & (move'=0) + 0.7: (x'=min(maxX,x+1)) & (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=1) -> 0.1: (x'=max(minX,x-0)) + 0.7: (x'=max(minX,x-2)) + 0.2: (x'=max(minX,x-4)) & (move'=0); - [update_x] move=3 & standstill<8 & (ski_position=14) -> 0.1: (x'=min(maxX,x+0)) + 0.7: (x'=min(maxX,x+2)) + 0.2: (x'=min(maxX,x+4)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=1) -> 0.2: (x'=max(minX,x-0)) & (move'=0) + 0.8: (x'=max(minX,x-1)) & (move'=0); + [update_x] move=3 & standstill<8 & (ski_position=8) -> 0.2: (x'=min(maxX,x+0)) & (move'=0) + 0.8: (x'=min(maxX,x+1)) & (move'=0); endmodule rewards - [left] !passed_gate & standstill<2 & Passed_Gate: 100; - [right] !passed_gate & standstill<2 & Passed_Gate: 100; - [noop] !passed_gate & standstill<2 & Passed_Gate: 100; + //[left] !passed_gate & standstill<2 & Passed_Gate: 100; + //[right] !passed_gate & standstill<2 & Passed_Gate: 100; + //[noop] !passed_gate & standstill<2 & Passed_Gate: 100; [left] !done & (Hit_Tree) : -100; [right] !done & (Hit_Tree) : -100;