%const length = 15.
%const p=3.  -- 4 persons
%const n=7.  -- 8 floors

person(0..p).
floor(0..n).

goal(T):- time(T), trans(control, 0, T).
goal(T+1):- time(T), T < length, goal(T).

:- not goal(length).

proc(serve(P,O,D)):- person(P),floor(O),floor(D).
head(serve(P,O,D), origin(P,O)):- person(P),floor(O),floor(D).
tail(serve(P,O,D), nextgo(P,O,D)):-person(P),floor(O),floor(D).

proc(nextgo(P,O,D)):- person(P),floor(O),floor(D).
head(nextgo(P,O,D), destination(P,D)):- person(P),floor(O),floor(D).
tail(nextgo(P,O,D), op(P,O,D)):- person(P),floor(O),floor(D).

proc(op(P,O,D)):- person(P),floor(O),floor(D).
head(op(P,O,D), p(O)):- person(P),floor(O),floor(D).
tail(op(P,O,D), go(P,O,D)):- person(P),floor(O),floor(D).

proc(go(P,O,D)):- person(P),floor(O),floor(D).
head(go(P,O,D), board(O,P)):- person(P),floor(O),floor(D).
tail(go(P,O,D), done(P,O,D)):- person(P),floor(O),floor(D).

proc(done(P,O,D)):- person(P),floor(O),floor(D).
head(done(P,O,D), p(D)):- person(P),floor(O),floor(D).
tail(done(P,O,D), depart(D,P)):- person(P),floor(O),floor(D).

choiceAction(p(O)):- floor(O).

in(up(N,O), p(O)):- floor(O),floor(N).
in(down(N,O), p(O)):- floor(N),floor(O).
in(lift_at(O), p(O)):- floor(O).

%proc(control).
%head(control, wloop).
%tail(control, null).

while(control, needService, one).

is_formula(needService).

exists(needService, existOn(P,O,D)):- person(P),floor(O),floor(D).

is_formula(existOn(P,O,D)):- person(P),floor(O),floor(D).
is_formula(pAtO(P,O)):- person(P),floor(O).
is_formula(pToD(P,D)):- person(P),floor(D).

isand(pAtO(P,O), neg(served(P)), origin(P,O)):- person(P),floor(O).
isand(pToD(P,D), neg(served(P)), destination(P,D)):- person(P),floor(D).
isand(existOn(P,O,D), pAtO(P,O), pToD(P,D)):- person(P),floor(O),floor(D).

choiceArgs(one,existOn(P,O,D),serve(P,O,D)):-
    person(P),floor(O),floor(D).

hide person(P).
hide floor(F).