% Sequential, Temporal Golog Program for a Coffee Delivery Robot

% GOLOG Procedures 

proc(deliverCoffee(T),
  ?(some(t, now(t) & t $<= T)) :
  (?(all(p,all(t1,all(t2,wantsCoffee(p,t1,t2) => hasCoffee(p))))) 
   #
   pi(rloc, ?(robotLocation(rloc)) :
            if(rloc = cm, /* THEN */ deliverOneCoffee(T),
                          /* ELSE */ goto(cm,T) : pi(t, ?(now(t)) : 
                                                     deliverOneCoffee(t))) :
            pi(t, ?(now(t)) : deliverCoffee(t))))).

proc(deliverOneCoffee(T),
  pi(p, pi(t1, pi(t2, pi(wait, pi(travTime,
     ?(wantsCoffee(p,t1,t2) & -hasCoffee(p) & (wait $>= 0) &
       travelTime(cm,office(p),travTime) & 
       t1 $<= T + wait + travTime & T + wait + travTime $<= t2) :
     pi(t, ?(t $= T + wait) : pickupCoffee(t)) :
     pi(t, ?(now(t)) : goto(office(p),t)) :
     pi(t, ?(now(t)) : giveCoffee(p,t)))))))). 


proc(goto(L,T),
  pi(rloc,?(robotLocation(rloc)) : pi(deltat,?(travelTime(rloc,L,deltat)) :
     goBetween(rloc,L,deltat,T)))).

proc(goBetween(Loc1,Loc2,Delta,T),
   startGo(Loc1,Loc2,T) :
   pi(t, ?(t $= T + Delta) : endGo(Loc1,Loc2,t))).

% Preconditions for Primitive Actions.

poss(pickupCoffee(T),S) :- not holdingCoffee(S),
                           robotLocation(cm,S).

poss(giveCoffee(Person,T),S) :- holdingCoffee(S),
                                robotLocation(office(Person),S).

poss(startGo(Loc1,Loc2,T),S) :- not going(L,LL,S), not Loc1 = Loc2,
                                robotLocation(Loc1,S).

poss(endGo(Loc1,Loc2,T),S) :- going(Loc1,Loc2,S).

% Successor State Axioms.

hasCoffee(Person,do(A,S)) :- A = giveCoffee(Person,T) ;
                             hasCoffee(Person,S).

robotLocation(Loc,do(A,S)) :- A = endGo(Loc1,Loc,T) ;
                                         (robotLocation(Loc,S),
                                          not A = endGo(Loc2,Loc3,T)).

going(Loc1,Loc2,do(A,S)) :- A = startGo(Loc1,Loc2,T) ;
                                   (going(Loc1,Loc2,S),
                                    not A = endGo(Loc1,Loc2,T)).

holdingCoffee(do(A,S)) :- A = pickupCoffee(T) ;
                                (holdingCoffee(S),
                                 not A = giveCoffee(Person,T)).


% Initial Situation.

robotLocation(cm,s0).

start(s0,0).

wantsCoffee(sue,140,160).
wantsCoffee(bill,100,110).
wantsCoffee(joe,90,100).
wantsCoffee(mary,130,170).

travelTime0(cm,office(sue),15).
travelTime0(cm,office(mary),10).
travelTime0(cm,office(bill),8).
travelTime0(cm,office(joe),10).

travelTime(L,L,0).
travelTime(L1,L2,T) :- travelTime0(L1,L2,T) ;
                       travelTime0(L2,L1,T).

% The time of an action occurrence is its last argument.

time(pickupCoffee(T),T).       time(giveCoffee(Person,T),T).
time(startGo(Loc1,Loc2,T),T).  time(endGo(Loc1,Loc2,T),T).

% Restore situation arguments to fluents. 

restoreSitArg(robotLocation(Rloc),S,robotLocation(Rloc,S)).
restoreSitArg(hasCoffee(Person),S,hasCoffee(Person,S)).
restoreSitArg(going(Loc1,Loc2),S,going(Loc1,Loc2,S)).
restoreSitArg(holdingCoffee,S,holdingCoffee(S)).

% Primitive Action Declarations.

primitive_action(pickupCoffee(T)).
primitive_action(giveCoffee(Person,T)).
primitive_action(startGo(Loc1,Loc2,T)).
primitive_action(endGo(Loc1,Loc2,T)).

% Fix on a solution to the temporal constraints. 

chooseTimes(s0).
chooseTimes(do(A,S)) :- chooseTimes(S), time(A,T), rmin(T).

% "now" is a synonym for "start".

now(S,T) :- start(S,T).
restoreSitArg(now(T),S,now(S,T)).

%  Utilities. 

prettyPrintSituation(S) :- makeActionList(S,Alist), nl, write(Alist), nl. 
 
makeActionList(s0,[]).
makeActionList(do(A,S), L) :- makeActionList(S,L1), append(L1, [A], L).
 
coffeeDelivery(T) :- do(deliverCoffee(T),s0,S), chooseTimes(S),
                     prettyPrintSituation(S), askForMore.                       
 
askForMore :- write('More? '), read(n).