Skiing/first_try.prism

mdp

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

const int maxY = 240;
const int minX = 12;
const int maxX = 147;


formula HitTree = (122<x & x<139) & (220<y & y=232);
formula HitGate = ((x=51 | x=79) & y=164);

formula PassedGates = (158<y & y<165 & 51<x & x<79);

global move : [0..3] init 0;

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

  [left]  !done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate));
  [right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate));
  [noop]  !done & move=0 -> (move'=1) & (done'=(PassedGates|HitTree|HitGate));

  [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);

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-3)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-5)) & (move'=0);
  [update_x]  move=2 & standstill<8 &  ski_position=9                      -> 0.1: (x'=min(maxX,x+3)) + 0.7: (x'=min(maxX,x+4)) + 0.2: (x'=min(maxX,x+5)) & (move'=0);

  [update_x]  move=2 & standstill<8 & (ski_position=4 | ski_position=5)    -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0);
  [update_x]  move=2 & standstill<8 & (ski_position=10 | ski_position=11)  -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (move'=0);

  [update_x]  move=2 & standstill<8 & (ski_position=2 | ski_position=3)    -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0);
  [update_x]  move=2 & standstill<8 & (ski_position=12 | ski_position=13)  -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (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-3)) & (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+3)) & (move'=0);
endmodule

rewards
  [left]  !done & PassedGates : 100;
  [right] !done & PassedGates : 100;
  [noop]  !done & PassedGates : 100;
  [left]  !done & (HitTree) : -200;
  [right] !done & (HitTree) : -200;
  [noop]  !done & (HitTree) : -200;
  [left]  !done & (HitGate) : -150;
  [right] !done & (HitGate) : -150;
  [noop]  !done & (HitGate) : -150;
endrewards