Browse Source

updated some old code

This is a summary commit containing changes from some time ago...
main
sp 8 months ago
parent
commit
1b4907e43f
  1. 70
      first_try.prism
  2. 88
      rom_evaluate.py
  3. 48
      simplified.prism
  4. 73
      test_model.py
  5. 74
      velocity.prism

70
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;

88
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]:
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)
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"
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")

48
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 = ((42<x & x<50 | 74<x & x=80) & 184<y & y<172);
formula Gate_2 = ((x=71 | x=104) & y=261);
formula Gate_3 = ((x=81 | x=113) & y=353);
formula Gate_4 = ((x=55 | x=88) & y=446);
@ -25,7 +25,7 @@ formula Left_Gate_3 = y>361;
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);

73
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")

74
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 = ((42<x & x<50 | 74<x & x=80) & 184<y & y<172);
formula Gate_2 = ((x=71 | x=104) & y=261);
formula Gate_3 = ((x=81 | x=113) & y=353);
formula Gate_4 = ((x=55 | x=88) & y=446);
formula Gate_5 = ((x=79 | x=110) & y=538);
formula Gate_1 = (((42<x & x<50) | (74<x & x<82)) & 164<y & y<172);
formula Gate_2 = (((72<x & x<80) | (104<x & x<112)) & 256<y & y<264);
formula Gate_3 = (((80<x & x<88) | (112<x & x<120)) & 349<y & y<357);
formula Gate_4 = (((54<x & x<62) | (88<x & x<96)) & 442<y & y<450);
formula Gate_5 = (((80<x & x<88) | (112<x & x<120)) & 530<y & y<538);
formula Passed_Gate_1 = ((x>41 & 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;

Loading…
Cancel
Save