// Two robots moving over a grid // One tries to move from the SW corner to the NE corner while the other does the reverse // When moving, a robot can end up in an adjacent grid square with probability q // concurrent game model csg // the players player robot1 robot1 endplayer player robot2 robot2 endplayer const double q; // probability of movement failure const int l; // size of grid // corner points const int xmin = 0; const int ymin = 0; const int xmax = l-1; const int ymax = l-1; // initial grid positions for the robots const int xi1 = xmin; const int yi1 = ymin; const int xi2 = xmax; const int yi2 = ymax; // goal grid positions for the robots const int xg1 = xmax; const int yg1 = ymax; const int xg2 = xmin; const int yg2 = ymin; // add labels for specifying properties label "goal1" = x1=xg1 & y1=yg1; label "goal2" = x2=xg2 & y2=yg2; // robots crash when they end up in same grid square label "crash" = x1=x2 & y1=y2; // first robot module robot1 x1 : [xmin..xmax] init xi1; // x coordinate y1 : [ymin..ymax] init yi1; // y coordinate [n1] y1 (1-q) : (y1'=y1+1) + q/2 : (y1'=y1+1) & (x1'=min(xmax,x1+1)) + q/2 : (y1'=y1+1) & (x1'=max(xmin,x1-1)); [e1] x1 (1-q) : (x1'=x1+1) + q/2 : (x1'=x1+1) & (y1'=min(ymax,y1+1)) + q/2 : (x1'=x1+1) & (y1'=max(ymin,y1-1)); [ne1] y1 (1-q) : (y1'=y1+1) & (x1'=x1+1) + q/2 : (y1'=y1+1) + q/2 : (x1'=x1+1); [done1] y1=yg1 & x1=xg1 -> true; endmodule // second robot module robot2 x2 : [xmin..xmax] init xi2; // x coordinate y2 : [ymin..ymax] init yi2; // y coordinate [s2] y2>ymin -> (1-q) : (y2'=y2-1) + q/2 : (y2'=y2-1) & (x2'=min(xmax,x2+1)) + q/2 : (y2'=y2-1) & (x2'=max(xmin,x2-1)); [w2] x2>xmin -> (1-q) : (x2'=x2-1) + q/2 : (x2'=x2-1) & (y2'=min(ymax,y2+1)) + q/2 : (x2'=x2-1) & (y2'=max(ymin,y2-1)); [sw2] y2>ymin & x2>xmin -> (1-q) : (y2'=y2-1) & (x2'=x2-1) + q/2 : (y2'=y2-1) + q/2 : (x2'=x2-1); [done2] y2=yg2 & x2=xg2 -> true; endmodule // rewards for robot 1 rewards "time1" [] !(x1=x2 & y1=y2) & !(y1=yg1 & x1=xg1) : 1; [] x1=x2 & y1=y2 & !(y1=yg1 & x1=xg1) : 10; // recovering from a crash takes 10 time units endrewards // rewards for robot 2 rewards "time2" [] !(x1=x2 & y1=y2) & !(y2=yg2 & x2=xg2) : 1; [] x1=x2 & y1=y2 & !(y2=yg2 & x2=xg2) : 10; // recovering from a crash takes 10 time units endrewards