////////////////////////////////////////////////////////////////////
// Elevator Domain
//
// Author: Tom Walsh (thomasjwalsh [at] gmail.com)
//
// Edited for competition and translation purposes by Scott Sanner.
//
// The "elevators" domain has a number of elevators delivering passengers 
// to either the top or the bottom floor (the only allowable destinations).
// Potential passengers arrive at a floor based on Bernoulli draws 
// with a potentially different arrival probability for each floor.  
//
// The elevator can move in its current direction if the doors are closed,
// can remain stationary (noop), or can open its door while indicating
// the direction that it will go in next (this allows potential passengers
// to determine whether to board or not).  Note that the elevator can only
// change direction by opening its door while indicating the opposite 
// direction. 
//
// A passable plan in this domain is to pick up a passenger every time 
// they appear and take them to their destination.  A better plan includes 
// having the elevator "hover" near floors where passengers are likely to 
// arrive and coordinating multiple elevators for up and down passengers.
//
// This domain was designed to support extension to multiple elevators
// and may be used in either single or multi-elevator mode.
////////////////////////////////////////////////////////////////////

domain elevators_mdp {
	
	requirements = { 
		constrained-state,
		reward-deterministic
	};
	
	types {
  		elevator : object;
 	  	floor    : object;
	}; 
	
	pvariables { 
	
		// Probability someone arrives at the floor (up or down)
		ARRIVE-PARAM(floor) : { non-fluent, real, default = 0.0 }; 		  		
		
		// Penalty for persons in the elevator going in right/wrong direction
		// Note: a constant 1.0 penalty for people waiting at a floor 
		ELEVATOR-PENALTY-RIGHT-DIR : { non-fluent, real, default = 0.75 };
		ELEVATOR-PENALTY-WRONG-DIR : { non-fluent, real, default = 3.00 };

		// Useful definitions
		TOP-FLOOR(floor)          : { non-fluent, bool, default = false };
   		BOTTOM-FLOOR(floor)       : { non-fluent, bool, default = false };
		ADJACENT-UP(floor, floor) : { non-fluent, bool, default = false }; 		  		
		
		// Person waiting state
		person-waiting-up(floor)   : { state-fluent, bool, default = false };
		person-waiting-down(floor) : { state-fluent, bool, default = false };
		person-in-elevator-going-up(elevator)   : { state-fluent, bool, default = false };
		person-in-elevator-going-down(elevator) : { state-fluent, bool, default = false };
		
		// Elevator state
		elevator-dir-up(elevator) : { state-fluent, bool, default = true };
		elevator-closed(elevator) : { state-fluent, bool, default = true };
		elevator-at-floor(elevator, floor) : { state-fluent, bool, default = false };

		// Actions: the elevator must move in one direction, it can only switch
		//          direction by signaling the change when the door opens
		//          (i.e., the passengers must know which direction the 
		//           elevator is going before they get on... then the elevator
		//           is constrained to go in that direction when the door closes).
		move-current-dir(elevator)     : { action-fluent, bool, default = false };
		open-door-going-up(elevator)   : { action-fluent, bool, default = false };
		open-door-going-down(elevator) : { action-fluent, bool, default = false };
		close-door(elevator)           : { action-fluent, bool, default = false };
	};
  
	cpfs {
		
		// We might even allow people to get off the elevator if it switches
		// directions on them while they're in it, but we won't model this now.
		
		// A person is waiting unless they get on an elevator going in their
		// direction.
		person-waiting-up'(?f) = 
			if (person-waiting-up(?f) ^ 
				~exists_{?e: elevator} [elevator-at-floor(?e, ?f) ^ elevator-dir-up(?e) ^ ~elevator-closed(?e)])
			then KronDelta(true) 
			else Bernoulli(ARRIVE-PARAM(?f));
			
		person-waiting-down'(?f) = 
			if (person-waiting-down(?f) ^ 
				~exists_{?e: elevator} [elevator-at-floor(?e, ?f) ^ ~elevator-dir-up(?e) ^ ~elevator-closed(?e)])
			then KronDelta(true) 
			else Bernoulli(ARRIVE-PARAM(?f));
  		
  		// A person is in the elevator going in a direction if someone gets on 
  		// in that direction or someone was already on in that direction and does
  		// not get off.
  		person-in-elevator-going-up'(?e) = 
  			if (person-in-elevator-going-up(?e))
  				// If elevator not at top floor then stays true, otherwise set to false
  				then KronDelta( ~exists_{?f : floor} [elevator-at-floor(?e, ?f) ^ TOP-FLOOR(?f)] )
  			else
  				// No one in elevator going up... can only be true if someone going up gets in
  				KronDelta( exists_{?f : floor} 
  					[ elevator-at-floor(?e, ?f) ^ elevator-dir-up(?e) ^ 
  					  ~elevator-closed(?e) ^ person-waiting-up(?f) ] );

  		person-in-elevator-going-down'(?e) = 
  			if (person-in-elevator-going-down(?e))
  				// If elevator not at bottom floor then stays true, otherwise set to false
  				then KronDelta( ~exists_{?f : floor} [elevator-at-floor(?e, ?f) ^ BOTTOM-FLOOR(?f)] )
  			else
  				// No one in elevator going up... can only be true if someone going up gets in
  				KronDelta( exists_{?f : floor} 
  					[ elevator-at-floor(?e, ?f) ^ ~elevator-dir-up(?e) ^ 
  					  ~elevator-closed(?e) ^ person-waiting-down(?f) ] );
  		      
		// Elevator needs to be explicitly closed
		elevator-closed'(?e) = 
			KronDelta([elevator-closed(?e) ^ ~open-door-going-up(?e) ^ ~open-door-going-down(?e)] 
					  | close-door(?e));

		// Elevator's destination is set when door is opened (to signal
		// to people which direction the elevator is going)
		elevator-dir-up'(?e) = 
			if (open-door-going-up(?e))
				then KronDelta(true)
			else if (open-door-going-down(?e))
				then KronDelta(false)
			else 
				// If not explicitly set then previous direction persists
				KronDelta( elevator-dir-up(?e) );
		
		// Elevator movement
		//
		// Note: if the elevator should pause at a floor, it can simply open
		//       do noops (all actions false).
		elevator-at-floor'(?e, ?f) =
		
			//////////////////////////////////////////////////////////////////
			// Elevator does not move if door is open or elevator does not move
			//////////////////////////////////////////////////////////////////
			if (~elevator-closed(?e) | ~move-current-dir(?e))
				then KronDelta( elevator-at-floor(?e, ?f) )

			//////////////////////////////////////////////////////////////////
			// These handle the floor that is moved to
			//////////////////////////////////////////////////////////////////
			else if (move-current-dir(?e) ^ elevator-dir-up(?e) ^ exists_{?cur : floor} 
					 [elevator-at-floor(?e, ?cur) ^ ADJACENT-UP(?cur,?f)])
				then KronDelta(true)
			else if (move-current-dir(?e) ^ ~elevator-dir-up(?e) ^ exists_{?cur : floor} 
						[elevator-at-floor(?e, ?cur) ^ ADJACENT-UP(?f,?cur)])
				then KronDelta(true)

			//////////////////////////////////////////////////////////////////
			// These handle failed actions -- stay at current floor
			//////////////////////////////////////////////////////////////////
			else if (move-current-dir(?e) ^ elevator-dir-up(?e) ^ ~exists_{?next : floor} 
					 [elevator-at-floor(?e, ?f) ^ ADJACENT-UP(?f,?next)])
				then KronDelta( elevator-at-floor(?e, ?f) )
			else if (move-current-dir(?e) ^ ~elevator-dir-up(?e) ^ ~exists_{?next : floor} 
						[elevator-at-floor(?e, ?f) ^ ADJACENT-UP(?next,?f)])
				then KronDelta( elevator-at-floor(?e, ?f) )

			//////////////////////////////////////////////////////////////////
			// Otherwise elevator ?e does not move to floor ?f
			//////////////////////////////////////////////////////////////////
			else
				// If here, state persists
				KronDelta( false ); 
	};
  
  	// Reward is a sum of waiting penalties for those in elevators and at floor
	reward = 
		[sum_{?e: elevator} [
			-ELEVATOR-PENALTY-RIGHT-DIR * (person-in-elevator-going-up(?e) ^ elevator-dir-up(?e))
		]] + 
		[sum_{?e: elevator} [
			-ELEVATOR-PENALTY-RIGHT-DIR * (person-in-elevator-going-down(?e) ^ ~elevator-dir-up(?e))
		]] + 
		[sum_{?e: elevator} [
			-ELEVATOR-PENALTY-WRONG-DIR * (person-in-elevator-going-up(?e) ^ ~elevator-dir-up(?e))
		]] + 
		[sum_{?e: elevator} [
			-ELEVATOR-PENALTY-WRONG-DIR * (person-in-elevator-going-down(?e) ^ elevator-dir-up(?e))
		]] + 
		[sum_{?f: floor} [
			- person-waiting-up(?f) - person-waiting-down(?f)
		]];

	state-action-constraints {
		// Can check uniqueness constraint in many ways, but for simulator easiest 
		// is just to count.
//		forall_{?e : elevator} ([sum_{?f: floor} elevator-at-floor(?e, ?f)] == 1);
		
		// Max of one action per elevator.
		forall_{?e : elevator} [(open-door-going-up(?e) + open-door-going-down(?e) + close-door(?e) + move-current-dir(?e)) <= 1];
		
		// All floors except top and bottom must have one adjacent floor above/below
//		forall_{?f : floor} [ TOP-FLOOR(?f) | (sum_{?fup : floor} ADJACENT-UP(?f,?fup)) == 1 ];
//		forall_{?f : floor} [ BOTTOM-FLOOR(?f) | (sum_{?fdown : floor} ADJACENT-UP(?fdown,?f)) == 1 ];
	};
}
