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.
65 lines
4.4 KiB
65 lines
4.4 KiB
smg
|
|
|
|
player Agent
|
|
[Agent_move_north], [Agent_move_east], [Agent_move_south], [Agent_move_west], [Agent_turn_left], [Agent_turn_right]
|
|
endplayer
|
|
player Blue
|
|
[Blue_move_north], [Blue_move_east], [Blue_move_south], [Blue_move_west], [Blue_turns]
|
|
endplayer
|
|
|
|
global move : [0..1] init 0;
|
|
|
|
label AgentOnBlue = (xAgent=1&yAgent=1) | (xAgent=1&yAgent=4) | (xAgent=1&yAgent=5) | (xAgent=2&yAgent=1) | (xAgent=2&yAgent=5);
|
|
label BlueOnBlue = (xBlue=1&yBlue=1) | (xBlue=1&yBlue=4) | (xBlue=1&yBlue=5) | (xBlue=2&yBlue=1) | (xBlue=2&yBlue=5);
|
|
label AgentOnGreen = (xAgent=3&yAgent=1) | (xAgent=3&yAgent=2) | (xAgent=3&yAgent=3) | (xAgent=3&yAgent=4) | (xAgent=3&yAgent=5) | (xAgent=4&yAgent=1) | (xAgent=4&yAgent=5) | (xAgent=5&yAgent=1) | (xAgent=5&yAgent=2) | (xAgent=5&yAgent=3) | (xAgent=5&yAgent=4) | (xAgent=5&yAgent=5);
|
|
label BlueOnGreen = (xBlue=3&yBlue=1) | (xBlue=3&yBlue=2) | (xBlue=3&yBlue=3) | (xBlue=3&yBlue=4) | (xBlue=3&yBlue=5) | (xBlue=4&yBlue=1) | (xBlue=4&yBlue=5) | (xBlue=5&yBlue=1) | (xBlue=5&yBlue=2) | (xBlue=5&yBlue=3) | (xBlue=5&yBlue=4) | (xBlue=5&yBlue=5);
|
|
label AgentOnRed = (xAgent=1&yAgent=2) | (xAgent=1&yAgent=3);
|
|
label BlueOnRed = (xBlue=1&yBlue=2) | (xBlue=1&yBlue=3);
|
|
formula AgentCannotMoveNorth = (xAgent=1&yAgent=2) | (xAgent=1&yAgent=3) | (xAgent=1&yAgent=4) | (xAgent=1&yAgent=5) | (xAgent=3&yAgent=2) | (xAgent=3&yAgent=4) | (xAgent=5&yAgent=2) | (xAgent=5&yAgent=4) | (xAgent=3&yAgent=3) | (xAgent=5&yAgent=3) | (xAgent=1&yAgent=1);
|
|
formula AgentCannotMoveEast = (xAgent=1&yAgent=5) | (xAgent=2&yAgent=1) | (xAgent=2&yAgent=5) | (xAgent=3&yAgent=5) | (xAgent=4&yAgent=5) | (xAgent=4&yAgent=1) | (xAgent=5&yAgent=5);
|
|
formula AgentCannotMoveSouth = (xAgent=1&yAgent=2) | (xAgent=1&yAgent=3) | (xAgent=1&yAgent=4) | (xAgent=3&yAgent=2) | (xAgent=3&yAgent=4) | (xAgent=5&yAgent=1) | (xAgent=5&yAgent=2) | (xAgent=5&yAgent=4) | (xAgent=3&yAgent=3) | (xAgent=5&yAgent=3) | (xAgent=5&yAgent=5);
|
|
formula AgentCannotMoveWest = (xAgent=2&yAgent=1) | (xAgent=2&yAgent=5) | (xAgent=3&yAgent=1) | (xAgent=4&yAgent=5) | (xAgent=5&yAgent=1) | (xAgent=1&yAgent=1) | (xAgent=4&yAgent=1);
|
|
formula AgentIsOnSlippery = false;
|
|
|
|
label AgentGoal = false;
|
|
formula BlueCannotMoveNorth = (xBlue=1&yBlue=2) | (xBlue=1&yBlue=3) | (xBlue=1&yBlue=4) | (xBlue=1&yBlue=5) | (xBlue=3&yBlue=2) | (xBlue=3&yBlue=4) | (xBlue=5&yBlue=2) | (xBlue=5&yBlue=4) | (xBlue=3&yBlue=3) | (xBlue=5&yBlue=3) | (xBlue=1&yBlue=1);
|
|
formula BlueCannotMoveEast = (xBlue=1&yBlue=5) | (xBlue=2&yBlue=1) | (xBlue=2&yBlue=5) | (xBlue=3&yBlue=5) | (xBlue=4&yBlue=5) | (xBlue=4&yBlue=1) | (xBlue=5&yBlue=5);
|
|
formula BlueCannotMoveSouth = (xBlue=1&yBlue=2) | (xBlue=1&yBlue=3) | (xBlue=1&yBlue=4) | (xBlue=3&yBlue=2) | (xBlue=3&yBlue=4) | (xBlue=5&yBlue=1) | (xBlue=5&yBlue=2) | (xBlue=5&yBlue=4) | (xBlue=3&yBlue=3) | (xBlue=5&yBlue=3) | (xBlue=5&yBlue=5);
|
|
formula BlueCannotMoveWest = (xBlue=2&yBlue=1) | (xBlue=2&yBlue=5) | (xBlue=3&yBlue=1) | (xBlue=4&yBlue=5) | (xBlue=5&yBlue=1) | (xBlue=1&yBlue=1) | (xBlue=4&yBlue=1);
|
|
formula BlueIsOnSlippery = false;
|
|
|
|
label BlueGoal = false;
|
|
label crash = (xAgent=xBlue)&(yAgent=yBlue);
|
|
|
|
module Agent
|
|
xAgent : [1..6] init 1;
|
|
yAgent : [1..6] init 1;
|
|
|
|
viewAgent : [0..3] init 1;
|
|
|
|
[Agent_turn_right] move=0 & true -> (viewAgent'=mod(viewAgent + 1, 4)) & (move'=1) ;
|
|
[Agent_turn_left] move=0 & viewAgent>0 -> (viewAgent'=viewAgent - 1) & (move'=1) ;
|
|
[Agent_turn_left] move=0 & viewAgent=0 -> (viewAgent'=3) & (move'=1) ;
|
|
|
|
|
|
[Agent_move_north] move=0 & viewAgent=3 & !AgentIsOnSlippery & !AgentCannotMoveNorth -> (xAgent'=xAgent-1) & (move'=1) ;
|
|
[Agent_move_east] move=0 & viewAgent=0 & !AgentIsOnSlippery & !AgentCannotMoveEast -> (yAgent'=yAgent+1) & (move'=1) ;
|
|
[Agent_move_south] move=0 & viewAgent=1 & !AgentIsOnSlippery & !AgentCannotMoveSouth -> (xAgent'=xAgent+1) & (move'=1) ;
|
|
[Agent_move_west] move=0 & viewAgent=2 & !AgentIsOnSlippery & !AgentCannotMoveWest -> (yAgent'=yAgent-1) & (move'=1) ;
|
|
|
|
endmodule
|
|
|
|
module Blue
|
|
xBlue : [1..6] init 5;
|
|
yBlue : [1..6] init 5;
|
|
|
|
[Blue_turns] move=1 & true -> (xBlue'=xBlue) & (move'=0) ;
|
|
|
|
|
|
[Blue_move_north] move=1 & !BlueIsOnSlippery & !BlueCannotMoveNorth -> (xBlue'=xBlue-1) & (move'=0) ;
|
|
[Blue_move_east] move=1 & !BlueIsOnSlippery & !BlueCannotMoveEast -> (yBlue'=yBlue+1) & (move'=0) ;
|
|
[Blue_move_south] move=1 & !BlueIsOnSlippery & !BlueCannotMoveSouth -> (xBlue'=xBlue+1) & (move'=0) ;
|
|
[Blue_move_west] move=1 & !BlueIsOnSlippery & !BlueCannotMoveWest -> (yBlue'=yBlue-1) & (move'=0) ;
|
|
|
|
endmodule
|
|
|