diff --git a/rom_evaluate.py b/rom_evaluate.py index 3d71a3a..b719fdc 100644 --- a/rom_evaluate.py +++ b/rom_evaluate.py @@ -69,6 +69,26 @@ 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 + 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} +""" + def csv(self, ws=" "): + return 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}{self.init_check_opt_min:0.04f}{ws}{self.init_check_opt_max:0.04f}{ws}{self.init_check_opt_avg:0.04f}" + def exec(command,verbose=True): if verbose: print(f"Executing {command}") system(f"echo {command} >> list_of_exec") @@ -77,7 +97,7 @@ def exec(command,verbose=True): num_tests_per_cluster = 50 factor_tests_per_cluster = 0.2 num_ski_positions = 8 -num_velocities = 8 +num_velocities = 5 def input_to_action(char): if char == "0": @@ -137,23 +157,41 @@ def run_single_test(ale, nn_wrapper, x,y,ski_position, velocity, duration=50): 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) + #saveObservations(all_obs, Verdict.BAD, testDir) return Verdict.BAD - saveObservations(all_obs, Verdict.GOOD, testDir) + #saveObservations(all_obs, Verdict.GOOD, testDir) return Verdict.GOOD def computeStateRanking(mdp_file, iteration): logger.info("Computing state ranking") tic() + prop = f"filter(min, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += f"filter(max, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += f"filter(avg, Pmin=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += f"filter(min, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += f"filter(max, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += f"filter(avg, Pmax=? [ G !(\"Hit_Tree\" | \"Hit_Gate\" | \"Unsafe\") ], !\"Hit_Tree\" & !\"Hit_Gate\" & !\"Unsafe\" );" + prop += 'Rmax=? [C <= 200]' + results = list() try: - command = f"{tempest_binary} --prism {mdp_file} --buildchoicelab --buildstateval --build-all-labels --prop 'Rmax=? [C <= 1000]'" - result = subprocess.run(command, shell=True, check=True) - print(result) - except Exception as e: - print(e) - sys.exit(-1) - exec(f"mv action_ranking action_ranking_{iteration:03}") + 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') + for line in output: + print(line) + 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)) def fillStateRanking(file_name, match=""): logger.info(f"Parsing state ranking, {file_name}") @@ -189,46 +227,17 @@ def fillStateRanking(file_name, match=""): def createDisjunction(formulas): return " | ".join(formulas) -def clusterFormula(cluster): - if len(cluster) == 0: return - formulas = list() - for state in cluster: - formulas.append(f"(x={state[0].x} & y={state[0].y} & velocity={state[0].velocity} & ski_position={state[0].ski_position})") - - while len(formulas) > 1: - formulas_tmp = [f"({formulas[i]} | {formulas[i+1]})" for i in range(0,len(formulas)//2)] - if len(formulas) % 2 == 1: - formulas_tmp.append(formulas[-1]) - formulas = formulas_tmp - - return "(" + formulas[0] + ")" - -def clusterFormulaXY(cluster): - if len(cluster) == 0: return - formulas = set() - for state in cluster: - formulas.add(f"(x={state[0].x} & y={state[0].y})") - formulas = list(formulas) - while len(formulas) > 1: - formulas_tmp = [f"({formulas[i]} | {formulas[i+1]})" for i in range(0,len(formulas)//2)] - if len(formulas) % 2 == 1: - formulas_tmp.append(formulas[-1]) - formulas = formulas_tmp - - return "(" + formulas[0] + ")" - -def clusterFormulaTrimmed(cluster): - formula = "" - states = [(s[0].x,s[0].y, s[0].ski_position, s[0].velocity) for s in cluster] +def statesFormulaTrimmed(states): + if len(states) == 0: return "false" #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) - #todo add velocity here - firstVelocity = True + formulas = list() for skiPosition, skiPos_group in skiPositionGroup.items(): - formula += f"ski_position={skiPosition} & " + formula = f"( ski_position={skiPosition} & " + firstVelocity = True velocityGroup = defaultdict(list) for item in skiPos_group: velocityGroup[item[3]].append(item) @@ -263,41 +272,25 @@ def clusterFormulaTrimmed(cluster): formula += " | ".join(x_ranges) formula += ") )" formula += ")" - return formula - - - -def createBalancedDisjunction(indices, name): - #logger.info(f"Creating balanced disjunction for {len(indices)} ({indices}) formulas") - if len(indices) == 0: - return f"formula {name} = false;\n" - else: - while len(indices) > 1: - indices_tmp = [f"({indices[i]} | {indices[i+1]})" for i in range(0,len(indices)//2)] - if len(indices) % 2 == 1: - indices_tmp.append(indices[-1]) - indices = indices_tmp - disjunction = f"formula {name} = " + " ".join(indices) + ";\n" - return disjunction - -def createUnsafeFormula(clusters): - label = "label \"Unsafe\" = Unsafe;\n" - formulas = "" - indices = list() - for i, cluster in enumerate(clusters): - formulas += f"formula Unsafe_{i} = {clusterFormulaXY(cluster)};\n" - indices.append(f"Unsafe_{i}") - return formulas + "\n" + createBalancedDisjunction(indices, "Unsafe") + label - -def createSafeFormula(clusters): - label = "label \"Safe\" = Safe;\n" - formulas = "" - indices = list() - for i, cluster in enumerate(clusters): - formulas += f"formula Safe_{i} = {clusterFormulaXY(cluster)};\n" - indices.append(f"Safe_{i}") - - return formulas + "\n" + createBalancedDisjunction(indices, "Safe") + label + formula += ")" + formulas.append(formula) + return createBalancedDisjunction(formulas) + +# 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") @@ -306,8 +299,10 @@ def updatePrismFile(newFile, iteration, safeStates, unsafeStates): newFile = f"{newFile}_{iteration:03}.prism" exec(f"cp {initFile} {newFile}", verbose=False) with open(newFile, "a") as prism: - prism.write(createSafeFormula(safeStates)) - prism.write(createUnsafeFormula(unsafeStates)) + prism.write(f"formula Safe = {statesFormulaTrimmed(safeStates)};\n") + prism.write(f"formula Unsafe = {statesFormulaTrimmed(unsafeStates)};\n") + prism.write(f"label \"Safe\" = Safe;\n") + prism.write(f"label \"Unsafe\" = Unsafe;\n") logger.info(f"Creating next prism file - DONE: took {toc()} seconds") @@ -331,7 +326,7 @@ x = 70 nn_wrapper = SampleFactoryNNQueryWrapper() experiment_id = int(time.time()) -init_mdp = "safety" +init_mdp = "velocity_safety" exec(f"mkdir -p images/testing_{experiment_id}", verbose=False) markerSize = 1 @@ -340,27 +335,46 @@ imagesDir = f"images/testing_{experiment_id}" def drawOntoSkiPosImage(states, color, target_prefix="cluster_", alpha_factor=1.0): #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 + 1) 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 = f"-fill 'rgba({color}, {alpha_factor * state[1].ranking})' -draw 'rectangle {s.x-markerSize},{s.y-markerSize} {s.x+markerSize},{s.y+markerSize} '" - marker = f"-fill 'rgba({color}, {alpha_factor * state[1].ranking})' -draw 'point {s.x},{s.y} '" + #marker = f"-fill 'rgba({color}, {alpha_factor * state[1].ranking})' -draw 'point {s.x},{s.y} '" + 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(): - command = f"convert {imagesDir}/{target_prefix}_{pos:02}_{vel:02}_individual.png {' '.join(marker)} {imagesDir}/{target_prefix}_{pos:02}_{vel:02}_individual.png" - exec(command, verbose=False) + #command = f"convert {imagesDir}/{target_prefix}_{pos:02}_{vel:02}_individual.png {' '.join(marker)} {imagesDir}/{target_prefix}_{pos:02}_{vel:02}_individual.png" + #exec(command, verbose=False) + if len(marker) == 0: continue + 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): - images = [f"{imagesDir}/{prefix}_{pos:02}_{vel:02}_individual.png" for vel in range(0,num_velocities+1) for pos in range(1,num_ski_positions+1) ] - for vel in range(0, num_velocities + 1): + 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}.png", verbose=False) + exec(f"montage {' '.join(mergedImages)} -geometry +0+0 -tile 8x9 {imagesDir}/{prefix}_{iteration}_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): """ @@ -380,33 +394,35 @@ def drawStatesOntoTiledImage(states, color, target, source="images/1_full_scaled """ def drawClusters(clusterDict, target, iteration, alpha_factor=1.0): - logger.info(f"Drawing clusters") + logger.info(f"Drawing {len(clusterDict)} clusters") tic() - for velocity in range(0, num_velocities + 1): - for ski_position in range(1, num_ski_positions + 1): - source = "images/1_full_scaled_down.png" - exec(f"cp {source} {imagesDir}/{target}_{ski_position:02}_{velocity:02}_individual.png", verbose=False) + #for velocity in range(0, num_velocities): + # for ski_position in range(1, num_ski_positions + 1): + # source = "images/1_full_scaled_down.png" + # exec(f"cp {source} {imagesDir}/{target}_{ski_position:02}_{velocity:02}_individual.png", verbose=False) for _, clusterStates in clusterDict.items(): - color = f"{np.random.choice(range(256))}, {np.random.choice(range(256))}, {np.random.choice(range(256))}" + 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 clusters - DONE: took {toc()} seconds") + logger.info(f"Drawing {len(clusterDict)} clusters - DONE: took {toc()} seconds") def drawResult(clusterDict, target, iteration): - logger.info(f"Drawing clusters") - for velocity in range(0,num_velocities+1): - for ski_position in range(1, num_ski_positions + 1): - source = "images/1_full_scaled_down.png" - exec(f"cp {source} {imagesDir}/{target}_{ski_position:02}_{velocity:02}_individual.png", verbose=False) + logger.info(f"Drawing {len(clusterDict)} results") + #for velocity in range(0,num_velocities): + # for ski_position in range(1, num_ski_positions + 1): + # source = "images/1_full_scaled_down.png" + # exec(f"cp {source} {imagesDir}/{target}_{ski_position:02}_{velocity:02}_individual.png", verbose=False) for _, (clusterStates, result) in clusterDict.items(): - color = "100,100,100" + # opencv wants BGR + color = (100,100,100) if result == Verdict.GOOD: - color = "0,200,0" + color = (0,200,0) elif result == Verdict.BAD: - color = "200,0,0" + color = (0,0,200) drawOntoSkiPosImage(clusterStates, color, target, alpha_factor=0.7) concatImages(target, iteration) - logger.info(f"Drawing clusters - DONE: took {toc()} seconds") + logger.info(f"Drawing {len(clusterDict)} results - DONE: took {toc()} seconds") def _init_logger(): logger = logging.getLogger('main') @@ -422,14 +438,20 @@ def clusterImportantStates(ranking, iteration): 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(n_clusters, random_state=0, n_init="auto").fit(states) - dbscan = DBSCAN(eps=15).fit(states) + dbscan = DBSCAN(eps=5).fit(states) labels = dbscan.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: continue + 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 @@ -440,21 +462,42 @@ if __name__ == '__main__': n_clusters = 40 testAll = False - safeStates = list() - unsafeStates = list() + 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) + safeStates = set() + unsafeStates = set() iteration = 0 + results = list() + eps = 0.1 while True: updatePrismFile(init_mdp, iteration, safeStates, unsafeStates) - computeStateRanking(f"{init_mdp}_{iteration:03}.prism", iteration) + modelCheckingResult = computeStateRanking(f"{init_mdp}_{iteration:03}.prism", iteration) + results.append(modelCheckingResult) + logger.info(f"Model Checking Result: {modelCheckingResult}") + if abs(modelCheckingResult.init_check_pes_avg - modelCheckingResult.init_check_opt_avg) < eps: + logger.info(f"Absolute difference between average estimates is below eps = {eps}... finishing!") + break + + ranking = fillStateRanking(f"action_ranking_{iteration:03}") sorted_ranking = sorted( (x for x in ranking.items() if x[1].ranking > 0.1), key=lambda x: x[1].ranking) - clusters = clusterImportantStates(sorted_ranking, iteration) + try: + clusters = clusterImportantStates(sorted_ranking, iteration) + except Exception as e: + print(e) + break if testAll: failingPerCluster = {i: list() for i in range(0, n_clusters)} clusterResult = dict() + logger.info(f"Running tests") + tic() for id, cluster in clusters.items(): num_tests = int(factor_tests_per_cluster * len(cluster)) - 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] @@ -467,22 +510,22 @@ if __name__ == '__main__': velocity = state[0].velocity #result = run_single_test(ale,nn_wrapper,x,y,ski_pos, duration=50) result = run_single_test(ale,nn_wrapper,x,y,ski_pos, velocity, duration=50) - result = Verdict.BAD # TODO REMOVE ME!!!!!!!!!!!!!! if result == Verdict.BAD: if testAll: failingPerCluster[id].append(state) else: clusterResult[id] = (cluster, Verdict.BAD) verdictGood = False - unsafeStates.append(cluster) + unsafeStates.update([(s[0].x,s[0].y, s[0].ski_position, s[0].velocity) for s in cluster]) break if verdictGood: clusterResult[id] = (cluster, Verdict.GOOD) - safeStates.append(cluster) - logger.info(f"Iteration: {iteration:03} -\tSafe Results : {sum([len(c) for c in safeStates])} -\tUnsafe Results:{sum([len(c) for c in unsafeStates])}") + safeStates.update([(s[0].x,s[0].y, s[0].ski_position, s[0].velocity) for s in cluster]) + logger.info(f"Iteration: {iteration:03}\t-\tSafe Results : {len(safeStates)}\t-\tUnsafe Results:{len(unsafeStates)}") if testAll: drawClusters(failingPerCluster, f"failing", iteration) - #drawResult(clusterResult, "result", iteration) + drawResult(clusterResult, "result", iteration) iteration += 1 - + for result in results: + print(result.csv()) diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism index 73c0abb..01d40c5 100644 --- a/velocity_safety_no_formulas.prism +++ b/velocity_safety_no_formulas.prism @@ -4,9 +4,10 @@ const int initY = 40; const int initX = 80; //const int maxY = 580; -const int maxY = 220; +const int maxY = 300; const int minX = 10; -const int maxX = 144; +const int maxX = 152; +const int maxVel = 8; formula Gate_1 = (((42=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; +label "Hit_Tree" = Hit_Tree; +label "Hit_Gate" = Hit_Gate; + global move : [0..3]; @@ -34,9 +38,9 @@ module skier done : bool init false; - [left] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); - [right] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1); - [noop] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); + [left] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); + [right] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1); + [noop] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); [done] move=0 & (Safe | Unsafe | Hit_Tree | Hit_Gate) -> (done'=true); @@ -53,8 +57,8 @@ module updateY [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); + [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 @@ -66,16 +70,16 @@ module updateX [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-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=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-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); + [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 - !done & Hit_Tree : -100; - !done & Hit_Gate : -100; - !done & Unsafe : -100; + [done] !done & Hit_Tree : -100; + [done] !done & Hit_Gate : -100; + [done] !done & Unsafe : -100; endrewards