Compare commits
merge into: sp:main
sp:add_velocity_into_framework
sp:main
pull from: sp:add_velocity_into_framework
sp:add_velocity_into_framework
sp:main
19 Commits
main
...
add_veloci
3 changed files with 1191 additions and 128 deletions
@ -0,0 +1,605 @@ |
|||
import sys |
|||
import operator |
|||
from copy import deepcopy |
|||
from os import listdir, system |
|||
import subprocess |
|||
import re |
|||
from collections import defaultdict |
|||
|
|||
from random import randrange |
|||
from ale_py import ALEInterface, SDL_SUPPORT, Action |
|||
from PIL import Image |
|||
from matplotlib import pyplot as plt |
|||
import cv2 |
|||
import pickle |
|||
import queue |
|||
from dataclasses import dataclass, field |
|||
|
|||
from sklearn.cluster import KMeans, DBSCAN |
|||
|
|||
from enum import Enum |
|||
|
|||
from copy import deepcopy |
|||
|
|||
import numpy as np |
|||
|
|||
import logging |
|||
logger = logging.getLogger(__name__) |
|||
|
|||
#import readchar |
|||
|
|||
from sample_factory.algo.utils.tensor_dict import TensorDict |
|||
from query_sample_factory_checkpoint import SampleFactoryNNQueryWrapper |
|||
|
|||
import time |
|||
|
|||
tempest_binary = "/home/spranger/projects/tempest-devel/ranking_release/bin/storm" |
|||
rom_file = "/home/spranger/research/Skiing/env/lib/python3.10/site-packages/AutoROM/roms/skiing.bin" |
|||
|
|||
def tic(): |
|||
import time |
|||
global startTime_for_tictoc |
|||
startTime_for_tictoc = time.time() |
|||
|
|||
def toc(): |
|||
import time |
|||
if 'startTime_for_tictoc' in globals(): |
|||
return time.time() - startTime_for_tictoc |
|||
|
|||
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) |
|||
|
|||
@dataclass(frozen=True) |
|||
class State: |
|||
x: int |
|||
y: int |
|||
ski_position: int |
|||
velocity: int |
|||
def default_value(): |
|||
return {'action' : None, 'choiceValue' : None} |
|||
|
|||
@dataclass(frozen=True) |
|||
class StateValue: |
|||
ranking: float |
|||
choices: dict = field(default_factory=default_value) |
|||
|
|||
@dataclass(frozen=False) |
|||
class TestResult: |
|||
init_check_pes_min: float |
|||
init_check_pes_max: float |
|||
init_check_pes_avg: float |
|||
init_check_opt_min: float |
|||
init_check_opt_max: float |
|||
init_check_opt_avg: float |
|||
safe_states: int |
|||
unsafe_states: int |
|||
safe_cluster: int |
|||
unsafe_cluster: int |
|||
good_verdicts: int |
|||
bad_verdicts: int |
|||
policy_queries: int |
|||
def __str__(self): |
|||
return f"""Test Result: |
|||
init_check_pes_min: {self.init_check_pes_min} |
|||
init_check_pes_max: {self.init_check_pes_max} |
|||
init_check_pes_avg: {self.init_check_pes_avg} |
|||
init_check_opt_min: {self.init_check_opt_min} |
|||
init_check_opt_max: {self.init_check_opt_max} |
|||
init_check_opt_avg: {self.init_check_opt_avg} |
|||
""" |
|||
@staticmethod |
|||
def csv_header(ws=" "): |
|||
string = f"pesmin{ws}pesmax{ws}pesavg{ws}" |
|||
string += f"optmin{ws}optmax{ws}optavg{ws}" |
|||
string += f"sState{ws}uState{ws}" |
|||
string += f"sClust{ws}uClust{ws}" |
|||
string += f"gVerd{ws}bVerd{ws}queries" |
|||
return string |
|||
|
|||
def csv(self): |
|||
ws = " " |
|||
string = f"{self.init_check_pes_min:0.04f}{ws}{self.init_check_pes_max:0.04f}{ws}{self.init_check_pes_avg:0.04f}{ws}" |
|||
string += f"{self.init_check_opt_min:0.04f}{ws}{self.init_check_opt_max:0.04f}{ws}{self.init_check_opt_avg:0.04f}{ws}" |
|||
ws = "\t" |
|||
string += f"{self.safe_states}{ws}{self.unsafe_states}{ws}" |
|||
string += f"{self.safe_cluster}{ws}{self.unsafe_cluster}{ws}" |
|||
string += f"{self.good_verdicts}{ws}{self.bad_verdicts}{ws}{self.policy_queries}" |
|||
return string |
|||
|
|||
|
|||
def exec(command,verbose=True): |
|||
if verbose: print(f"Executing {command}") |
|||
system(f"echo {command} >> list_of_exec") |
|||
return system(command) |
|||
|
|||
num_tests_per_cluster = 50 |
|||
#factor_tests_per_cluster = 0.2 |
|||
num_ski_positions = 8 |
|||
num_velocities = 5 |
|||
|
|||
def input_to_action(char): |
|||
if char == "0": |
|||
return Action.NOOP |
|||
if char == "1": |
|||
return Action.RIGHT |
|||
if char == "2": |
|||
return Action.LEFT |
|||
if char == "3": |
|||
return "reset" |
|||
if char == "4": |
|||
return "set_x" |
|||
if char == "5": |
|||
return "set_vel" |
|||
if char in ["w", "a", "s", "d"]: |
|||
return char |
|||
|
|||
def saveObservations(observations, verdict, testDir): |
|||
testDir = f"images/testing_{experiment_id}/{verdict.name}_{testDir}_{len(observations)}" |
|||
if len(observations) < 20: |
|||
logger.warn(f"Potentially spurious test case for {testDir}") |
|||
testDir = f"{testDir}_pot_spurious" |
|||
exec(f"mkdir {testDir}", verbose=False) |
|||
for i, obs in enumerate(observations): |
|||
img = Image.fromarray(obs) |
|||
img.save(f"{testDir}/{i:003}.png") |
|||
|
|||
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, velocity, duration=50): |
|||
#print(f"Running Test from x: {x:04}, y: {y:04}, ski_position: {ski_position}", end="") |
|||
testDir = f"{x}_{y}_{ski_position}_{velocity}" |
|||
try: |
|||
for i, r in enumerate(ramDICT[y]): |
|||
ale.setRAM(i,r) |
|||
ski_position_setting = ski_position_counter[ski_position] |
|||
for i in range(0,ski_position_setting[1]): |
|||
ale.act(ski_position_setting[0]) |
|||
ale.setRAM(14,0) |
|||
ale.setRAM(25,x) |
|||
ale.setRAM(14,180) # TODO |
|||
except Exception as e: |
|||
print(e) |
|||
logger.warn(f"Could not run test for x: {x}, y: {y}, ski_position: {ski_position}, velocity: {velocity}") |
|||
return (Verdict.INCONCLUSIVE, 0) |
|||
|
|||
num_queries = 0 |
|||
all_obs = list() |
|||
speed_list = list() |
|||
resized_obs = cv2.resize(ale.getScreenGrayscale(), (84,84), interpolation=cv2.INTER_AREA) |
|||
for i in range(0,4): |
|||
all_obs.append(resized_obs) |
|||
for i in range(0,duration-4): |
|||
resized_obs = cv2.resize(ale.getScreenGrayscale(), (84,84), interpolation=cv2.INTER_AREA) |
|||
all_obs.append(resized_obs) |
|||
if i % 4 == 0: |
|||
stack_tensor = TensorDict({"obs": np.array(all_obs[-4:])}) |
|||
action = nn_wrapper.query(stack_tensor) |
|||
num_queries += 1 |
|||
ale.act(input_to_action(str(action))) |
|||
else: |
|||
ale.act(input_to_action(str(action))) |
|||
speed_list.append(ale.getRAM()[14]) |
|||
if len(speed_list) > 15 and sum(speed_list[-6:-1]) == 0: |
|||
#saveObservations(all_obs, Verdict.BAD, testDir) |
|||
return (Verdict.BAD, num_queries) |
|||
#saveObservations(all_obs, Verdict.GOOD, testDir) |
|||
return (Verdict.GOOD, num_queries) |
|||
|
|||
def skiPositionFormulaList(name): |
|||
formulas = list() |
|||
for i in range(1, num_ski_positions+1): |
|||
formulas.append(f"\"{name}_{i}\"") |
|||
return createBalancedDisjunction(formulas) |
|||
|
|||
|
|||
def computeStateRanking(mdp_file, iteration): |
|||
logger.info("Computing state ranking") |
|||
tic() |
|||
prop = f"filter(min, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += f"filter(max, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += f"filter(avg, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += f"filter(min, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += f"filter(max, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += f"filter(avg, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | {skiPositionFormulaList('Unsafe')}) ], (!\"S_Hit_Tree\" & !\"S_Hit_Gate\") | ({skiPositionFormulaList('Safe')} | {skiPositionFormulaList('Unsafe')}) );" |
|||
prop += 'Rmax=? [C <= 200]' |
|||
results = list() |
|||
try: |
|||
command = f"{tempest_binary} --prism {mdp_file} --buildchoicelab --buildstateval --build-all-labels --prop '{prop}'" |
|||
output = subprocess.check_output(command, shell=True).decode("utf-8").split('\n') |
|||
num_states = 0 |
|||
for line in output: |
|||
#print(line) |
|||
if "States:" in line: |
|||
num_states = int(line.split(" ")[-1]) |
|||
if "Result" in line and not len(results) >= 6: |
|||
range_value = re.search(r"(.*:).*\[(-?\d+\.?\d*), (-?\d+\.?\d*)\].*", line) |
|||
if range_value: |
|||
results.append(float(range_value.group(2))) |
|||
results.append(float(range_value.group(3))) |
|||
else: |
|||
value = re.search(r"(.*:)(.*)", line) |
|||
results.append(float(value.group(2))) |
|||
exec(f"mv action_ranking action_ranking_{iteration:03}") |
|||
except subprocess.CalledProcessError as e: |
|||
# todo die gracefully if ranking is uniform |
|||
print(e.output) |
|||
logger.info(f"Computing state ranking - DONE: took {toc()} seconds") |
|||
return TestResult(*tuple(results),0,0,0,0,0,0,0), num_states |
|||
|
|||
def fillStateRanking(file_name, match=""): |
|||
logger.info(f"Parsing state ranking, {file_name}") |
|||
tic() |
|||
state_ranking = dict() |
|||
try: |
|||
with open(file_name, "r") as f: |
|||
file_content = f.readlines() |
|||
for line in file_content: |
|||
if not "move=0" in line: continue |
|||
ranking_value = float(re.search(r"Value:([+-]?(\d*\.\d+)|\d+)", line)[0].replace("Value:","")) |
|||
if ranking_value <= 0.1: |
|||
continue |
|||
stateMapping = convert(re.findall(r"([a-zA-Z_]*[a-zA-Z])=(\d+)?", line)) |
|||
choices = convert(re.findall(r"[a-zA-Z_]*(left|right|noop)[a-zA-Z_]*:(-?\d+\.?\d*)", line)) |
|||
choices = {key:float(value) for (key,value) in choices.items()} |
|||
state = State(int(stateMapping["x"]), int(stateMapping["y"]), int(stateMapping["ski_position"]), int(stateMapping["velocity"])//2) |
|||
value = StateValue(ranking_value, choices) |
|||
state_ranking[state] = value |
|||
logger.info(f"Parsing state ranking - DONE: took {toc()} seconds") |
|||
return state_ranking |
|||
except EnvironmentError: |
|||
print("Ranking file not available. Exiting.") |
|||
toc() |
|||
sys.exit(-1) |
|||
except: |
|||
toc() |
|||
|
|||
def createDisjunction(formulas): |
|||
return " | ".join(formulas) |
|||
|
|||
def statesFormulaTrimmed(states, name): |
|||
#states = [(s[0].x,s[0].y, s[0].ski_position) for s in cluster] |
|||
skiPositionGroup = defaultdict(list) |
|||
for item in states: |
|||
skiPositionGroup[item[2]].append(item) |
|||
|
|||
formulas = list() |
|||
for skiPosition, skiPos_group in skiPositionGroup.items(): |
|||
formula = f"formula {name}_{skiPosition} = ( ski_position={skiPosition} & " |
|||
#print(f"{name} ski_pos:{skiPosition}") |
|||
velocityGroup = defaultdict(list) |
|||
velocityFormulas = list() |
|||
for item in skiPos_group: |
|||
velocityGroup[item[3]].append(item) |
|||
for velocity, velocity_group in velocityGroup.items(): |
|||
#print(f"\tvel:{velocity}") |
|||
formulasPerSkiPosition = list() |
|||
yPosGroup = defaultdict(list) |
|||
yFormulas = list() |
|||
for item in velocity_group: |
|||
yPosGroup[item[1]].append(item) |
|||
for y, y_group in yPosGroup.items(): |
|||
#print(f"\t\ty:{y}") |
|||
sorted_y_group = sorted(y_group, key=lambda s: s[0]) |
|||
current_x_min = sorted_y_group[0][0] |
|||
current_x = sorted_y_group[0][0] |
|||
x_ranges = list() |
|||
for state in sorted_y_group[1:-1]: |
|||
if state[0] - current_x == 1: |
|||
current_x = state[0] |
|||
else: |
|||
x_ranges.append(f" ({current_x_min}<=x&x<={current_x})") |
|||
current_x_min = state[0] |
|||
current_x = state[0] |
|||
x_ranges.append(f" {current_x_min}<=x&x<={sorted_y_group[-1][0]}") |
|||
yFormulas.append(f" (y={y} & {createBalancedDisjunction(x_ranges)})") |
|||
#x_ranges.clear() |
|||
|
|||
#velocityFormulas.append(f"(velocity={velocity} & {createBalancedDisjunction(yFormulas)})") |
|||
velocityFormulas.append(f"({createBalancedDisjunction(yFormulas)})") |
|||
#yFormulas.clear() |
|||
formula += createBalancedDisjunction(velocityFormulas) + ");" |
|||
#velocityFormulas.clear() |
|||
formulas.append(formula) |
|||
for i in range(1, num_ski_positions+1): |
|||
if i in skiPositionGroup: |
|||
continue |
|||
formulas.append(f"formula {name}_{i} = false;") |
|||
return "\n".join(formulas) + "\n" |
|||
|
|||
# https://stackoverflow.com/questions/5389507/iterating-over-every-two-elements-in-a-list |
|||
def pairwise(iterable): |
|||
"s -> (s0, s1), (s2, s3), (s4, s5), ..." |
|||
a = iter(iterable) |
|||
return zip(a, a) |
|||
|
|||
def createBalancedDisjunction(formulas): |
|||
if len(formulas) == 0: |
|||
return "false" |
|||
while len(formulas) > 1: |
|||
formulas_tmp = [f"({f} | {g})" for f,g in pairwise(formulas)] |
|||
if len(formulas) % 2 == 1: |
|||
formulas_tmp.append(formulas[-1]) |
|||
formulas = formulas_tmp |
|||
return " ".join(formulas) |
|||
|
|||
def updatePrismFile(newFile, iteration, safeStates, unsafeStates): |
|||
logger.info("Creating next prism file") |
|||
tic() |
|||
initFile = f"{newFile}_no_formulas.prism" |
|||
newFile = f"{newFile}_{iteration:03}.prism" |
|||
exec(f"cp {initFile} {newFile}", verbose=False) |
|||
with open(newFile, "a") as prism: |
|||
prism.write(statesFormulaTrimmed(safeStates, "Safe")) |
|||
prism.write(statesFormulaTrimmed(unsafeStates, "Unsafe")) |
|||
for i in range(1,num_ski_positions+1): |
|||
prism.write(f"label \"Safe_{i}\" = Safe_{i};\n") |
|||
prism.write(f"label \"Unsafe_{i}\" = Unsafe_{i};\n") |
|||
|
|||
logger.info(f"Creating next prism file - DONE: took {toc()} seconds") |
|||
|
|||
|
|||
ale = ALEInterface() |
|||
|
|||
|
|||
#if SDL_SUPPORT: |
|||
# ale.setBool("sound", True) |
|||
# ale.setBool("display_screen", True) |
|||
|
|||
# Load the ROM file |
|||
ale.loadROM(rom_file) |
|||
|
|||
with open('all_positions_v2.pickle', 'rb') as handle: |
|||
ramDICT = pickle.load(handle) |
|||
y_ram_setting = 60 |
|||
x = 70 |
|||
|
|||
|
|||
nn_wrapper = SampleFactoryNNQueryWrapper() |
|||
|
|||
experiment_id = int(time.time()) |
|||
init_mdp = "velocity_safety" |
|||
exec(f"mkdir -p images/testing_{experiment_id}", verbose=False) |
|||
|
|||
|
|||
imagesDir = f"images/testing_{experiment_id}" |
|||
|
|||
def drawOntoSkiPosImage(states, color, target_prefix="cluster_", alpha_factor=1.0, markerSize=1, drawCircle=False): |
|||
#markerList = {ski_position:list() for ski_position in range(1,num_ski_positions + 1)} |
|||
markerList = {(ski_position, velocity):list() for velocity in range(0, num_velocities) for ski_position in range(1,num_ski_positions + 1)} |
|||
images = dict() |
|||
mergedImages = dict() |
|||
for ski_position in range(1, num_ski_positions + 1): |
|||
for velocity in range(0,num_velocities): |
|||
images[(ski_position, velocity)] = cv2.imread(f"{imagesDir}/{target_prefix}_{ski_position:02}_{velocity:02}_individual.png") |
|||
mergedImages[ski_position] = cv2.imread(f"{imagesDir}/{target_prefix}_{ski_position:02}_individual.png") |
|||
for state in states: |
|||
s = state[0] |
|||
marker = [color, alpha_factor * state[1].ranking, (s.x-markerSize, s.y-markerSize), (s.x+markerSize, s.y+markerSize)] |
|||
markerList[(s.ski_position, s.velocity)].append(marker) |
|||
for (pos, vel), marker in markerList.items(): |
|||
if len(marker) == 0: continue |
|||
if drawCircle: |
|||
for m in marker: |
|||
images[(pos,vel)] = cv2.circle(images[(pos,vel)], m[2], 1, m[0], thickness=-1) |
|||
mergedImages[pos] = cv2.circle(mergedImages[pos], m[2], 1, m[0], thickness=-1) |
|||
else: |
|||
for m in marker: |
|||
images[(pos,vel)] = cv2.rectangle(images[(pos,vel)], m[2], m[3], m[0], cv2.FILLED) |
|||
mergedImages[pos] = cv2.rectangle(mergedImages[pos], m[2], m[3], m[0], cv2.FILLED) |
|||
for (ski_position, velocity), image in images.items(): |
|||
cv2.imwrite(f"{imagesDir}/{target_prefix}_{ski_position:02}_{velocity:02}_individual.png", image) |
|||
for ski_position, image in mergedImages.items(): |
|||
cv2.imwrite(f"{imagesDir}/{target_prefix}_{ski_position:02}_individual.png", image) |
|||
|
|||
|
|||
def concatImages(prefix, iteration): |
|||
logger.info(f"Concatenating images") |
|||
images = [f"{imagesDir}/{prefix}_{pos:02}_{vel:02}_individual.png" for vel in range(0,num_velocities) for pos in range(1,num_ski_positions+1)] |
|||
mergedImages = [f"{imagesDir}/{prefix}_{pos:02}_individual.png" for pos in range(1,num_ski_positions+1)] |
|||
for vel in range(0, num_velocities): |
|||
for pos in range(1, num_ski_positions + 1): |
|||
command = f"convert {imagesDir}/{prefix}_{pos:02}_{vel:02}_individual.png " |
|||
command += f"-pointsize 10 -gravity NorthEast -annotate +8+0 'p{pos:02}v{vel:02}' " |
|||
command += f"{imagesDir}/{prefix}_{pos:02}_{vel:02}_individual.png" |
|||
exec(command, verbose=False) |
|||
exec(f"montage {' '.join(images)} -geometry +0+0 -tile 8x9 {imagesDir}/{prefix}_{iteration:03}.png", verbose=False) |
|||
exec(f"montage {' '.join(mergedImages)} -geometry +0+0 -tile 8x9 {imagesDir}/{prefix}_{iteration:03}_merged.png", verbose=False) |
|||
#exec(f"sxiv {imagesDir}/{prefix}_{iteration}.png&", verbose=False) |
|||
logger.info(f"Concatenating images - DONE") |
|||
|
|||
def drawStatesOntoTiledImage(states, color, target, source="images/1_full_scaled_down.png", alpha_factor=1.0): |
|||
""" |
|||
Useful to draw a set of states, e.g. a single cluster |
|||
TODO |
|||
markerList = {1: list(), 2:list(), 3:list(), 4:list(), 5:list(), 6:list(), 7:list(), 8:list()} |
|||
logger.info(f"Drawing {len(states)} states onto {target}") |
|||
tic() |
|||
for state in states: |
|||
s = state[0] |
|||
marker = f"-fill 'rgba({color}, {alpha_factor * state[1].ranking})' -draw 'rectangle {s.x-markerSize},{s.y-markerSize} {s.x+markerSize},{s.y+markerSize} '" |
|||
markerList[s.ski_position].append(marker) |
|||
for pos, marker in markerList.items(): |
|||
command = f"convert {source} {' '.join(marker)} {imagesDir}/{target}_{pos:02}_individual.png" |
|||
exec(command, verbose=False) |
|||
exec(f"montage {imagesDir}/{target}_*_individual.png -geometry +0+0 -tile x1 {imagesDir}/{target}.png", verbose=False) |
|||
logger.info(f"Drawing {len(states)} states onto {target} - Done: took {toc()} seconds") |
|||
""" |
|||
|
|||
def drawClusters(clusterDict, target, iteration, alpha_factor=1.0): |
|||
logger.info(f"Drawing {len(clusterDict)} clusters") |
|||
tic() |
|||
for _, clusterStates in clusterDict.items(): |
|||
color = (np.random.choice(range(256)), np.random.choice(range(256)), np.random.choice(range(256))) |
|||
color = (int(color[0]), int(color[1]), int(color[2])) |
|||
drawOntoSkiPosImage(clusterStates, color, target, alpha_factor=alpha_factor) |
|||
concatImages(target, iteration) |
|||
logger.info(f"Drawing {len(clusterDict)} clusters - DONE: took {toc()} seconds") |
|||
|
|||
def drawResult(clusterDict, target, iteration, drawnCluster=set()): |
|||
logger.info(f"Drawing {len(clusterDict)} results") |
|||
tic() |
|||
for id, (clusterStates, result) in clusterDict.items(): |
|||
if id in drawnCluster: continue |
|||
# opencv wants BGR |
|||
color = (100,100,100) |
|||
if result == Verdict.GOOD: |
|||
color = (0,200,0) |
|||
elif result == Verdict.BAD: |
|||
color = (0,0,200) |
|||
drawOntoSkiPosImage(clusterStates, color, target, alpha_factor=0.7) |
|||
logger.info(f"Drawing {len(clusterDict)} results - DONE: took {toc()} seconds") |
|||
|
|||
def _init_logger(): |
|||
logger = logging.getLogger('main') |
|||
logger.setLevel(logging.INFO) |
|||
handler = logging.StreamHandler(sys.stdout) |
|||
formatter = logging.Formatter( '[%(levelname)s] %(module)s - %(message)s') |
|||
handler.setFormatter(formatter) |
|||
logger.addHandler(handler) |
|||
|
|||
def clusterImportantStates(ranking, iteration): |
|||
logger.info(f"Starting to cluster {len(ranking)} states into clusters") |
|||
tic() |
|||
states = [[s[0].x,s[0].y, s[0].ski_position * 20, s[0].velocity * 20, s[1].ranking] for s in ranking] |
|||
#states = [[s[0].x,s[0].y, s[0].ski_position * 30, s[1].ranking] for s in ranking] |
|||
kmeans = KMeans(len(states) // 15, random_state=0, n_init="auto").fit(states) |
|||
#dbscan = DBSCAN(eps=5).fit(states) |
|||
#labels = dbscan.labels_ |
|||
labels = kmeans.labels_ |
|||
n_clusters = len(set(labels)) - (1 if -1 in labels else 0) |
|||
logger.info(f"Starting to cluster {len(ranking)} states into clusters - DONE: took {toc()} seconds with {n_clusters} cluster") |
|||
clusterDict = {i : list() for i in range(0,n_clusters)} |
|||
strayStates = list() |
|||
for i, state in enumerate(ranking): |
|||
if labels[i] == -1: |
|||
clusterDict[n_clusters + len(strayStates) + 1] = list() |
|||
clusterDict[n_clusters + len(strayStates) + 1].append(state) |
|||
strayStates.append(state) |
|||
continue |
|||
clusterDict[labels[i]].append(state) |
|||
if len(strayStates) > 0: logger.warning(f"{len(strayStates)} stray states with label -1") |
|||
#drawClusters(clusterDict, f"clusters", iteration) |
|||
return clusterDict |
|||
|
|||
|
|||
def run_experiment(factor_tests_per_cluster): |
|||
logger.info("Starting") |
|||
num_queries = 0 |
|||
|
|||
source = "images/1_full_scaled_down.png" |
|||
for ski_position in range(1, num_ski_positions + 1): |
|||
for velocity in range(0,num_velocities): |
|||
exec(f"cp {source} {imagesDir}/clusters_{ski_position:02}_{velocity:02}_individual.png", verbose=False) |
|||
exec(f"cp {source} {imagesDir}/result_{ski_position:02}_{velocity:02}_individual.png", verbose=False) |
|||
exec(f"cp {source} {imagesDir}/clusters_{ski_position:02}_individual.png", verbose=False) |
|||
exec(f"cp {source} {imagesDir}/result_{ski_position:02}_individual.png", verbose=False) |
|||
|
|||
goodVerdicts = 0 |
|||
badVerdicts = 0 |
|||
goodVerdictTestCases = list() |
|||
badVerdictTestCases = list() |
|||
safeClusters = 0 |
|||
unsafeClusters = 0 |
|||
safeStates = set() |
|||
unsafeStates = set() |
|||
iteration = 0 |
|||
results = list() |
|||
|
|||
eps = 0.1 |
|||
updatePrismFile(init_mdp, iteration, set(), set()) |
|||
#modelCheckingResult, numStates = TestResult(0,0,0,0,0,0,0,0,0,0,0,0,0), 10 |
|||
modelCheckingResult, numStates = computeStateRanking(f"{init_mdp}_000.prism", iteration) |
|||
results.append(modelCheckingResult) |
|||
ranking = fillStateRanking(f"action_ranking_000") |
|||
|
|||
sorted_ranking = sorted( (x for x in ranking.items() if x[1].ranking > 0.1), key=lambda x: x[1].ranking) |
|||
try: |
|||
clusters = clusterImportantStates(sorted_ranking, iteration) |
|||
except Exception as e: |
|||
print(e) |
|||
sys.exit(-1) |
|||
|
|||
clusterResult = dict() |
|||
logger.info(f"Running tests") |
|||
tic() |
|||
num_cluster_tested = 0 |
|||
iteration = 0 |
|||
drawnCluster = set() |
|||
for id, cluster in clusters.items(): |
|||
num_tests = int(factor_tests_per_cluster * len(cluster)) |
|||
if num_tests == 0: num_tests = 1 |
|||
logger.info(f"Testing {num_tests} states (from {len(cluster)} states) from cluster {id}") |
|||
randomStates = np.random.choice(len(cluster), num_tests, replace=False) |
|||
randomStates = [cluster[i] for i in randomStates] |
|||
|
|||
verdictGood = True |
|||
for state in randomStates: |
|||
x = state[0].x |
|||
y = state[0].y |
|||
ski_pos = state[0].ski_position |
|||
velocity = state[0].velocity |
|||
result, num_queries_this_test_case = run_single_test(ale,nn_wrapper,x,y,ski_pos, velocity, duration=50) |
|||
num_queries += num_queries_this_test_case |
|||
if result == Verdict.BAD: |
|||
clusterResult[id] = (cluster, Verdict.BAD) |
|||
verdictGood = False |
|||
unsafeStates.update([(s[0].x,s[0].y, s[0].ski_position, s[0].velocity) for s in cluster]) |
|||
badVerdicts += 1 |
|||
badVerdictTestCases.append(state) |
|||
|
|||
elif result == Verdict.GOOD: |
|||
goodVerdicts += 1 |
|||
goodVerdictTestCases.append(state) |
|||
if verdictGood: |
|||
clusterResult[id] = (cluster, Verdict.GOOD) |
|||
safeClusters += 1 |
|||
safeStates.update([(s[0].x,s[0].y, s[0].ski_position, s[0].velocity) for s in cluster]) |
|||
else: |
|||
unsafeClusters += 1 |
|||
results[-1].safe_states = len(safeStates) |
|||
results[-1].unsafe_states = len(unsafeStates) |
|||
results[-1].policy_queries = num_queries |
|||
results[-1].safe_cluster = safeClusters |
|||
results[-1].unsafe_cluster = unsafeClusters |
|||
results[-1].good_verdicts = goodVerdicts |
|||
results[-1].bad_verdicts = badVerdicts |
|||
num_cluster_tested += 1 |
|||
if num_cluster_tested % (len(clusters)//20) == 0: |
|||
iteration += 1 |
|||
logger.info(f"Tested Cluster: {num_cluster_tested:03}\tSafe Cluster States : {len(safeStates)}({safeClusters}/{len(clusters)})\tUnsafe Cluster States:{len(unsafeStates)}({unsafeClusters}/{len(clusters)})\tGood Test Cases:{goodVerdicts}\tFailing Test Cases:{badVerdicts}\t{len(safeStates)/len(unsafeStates)} - {goodVerdicts/badVerdicts}") |
|||
drawResult(clusterResult, "result", iteration, drawnCluster) |
|||
drawOntoSkiPosImage(goodVerdictTestCases, (10,255,50), "result", alpha_factor=0.7, markerSize=0, drawCircle=True) |
|||
drawOntoSkiPosImage(badVerdictTestCases, (0,0,0), "result", alpha_factor=0.7, markerSize=0, drawCircle=True) |
|||
concatImages("result", iteration) |
|||
drawnCluster.update(clusterResult.keys()) |
|||
#updatePrismFile(init_mdp, iteration, safeStates, unsafeStates) |
|||
#modelCheckingResult, numStates = computeStateRanking(f"{init_mdp}_{iteration:03}.prism", iteration) |
|||
results.append(deepcopy(modelCheckingResult)) |
|||
logger.info(f"Model Checking Result: {modelCheckingResult}") |
|||
# Account for self-loop states after first iteration |
|||
if iteration > 0: |
|||
results[-1].init_check_pes_avg = 1/(numStates+len(safeStates)+len(unsafeStates)) * (results[-1].init_check_pes_avg*numStates + 1.0*results[-2].unsafe_states + 0.0*results[-2].safe_states) |
|||
results[-1].init_check_opt_avg = 1/(numStates+len(safeStates)+len(unsafeStates)) * (results[-1].init_check_opt_avg*numStates + 0.0*results[-2].unsafe_states + 1.0*results[-2].safe_states) |
|||
print(TestResult.csv_header()) |
|||
for result in results[:-1]: |
|||
print(result.csv()) |
|||
|
|||
|
|||
with open(f"data_new_method_{factor_tests_per_cluster}", "w") as f: |
|||
f.write(TestResult.csv_header() + "\n") |
|||
for result in results[:-1]: |
|||
f.write(result.csv() + "\n") |
|||
|
|||
|
|||
_init_logger() |
|||
logger = logging.getLogger('main') |
|||
if __name__ == '__main__': |
|||
for factor_tests_per_cluster in [0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 1.0]: |
|||
run_experiment(factor_tests_per_cluster) |
|||
@ -0,0 +1,137 @@ |
|||
mdp |
|||
|
|||
const int initY = 40; |
|||
const int initX = 80; |
|||
|
|||
const int maxY = 580; |
|||
//const int maxY = 360; |
|||
//const int maxY = 200; |
|||
const int minX = 10; |
|||
const int maxX = 152; |
|||
const int maxVel = 8; |
|||
|
|||
|
|||
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 S_Gate_1 = (((32<x & x<60) | (64<x & x<92)) & 124<y & y<172); |
|||
formula S_Gate_2 = (((62<x & x<90) | (94<x & x<132)) & 216<y & y<264); |
|||
formula S_Gate_3 = (((70<x & x<98) | (102<x & x<130)) & 309<y & y<357); |
|||
formula S_Gate_4 = (((44<x & x<72) | (78<x & x<106)) & 402<y & y<450); |
|||
formula S_Gate_5 = (((70<x & x<98) | (102<x & x<130)) & 490<y & y<538); |
|||
|
|||
|
|||
formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200)); |
|||
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 S_Tree_1 = ((x>=114 & x<=152) & (y>=150 & y<=200)); |
|||
formula S_Tree_2 = ((x>=22 & x<=59) & (y>=244 & y<=295)); |
|||
formula S_Tree_3 = ((x>=20 & x<=59) & (y>=277 & y<=327)); |
|||
formula S_Tree_4 = ((x>=2 & x<=40) & (y>=368 & y<=418)); |
|||
formula S_Tree_5 = ((x>=119 & x<=156) & (y>=438 & y<=480)); |
|||
formula S_Tree_6 = ((x>=130 & x<=162) & (y>=456 & 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; |
|||
formula S_Hit_Tree = S_Tree_1 | S_Tree_2 | S_Tree_3 | S_Tree_4 | S_Tree_5 | S_Tree_6; |
|||
formula S_Hit_Gate = S_Gate_1 | S_Gate_2 | S_Gate_3 | S_Gate_4 | S_Gate_5; |
|||
|
|||
formula Safe = ( (Safe_1 | Safe_2) | (Safe_3 | Safe_4) ) | ( (Safe_5 | Safe_6) | (Safe_7 | Safe_8) ); |
|||
formula Unsafe = ( (Unsafe_1 | Unsafe_2) | (Unsafe_3 | Unsafe_4) ) | ( (Unsafe_5 | Unsafe_6) | (Unsafe_7 | Unsafe_8) ); |
|||
|
|||
|
|||
label "Hit_Tree" = Hit_Tree; |
|||
label "Hit_Gate" = Hit_Gate; |
|||
label "S_Hit_Tree" = S_Hit_Tree; |
|||
label "S_Hit_Gate" = S_Hit_Gate; |
|||
|
|||
|
|||
global move : [0..3]; |
|||
|
|||
|
|||
|
|||
module skier |
|||
ski_position : [1..8] init 4; |
|||
reward_given: bool init false; |
|||
//done: bool init false; |
|||
|
|||
|
|||
[left] !reward_given & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); |
|||
[right] !reward_given & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1); |
|||
[noop] !reward_given & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); |
|||
|
|||
|
|||
[done] !reward_given & (Hit_Tree | Hit_Gate | Safe | Unsafe) & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_1 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_2 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_3 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_4 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_5 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_6 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_7 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Unsafe_8 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_1 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_2 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_3 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_4 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_5 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_6 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_7 & move=0 -> (reward_given'=true); |
|||
//[done] !reward_given & Safe_8 & move=0 -> (reward_given'=true); |
|||
|
|||
|
|||
endmodule |
|||
|
|||
module updateY |
|||
y : [initY..maxY] ; |
|||
|
|||
velocity: [0..16]; |
|||
standstill : [0..8] ; |
|||
[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 = 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(maxVel,velocity+2)) & (standstill'=0) & (move'=3); |
|||
[update_y] move=2 & (ski_position=4 | ski_position = 5) -> (velocity'=min(maxVel,velocity+4)) & (standstill'=0) & (move'=3); |
|||
endmodule |
|||
|
|||
module updateX |
|||
x : [minX..maxX] init initX; |
|||
|
|||
[update_x] move=3 & standstill>=8 -> (move'=0); |
|||
[update_x] move=3 & standstill<8 & (ski_position=4 | ski_position=5) -> (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) -> 0.3: (x'=max(minX,x-1)) & (move'=0) + 0.7: (x'=max(minX,x-2)) & (move'=0); |
|||
[update_x] move=3 & standstill<8 & (ski_position=7) -> 0.3: (x'=min(maxX,x+1)) & (move'=0) + 0.7: (x'=min(maxX,x+2)) & (move'=0); |
|||
|
|||
[update_x] move=3 & standstill<8 & (ski_position=1) -> 0.2: (x'=max(minX,x-2)) & (move'=0) + 0.8: (x'=max(minX,x-3)) & (move'=0); |
|||
[update_x] move=3 & standstill<8 & (ski_position=8) -> 0.2: (x'=min(maxX,x+2)) & (move'=0) + 0.8: (x'=min(maxX,x+3)) & (move'=0); |
|||
endmodule |
|||
|
|||
//rewards |
|||
// [left] !done & !reward_given & Hit_Tree : -100; |
|||
// [left] !done & !reward_given & Hit_Gate : -100; |
|||
// [left] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100; |
|||
// [right] !done & !reward_given & Hit_Tree : -100; |
|||
// [right] !done & !reward_given & Hit_Gate : -100; |
|||
// [right] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100; |
|||
// [noop] !done & !reward_given & Hit_Tree : -100; |
|||
// [noop] !done & !reward_given & Hit_Gate : -100; |
|||
// [noop] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100; |
|||
//endrewards |
|||
|
|||
rewards |
|||
[done] !reward_given & (Hit_Gate | Hit_Tree | Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100; |
|||
endrewards |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue