You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
58 lines
1.8 KiB
58 lines
1.8 KiB
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
|