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.
132 lines
7.4 KiB
132 lines
7.4 KiB
mdp
|
|
|
|
const int initY = 40;
|
|
const int initX = 80;
|
|
|
|
const int maxY = 180;
|
|
const int minX = 4;
|
|
const int maxX = 144;
|
|
|
|
|
|
formula Gate_1 = ((x=41 | x=73) & y=168);
|
|
formula Gate_2 = ((x=71 | x=104) & y=261);
|
|
formula Gate_3 = ((x=81 | x=113) & y=353);
|
|
formula Gate_4 = ((x=55 | x=88) & y=446);
|
|
formula Gate_5 = ((x=79 | x=110) & y=538);
|
|
|
|
formula Passed_Gate_1 = ((x>41 & x<73) & (y>164 & y<170)); //(y=168));
|
|
formula Passed_Gate_2 = ((x>71 & x<104) & (y>257 & y<262)); //(y=261));
|
|
formula Passed_Gate_3 = ((x>81 & x<113) & (y>349 & y<355)); //(y=353));
|
|
formula Passed_Gate_4 = ((x>55 & x<88) & (y>442 & y<448)); //(y=446));
|
|
formula Passed_Gate_5 = ((x>79 & x<110) & (y>534 & y<540)); //(y=538));
|
|
|
|
formula Tree_1 = ((x>=124 & x<=134) & (y>=194 & y<=200));
|
|
formula Tree_2 = ((x>=32 & x<=42) & (y>=291 & y<=297));
|
|
formula Tree_3 = ((x>=28 & x<=38) & (y>=321 & y<=327));
|
|
formula Tree_4 = ((x>=12 & x<=22) & (y>=412 & y<=418));
|
|
formula Tree_5 = ((x>=129 & x<=139) & (y>=472 & y<=480));
|
|
formula Tree_6 = ((x>=140 & x<=144) & (y>=502 & 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;
|
|
|
|
|
|
global move : [0..3] init 0;
|
|
|
|
module skier
|
|
ski_position : [1..14] init 8;
|
|
done : bool init false;
|
|
|
|
passed_gate_1 : bool init false;
|
|
passed_gate_2 : bool init false;
|
|
passed_gate_3 : bool init false;
|
|
passed_gate_4 : bool init false;
|
|
passed_gate_5 : bool init false;
|
|
|
|
[left] !passed_gate_1 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1));
|
|
[right] !passed_gate_1 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1));
|
|
[noop] !passed_gate_1 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1));
|
|
|
|
[left] !passed_gate_2 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2));
|
|
[right] !passed_gate_2 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2));
|
|
[noop] !passed_gate_2 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2));
|
|
|
|
[left] !passed_gate_3 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3));
|
|
[right] !passed_gate_3 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3));
|
|
[noop] !passed_gate_3 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3));
|
|
|
|
[left] !passed_gate_4 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4));
|
|
[right] !passed_gate_4 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4));
|
|
[noop] !passed_gate_4 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4));
|
|
|
|
[left] !passed_gate_5 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5));
|
|
[right] !passed_gate_5 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5));
|
|
[noop] !passed_gate_5 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5));
|
|
|
|
[left] !done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate));
|
|
[right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate));
|
|
[noop] !done & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate));
|
|
|
|
//[left] done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
|
|
//[right] done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1);
|
|
//[noop] done & move=0 -> (move'=1);
|
|
[done] done -> true;
|
|
endmodule
|
|
|
|
module updateY
|
|
y : [initY..maxY] init initY;
|
|
standstill : [0..8] init 0;
|
|
[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] init initX;
|
|
|
|
[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_1 & Passed_Gate_1: 100;
|
|
[right] !passed_gate_1 & Passed_Gate_1: 100;
|
|
[noop] !passed_gate_1 & Passed_Gate_1: 100;
|
|
|
|
[left] !passed_gate_2 & Passed_Gate_2: 100;
|
|
[right] !passed_gate_2 & Passed_Gate_2: 100;
|
|
[noop] !passed_gate_2 & Passed_Gate_2: 100;
|
|
|
|
[left] !passed_gate_3 & Passed_Gate_3: 100;
|
|
[right] !passed_gate_3 & Passed_Gate_3: 100;
|
|
[noop] !passed_gate_3 & Passed_Gate_3: 100;
|
|
|
|
[left] !passed_gate_4 & Passed_Gate_4: 100;
|
|
[right] !passed_gate_4 & Passed_Gate_4: 100;
|
|
[noop] !passed_gate_4 & Passed_Gate_4: 100;
|
|
|
|
[left] !passed_gate_5 & Passed_Gate_5: 100;
|
|
[right] !passed_gate_5 & Passed_Gate_5: 100;
|
|
[noop] !passed_gate_5 & Passed_Gate_5: 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
|