const length = 4.

:- not tran(serve(3),0,4).

%:- not tran(s1(3),0,4).

floor(0..5).

action(up(N)):- floor(N).
action(down(N)):- floor(N).
action(turnoff(N)):- floor(N).
action(open).
action(close).
action(null).


fluent(currentFloor(N)):- floor(N).
fluent(on(N)):- floor(N).
fluent(opened).

causes(up(N), currentFloor(N), nil):- floor(N).
causes(down(N), currentFloor(N), nil):- floor(N).
causes(turnoff(N), neg(on(N)), nil):- floor(N).
causes(open, opened, nil).
causes(close, neg(opened), nil).

holds(neg(currentFloor(N)), T):-
	time(T), floor(N), floor(M),
	holds(currentFloor(M), T),
	neq(N,M).

executable(up(N), above(N)):- floor(N).
executable(down(N), below(N)):- floor(N).
executable(turnoff(N), on(N)):- floor(N).
executable(open, true).
executable(close, true).
executable(null, true).

holds(true, T):- time(T).

holds(below(N), T):- 
	time(T), floor(N), floor(M), 
	holds(currentFloor(M), T), N < M, holds(neg(opened),T).

holds(above(N), T):- 
	time(T), floor(N), floor(M), 
	holds(currentFloor(M), T), N > M, holds(neg(opened),T).

initially(on(3)).
initially(on(5)).
initially(currentFloor(2)).
initially(neg(opened)).

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

first(s1(N), up(N)):- floor(N).
last(s1(N), nextgo(N)):- floor(N).


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

first(serve(N), go(N)):- floor(N).
last(serve(N), nextgo(N)):- floor(N).

proc(nextgo(N)):- floor(N).
first(nextgo(N), turnoff(N)):- floor(N).
last(nextgo(N), op):- floor(N).

proc(op).
first(op, open).
last(op, close).

proc(go(N)):- floor(N).
first(go(N), p(N)):- floor(N).
last(go(N), null):- floor(N).

pin(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).


hide floor(N).

:- time(T), occ(null,T).