You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
113 lines
5.4 KiB
113 lines
5.4 KiB
mdp
|
|
|
|
const int initY = 40;
|
|
const int initX = 80;
|
|
|
|
const int maxY = 580;
|
|
const int minX = 10;
|
|
const int maxX = 144;
|
|
|
|
|
|
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>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;
|
|
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<=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;
|
|
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;
|
|
|
|
|
|
|
|
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..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<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<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));
|
|
[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] ;
|
|
|
|
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(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=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-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.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] !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
|