////////////////////////////////////////////////////////////////////
//
// Crossing Traffic Robot Navigation
//
// Author: Sungwook Yoon (sungwook.yoon [at] gmail.com)
//
// Modified for competition and translation purposes by Scott Sanner.
//
// In a grid, a robot (R) must get to a goal (G) and avoid obstacles (O)
// arriving randomly and moving left. If an obstacle overlaps with the
// robot, the robot disappears and can no longer move around. The robot
// can “duck” underneath a car by deliberately moving right/east when
// a car is to the right of it (this can make the solution interesting…
// the robot should start at the left side of the screen then). The robot
// receives -1 for every time step it has not reached the goal. The goal
// state is absorbing with 0 reward.
//
// ****************
// * R *
// * <-O <-O <-O *
// * <-O <-O *
// * <-O <-O *
// * <-O <-O *
// * G *
// ****************
//
// You can think of this as the RDDL version of Frogger:
//
// http://en.wikipedia.org/wiki/Frogger
//
////////////////////////////////////////////////////////////////////
domain crossing_traffic_mdp {
requirements = {
// constrained-state,
reward-deterministic
};
types {
xpos : object;
ypos : object;
};
pvariables {
NORTH(ypos, ypos) : {non-fluent, bool, default = false};
SOUTH(ypos, ypos) : {non-fluent, bool, default = false};
EAST(xpos, xpos) : {non-fluent, bool, default = false};
WEST(xpos, xpos) : {non-fluent, bool, default = false};
MIN-XPOS(xpos) : {non-fluent, bool, default = false};
MAX-XPOS(xpos) : {non-fluent, bool, default = false};
MIN-YPOS(ypos) : {non-fluent, bool, default = false};
MAX-YPOS(ypos) : {non-fluent, bool, default = false};
INPUT-RATE : {non-fluent, real, default = 0.2};
GOAL(xpos,ypos) : {non-fluent, bool, default = false};
// Fluents
robot-at(xpos, ypos) : {state-fluent, bool, default = false};
obstacle-at(xpos, ypos) : {state-fluent, bool, default = false};
// Actions
move-north : {action-fluent, bool, default = false};
move-south : {action-fluent, bool, default = false};
move-east : {action-fluent, bool, default = false};
move-west : {action-fluent, bool, default = false};
};
cpfs {
robot-at'(?x,?y) =
// Goal is absorbing so robot stays put
if ( GOAL(?x,?y) ^ robot-at(?x,?y) )
then
KronDelta(true)
else if ( exists_{?x2 : xpos, ?y2 : ypos} [ GOAL(?x2,?y2) ^ robot-at(?x2,?y2) ] )
then
KronDelta(false) // because of fall-through we know (?x,y) != (?x2,?y2)
// Check for legal robot movement (robot disappears if at an obstacle)
else if ( move-north ^ exists_{?y2 : ypos} [ NORTH(?y2,?y) ^ robot-at(?x,?y2) ^ ~obstacle-at(?x,?y2) ] )
then
KronDelta(true) // robot moves to this location
else if ( move-north ^ exists_{?y2 : ypos} [ NORTH(?y,?y2) ^ robot-at(?x,?y) ] )
then
KronDelta(false) // robot leaves this location
else if ( move-south ^ exists_{?y2 : ypos} [ SOUTH(?y2,?y) ^ robot-at(?x,?y2) ^ ~obstacle-at(?x,?y2) ] )
then
KronDelta(true) // robot moves to this location
else if ( move-south ^ exists_{?y2 : ypos} [ SOUTH(?y,?y2) ^ robot-at(?x,?y) ] )
then
KronDelta(false) // robot leaves this location
else if ( move-east ^ exists_{?x2 : xpos} [ EAST(?x2,?x) ^ robot-at(?x2,?y) ^ ~obstacle-at(?x2,?y) ] )
then
KronDelta(true) // robot moves to this location
else if ( move-east ^ exists_{?x2 : xpos} [ EAST(?x,?x2) ^ robot-at(?x,?y) ] )
then
KronDelta(false) // robot leaves this location
else if ( move-west ^ exists_{?x2 : xpos} [ WEST(?x2,?x) ^ robot-at(?x2,?y) ^ ~obstacle-at(?x2,?y) ] )
then
KronDelta(true) // robot moves to this location
else if ( move-west ^ exists_{?x2 : xpos} [ WEST(?x,?x2) ^ robot-at(?x,?y) ] )
then
KronDelta(false) // robot leaves this location
// A noop or illegal movement, so state unchanged
else
KronDelta( robot-at(?x,?y) ^ ~obstacle-at(?x,?y) );
obstacle-at'(?x, ?y) =
// No obstacles in top or bottom row (these rows are safe havens)
if ( MIN-YPOS(?y) | MAX-YPOS(?y) )
then KronDelta( false )
// Check for RHS border input cell
else if ( MAX-XPOS(?x) )
then Bernoulli( INPUT-RATE )
// Not a top or bottom row and not a border input cell -- inherits obstacle to east
else
KronDelta( exists_{?x2 : xpos} [EAST(?x,?x2) ^ obstacle-at(?x2,?y)] );
};
// 0 reward for reaching goal, -1 in all other cases
reward = [sum_{?x : xpos, ?y : ypos} -(GOAL(?x,?y) ^ ~robot-at(?x,?y))];
// state-action-constraints {
//
// // Robot at exactly one position
// [sum_{?x : xpos, ?y : ypos} robot-at(?x,?y)] <= 1;
//
// // EAST, WEST, NORTH, SOUTH defined properly (unique and symmetric)
// forall_{?x1 : xpos} [(sum_{?x2 : xpos} WEST(?x1,?x2)) <= 1];
// forall_{?x1 : xpos} [(sum_{?x2 : xpos} EAST(?x1,?x2)) <= 1];
// forall_{?y1 : ypos} [(sum_{?y2 : ypos} NORTH(?y1,?y2)) <= 1];
// forall_{?y1 : ypos} [(sum_{?y2 : ypos} SOUTH(?y1,?y2)) <= 1];
// forall_{?x1 : xpos, ?x2 : xpos} [ EAST(?x1,?x2) <=> WEST(?x2,?x1) ];
// forall_{?y1 : ypos, ?y2 : ypos} [ SOUTH(?y1,?y2) <=> NORTH(?y2,?y1) ];
//
// // Definition verification
// [ sum_{?x : xpos} MIN-XPOS(?x) ] == 1;
// [ sum_{?x : xpos} MAX-XPOS(?x) ] == 1;
// [ sum_{?y : ypos} MIN-YPOS(?y) ] == 1;
// [ sum_{?y : ypos} MAX-YPOS(?y) ] == 1;
// [ sum_{?x : xpos, ?y : ypos} GOAL(?x,?y) ] == 1;
//
// };
}