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