sp
/
Skiing
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added another version of the MDP

main
sp 2 years ago
parent
5156803080
commit
aaf83f61b1
1 changed files with 115 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 115
      velocity.prism

115
velocity.prism
View File

@ -0,0 +1,115 @@
mdp
const int initY = 40;
const int initX = 80;
const int maxY = 210;
const int minX = 4;
const int maxX = 144;
formula Gate_1 = ((42<x & x<50 | 74<x & x=80) & 184<y & y<172);
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>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;
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] ;
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 = 14) & standstill>=5 -> (standstill'=min(8,standstill+1)) & (move'=3);
[update_y] move=2 & (ski_position=1 | ski_position = 14) & standstill<5 -> (velocity'=max(0,velocity-4)) &(move'=3);
[update_y] move=2 & (ski_position=2 | ski_position = 3 | ski_position = 12 | ski_position = 13) -> (velocity'=max(0 ,velocity-2)) & (standstill'=0) & (move'=3);
[update_y] move=2 & (ski_position=4 | ski_position = 5 | ski_position = 10 | ski_position = 11) -> (velocity'=min(16,velocity+2)) & (standstill'=0) & (move'=3);
[update_y] move=2 & (ski_position=6 | ski_position = 7 | ski_position = 8 | ski_position = 9) -> (velocity'=min(16,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=7 | ski_position=8) -> (move'=0);
[update_x] move=3 & 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=3 & 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=3 & 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=3 & 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=3 & 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=3 & 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=3 & 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=3 & 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
Write Preview
Loading…
Cancel
Save