%const length = 8.

goal(T):- time(T), trans(wloop, 0, T).

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

:- not goal(length).

floor(0..5).

proc(serve(N)):- floor(N).

head(serve(N), go(N)):- floor(N).
tail(serve(N), nextgo(N)):- floor(N).

proc(nextgo(N)):- floor(N).
head(nextgo(N), open):- floor(N).
tail(nextgo(N), op(N)):- floor(N).

proc(op(N)):- floor(N).
head(op(N), turnoff(N)):- floor(N).
tail(op(N), close):- floor(N).

proc(go(N)):- floor(N).
head(go(N), p(N)):- floor(N).
tail(go(N), null):- floor(N).

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

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

%proc(serve_a_floor).
%head(serve_a_floor, s(N)):- floor(N).
%tail(serve_a_floor, null).

choiceArgs(serve_a_floor, on(N), serve(N)):- floor(N).

proc(control).
head(control, wloop).
tail(control, park).

while(wloop, existOn, serve_a_floor).

is_formula(existOn).

exists(existOn, on(N)):- floor(N).

proc(park).
head(park, if0).
tail(park, null).

if(if0, currentFloor(0), open, elsePark).

proc(elsePark).
head(elsePark, down(0)).
tail(elsePark, open).

% hiding output

hide floor(N).