mdp const int initY = 40; const int initX = 80; const int maxY = 210; const int minX = 4; const int maxX = 144; formula Gate_1 = ((4241 & 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 Left_Gate_1 = y>176; formula Left_Gate_2 = y>269; formula Left_Gate_3 = y>361; 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 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 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]; 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] ; 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)); [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)); [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)); [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)); [done] done -> true; endmodule module updateY 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); [update_y] move=1 & (ski_position=4 | ski_position = 5 | ski_position = 10 | ski_position = 11) -> (y'=min(maxY,y+12)) & (standstill'=0) & (move'=2); [update_y] move=1 & (ski_position=6 | ski_position = 7 | ski_position = 8 | ski_position = 9) -> (y'=min(maxY,y+16)) & (standstill'=0) & (move'=2); endmodule module updateX x : [minX..maxX] ; [update_x] move=2 & standstill>=8 -> (move'=0); [update_x] move=2 & standstill<8 & (ski_position=7 | ski_position=8) -> (move'=0); [update_x] move=2 & standstill<8 & ski_position=6 -> 0.1: (x'=max(minX,x-2)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-6)) & (move'=0); [update_x] move=2 & 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=2 & 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=2 & 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=2 & 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=2 & 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=2 & standstill<8 & (ski_position=1) -> 0.1: (x'=max(minX,x-0)) + 0.7: (x'=max(minX,x-2)) + 0.2: (x'=max(minX,x-4)) & (move'=0); [update_x] move=2 & standstill<8 & (ski_position=14) -> 0.1: (x'=min(maxX,x+0)) + 0.7: (x'=min(maxX,x+2)) + 0.2: (x'=min(maxX,x+4)) & (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] !done & (Hit_Tree) : -100; [right] !done & (Hit_Tree) : -100; [noop] !done & (Hit_Tree) : -100; [left] !done & (Hit_Gate) : -100; [right] !done & (Hit_Gate) : -100; [noop] !done & (Hit_Gate) : -100; endrewards