////////////////////////////////////////////////////////////////////
//
// 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;
//		
//	};
	
}
