tempestpy/lib/stormpy/examples/files/smg/safety_shield_robot.prism

smg

player shieldedRobot
  [e1], [w1], [n1], [s1]
endplayer

player adverseryRobot
  [e2], [w2], [n2], [s2]
endplayer

// (w+1)x16 - grid
//const int w;
const int width = 6;
const int height = 15;

const int xmin = 0;
const int xmax = width;
const int ymin = 0;
const int ymax = height;

// probabilty to get stuck
const double stuckProp = 1/5;
const double notstuckProp = 1 - stuckProp;

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

formula robot1BetweenShelves = !(y1=0 | y1=height);
formula robot2BetweenShelves = !(y2=0 | y2=height);
formula robot1AboveShelves = mod(x1, 2) = 1;
formula robot1BelowShelves = mod(x1, 2) = 1;
formula robot2AboveShelves = mod(x2, 2) = 1;
formula robot2BelowShelves = mod(x2, 2) = 1;
formula robot1OpenRow = mod(y1, 5) = 0;
formula robot2OpenRow = mod(y2, 5) = 0;

label "crash" = x1=x2 & y1=y2;

module robot1
  x1 : [0..width] init 0;
  y1 : [0..height] init ymax;

  [e1]    move=0 & x1<xmax & (!robot1BetweenShelves | robot1OpenRow) -> (x1'=x1+1) & (move'=1);
  [w1]    move=0 & x1>0    & (!robot1BetweenShelves | robot1OpenRow) -> (x1'=x1-1) & (move'=1);

  [n1]    move=0 & y1>0    & !robot1BelowShelves -> (y1'=y1-1) & (move'=1);
  [s1]    move=0 & y1<ymax & !robot1AboveShelves -> (y1'=y1+1) & (move'=1);
endmodule

module robot2
  x2 : [0..width] init xmax;
  y2 : [0..height] init 0;

  [e2]    move=1 & x2<xmax & (!robot2BetweenShelves | robot2OpenRow) -> notstuckProp : (x2'=x2+1) & (move'=0) + stuckProp : (move'=0);
  [w2]    move=1 & x2>0    & (!robot2BetweenShelves | robot2OpenRow) -> notstuckProp : (x2'=x2-1) & (move'=0) + stuckProp : (move'=0);

  [n2]    move=1 & y2>0    & !robot2BelowShelves -> notstuckProp : (y2'=y2-1) & (move'=0) + stuckProp : (move'=0);
  [s2]    move=1 & y2<ymax & !robot2AboveShelves -> notstuckProp : (y2'=y2+1) & (move'=0) + stuckProp : (move'=0);
endmodule