From 8f7efe48db1cc8c333d6715b045605d39f521bfa Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 11 Sep 2023 16:02:23 +0200 Subject: [PATCH] initial commit, testing only --- first_try.prism | 71 ++++++++++++++++++++++++++++++++++++++++++++ test.py | 78 +++++++++++++++++++++++++++++++++++++++++++++++++ test_model.py | 78 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 227 insertions(+) create mode 100644 first_try.prism create mode 100644 test.py create mode 100644 test_model.py diff --git a/first_try.prism b/first_try.prism new file mode 100644 index 0000000..339b125 --- /dev/null +++ b/first_try.prism @@ -0,0 +1,71 @@ +mdp + +const int initY = 40; +const int initX = 80; + +const int maxY = 240; +const int minX = 12; +const int maxX = 147; + + +formula HitTree = (1221 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate)); + [right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate)); + [noop] !done & move=0 -> (move'=1) & (done'=(PassedGates|HitTree|HitGate)); + + [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); + +endmodule + +module updateY + y : [initY..maxY] init initY; + standstill : [0..8] init 0; + [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); + [update_y] move=1 & (ski_position=4 | ski_position = 5 | ski_position = 10 | ski_position = 11) -> (y'=min(maxY,y+12)) & (standstill'=0) & (move'=2); + [update_y] move=1 & (ski_position=6 | ski_position = 7 | ski_position = 8 | ski_position = 9) -> (y'=min(maxY,y+16)) & (standstill'=0) & (move'=2); +endmodule + +module updateX + x : [minX..maxX] init initX; + + [update_x] move=2 & standstill>=8 -> (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=7 | ski_position=8) -> (move'=0); + + [update_x] move=2 & standstill<8 & ski_position=6 -> 0.1: (x'=max(minX,x-3)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-5)) & (move'=0); + [update_x] move=2 & standstill<8 & ski_position=9 -> 0.1: (x'=min(maxX,x+3)) + 0.7: (x'=min(maxX,x+4)) + 0.2: (x'=min(maxX,x+5)) & (move'=0); + + [update_x] move=2 & standstill<8 & (ski_position=4 | ski_position=5) -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=10 | ski_position=11) -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (move'=0); + + [update_x] move=2 & standstill<8 & (ski_position=2 | ski_position=3) -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=12 | ski_position=13) -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (move'=0); + + [update_x] move=2 & 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-3)) & (move'=0); + [update_x] move=2 & 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+3)) & (move'=0); +endmodule + +rewards + [left] !done & PassedGates : 100; + [right] !done & PassedGates : 100; + [noop] !done & PassedGates : 100; + [left] !done & (HitTree) : -200; + [right] !done & (HitTree) : -200; + [noop] !done & (HitTree) : -200; + [left] !done & (HitGate) : -150; + [right] !done & (HitGate) : -150; + [noop] !done & (HitGate) : -150; +endrewards diff --git a/test.py b/test.py new file mode 100644 index 0000000..6401f41 --- /dev/null +++ b/test.py @@ -0,0 +1,78 @@ +import gym +from PIL import Image +from copy import deepcopy +import numpy as np + +from matplotlib import pyplot as plt +import readchar + +import queue + +ski_position_queue = queue.Queue() + +env = gym.make("ALE/Skiing-v5", render_mode="human") + + +observation, info = env.reset() +y = 40 + + +standstillcounter = 0 +def update_y(y, ski_position): + global standstillcounter + if ski_position in [6,7, 8,9]: + standstillcounter = 0 + y_update = 16 + elif ski_position in [4,5, 10,11]: + standstillcounter = 0 + y_update = 12 + elif ski_position in [2,3, 12,13]: + standstillcounter = 0 + y_update = 8 + elif ski_position in [1, 14] and standstillcounter >= 5: + if standstillcounter >= 8: + print("!!!!!!!!!! no more x updates!!!!!!!!!!!") + y_update = 0 + elif ski_position in [1, 14]: + y_update = 4 + + if ski_position in [1, 14]: + standstillcounter += 1 + return y_update + +def update_ski_position(ski_position, action): + if action == 0: + return ski_position + elif action == 1: + return min(ski_position+1, 14) + elif action == 2: + return max(ski_position-1, 1) + +approx_x_coordinate = 80 +ski_position = 8 +for _ in range(1000000): + action = env.action_space.sample() # agent policy that uses the observation and info + action = int(repr(readchar.readchar())[1]) + ski_position = update_ski_position(ski_position, action) + y_update = update_y(y, ski_position) + y += y_update if y_update else 0 + + old_x = deepcopy(approx_x_coordinate) + approx_x_coordinate = int(np.mean(np.where(observation[:,:,1] == 92)[1])) + print(f"Action: {action},\tski position: {ski_position},\ty_update: {y_update},\ty: {y},\tx: {approx_x_coordinate},\tx_update:{approx_x_coordinate - old_x}") + observation, reward, terminated, truncated, info = env.step(action) + if terminated or truncated: + observation, info = env.reset() + + + observation, reward, terminated, truncated, info = env.step(0) + observation, reward, terminated, truncated, info = env.step(0) + observation, reward, terminated, truncated, info = env.step(0) + observation, reward, terminated, truncated, info = env.step(0) + + #plt.imshow(observation) + #plt.show() + #im = Image.fromarray(observation) + #im.save("init.png") + +env.close() diff --git a/test_model.py b/test_model.py new file mode 100644 index 0000000..36d1135 --- /dev/null +++ b/test_model.py @@ -0,0 +1,78 @@ +import time, re, sys, csv, os + +from subprocess import call +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"} + +def convert(tuples): + return dict(tuples) +@dataclass(frozen=True) +class State: + x: int + y: int + ski_position: int + +def default_value(): + return {'action' : None, 'choiceValue' : None} + +@dataclass(frozen=True) +class StateValue: + ranking: float + choices: dict = field(default_factory=default_value) +def exec(command): + print(f"Executing {command}") + system(f"echo {command} >> list_of_exec") + return system(command) + +def fillStateRanking(file_name, match=""): + state_ranking = dict() + try: + with open(file_name, "r") as f: + file_content = f.readlines() + for line in file_content: + if match and skip_line.match(line): continue + stateMapping = convert(re.findall(r"([a-zA-Z_]*[a-zA-Z])=(\d+)?", line)) + #print("stateMapping", stateMapping) + choices = convert(re.findall(r"[a-zA-Z_]*(left|right|noop)[a-zA-Z_]*:(-?\d+\.?\d*)", line)) + #print("choices", choices) + ranking_value = float(re.search(r"Value:([+-]?(\d*\.\d+)|\d+)", line)[0].replace("Value:","")) + #print("ranking_value", ranking_value) + state = State(int(stateMapping["x"]), int(stateMapping["y"]), int(stateMapping["ski_position"])) + value = StateValue(ranking_value, choices) + state_ranking[state] = value + return state_ranking + + except EnvironmentError: + print("TODO file not available. Exiting.") + sys.exit(1) + +ranking = fillStateRanking("action_ranking") +sorted_ranking = sorted(ranking.items(), key=lambda x: x[1].ranking) + +draw_commands = list() + +for state in sorted_ranking[-20:-1]: + print(state) + 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)