Skiing/simplified.prism

mdp

const int initY = 40;
const int initX = 80;

const int maxY = 600;
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>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<=134) & (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] init 0;

module skier
  ski_position : [1..14] init 8;
  done : bool init false;

  passed_gate : bool init false;

  [left]  !passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate));
  [right] !passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate));
  [noop]  !passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Passed_Gate));

  [left]  passed_gate & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate));
  [right] passed_gate & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_Gate));
  [noop]  passed_gate & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate'=(Left_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 & 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