more work on testing framework

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())

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<x & x<50) | (74<x  & x<82))   & 164<y & y<172);
@@ -26,6 +27,9 @@ 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;
 
+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