% Train Rescheduling encoding (without alternative routes). Conflicts are resolved
% by delaying trains on tracks.
% current_schedule_* provides the current routes and times
% solved_schedule_ is the fixed schedule

% Required input: -> see rescheduling_delay.lp

cspdomain(fd).

#const overlappingTime = 1.

% ----------------- CSP VARIABLES -----------------

% definition of csp variables solved_schedule_*
cspvar(solved_schedule_begin(TRAIN,TRACK),MINTIME,MAXTIME) :-
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	maxTime(MAXTIME), minTime(MINTIME).

cspvar(solved_schedule_end(TRAIN,TRACK),MINTIME,MAXTIME) :-
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	maxTime(MAXTIME), minTime(MINTIME).

% definition of csp variables actualDelay
cspvar(actualDelay(TRAIN,TRACK),MINDELAY,MAXDELAY) :-
	minDelay(MINDELAY), maxDelay(MAXDELAY),
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	current_schedule_stay(TRAIN,TRACK,STAY).

% ----------------- CONSTRAINTS -----------------

% derive stay of trains on tracks from current schedule
current_schedule_stay(TRAIN,TRACK,STAY) :-
    current_schedule_begin(TRAIN,TRACK,BEGIN),
    current_schedule_end(TRAIN,TRACK,END),
    STAY = END-BEGIN.

% all trains with begin and end times <= current time stay the same
% because they lie in the past
required(solved_schedule_begin(TRAIN,TRACK) == BEGIN) :- 
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	current_time(TIME),
	BEGIN <= TIME.

required(solved_schedule_end(TRAIN,TRACK) == END) :-
	current_schedule_end(TRAIN,TRACK,END),
	current_time(TIME),
	END <= TIME.

required(actualDelay(TRAIN,TRACK) == 0) :-
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	current_schedule_stay(TRAIN,TRACK,STAY),
	current_time(TIME),
	BEGIN+STAY <= TIME.

% if there is the case that the start time of first track of a route
% occurs after the current time, it can be delayed
required(solved_schedule_begin(TRAIN,TRACK) == (BEGIN + actualDelay(TRAIN,TRACK))) :-
	route_first(TRAIN,TRACK),
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	current_time(TIME),
	BEGIN > TIME.

% otherwise, for all other tracks of a route, the begin time is the
% end time minus the overlapping time (1)
required((solved_schedule_begin(TRAIN,TRACK) == solved_schedule_end(TRAIN,PREVIOUSTRACK) - overlappingTime) /\
	(solved_schedule_end(TRAIN,PREVIOUSTRACK) - overlappingTime > TIME)) :-
	current_schedule_begin(TRAIN,TRACK,BEGIN),
	route_next(TRAIN,PREVIOUSTRACK,TRACK),
	current_time(TIME).

% no delay on first route track because there is possible delay at the beginning  
required((solved_schedule_end(TRAIN,TRACK) == (solved_schedule_begin(TRAIN,TRACK) + STAY)) /\
	(solved_schedule_begin(TRAIN,TRACK) + STAY > TIME)) :-
	route_first(TRAIN,TRACK),
	current_schedule_stay(TRAIN,TRACK,STAY),
	current_time(TIME).

% at the end of track, the train can be delayed  
required((solved_schedule_end(TRAIN,TRACK) == (solved_schedule_begin(TRAIN,TRACK) + STAY + actualDelay(TRAIN,TRACK))) /\
	(solved_schedule_begin(TRAIN,TRACK) + STAY > TIME)) :-
	route_next(TRAIN,PREVIOUSTRACK,TRACK),
	current_schedule_stay(TRAIN,TRACK,STAY),
	current_time(TIME).

% special case: end of last track -> no delays
% no delays
required((solved_schedule_end(TRAIN,TRACK) == solved_schedule_begin(TRAIN,TRACK) + STAY) /\
	(solved_schedule_begin(TRAIN,TRACK) + STAY > TIME)) :- 
	route_last(TRAIN,TRACK),
	current_schedule_stay(TRAIN,TRACK,STAY),
	current_time(TIME).

% defines how long a train (normally) occupies a track 
train_trackoccupation(TRAIN,TRACK,OCCUPATION):-
    train_timeontrack(TRAIN,TRACK,DURATION),
    train_stay(TRAIN,STATION,STAY),
    OCCUPATION=DURATION+STAY,    
    station_tracks(STATION,TRACK).

% instead of using default negation in next rule, derive station tracks
track_of_station(TRACK) :- 
	station_tracks(STATION,TRACK).

train_trackoccupation(TRAIN,TRACK,OCCUPATION):-
    train_timeontrack(TRAIN,TRACK,OCCUPATION),
%   not station_tracks(STATION,TRACK) : station_tracks(STATION,TRACK).
    not track_of_station(TRACK).

% derive which tracks are in a route of a train
route_track(TRAIN,TRACK) :- route_next(TRAIN,TRACK,TRACKNEXT).
route_track(TRAIN,TRACK) :- route_last(TRAIN,TRACK).

% two trains cannot be on the same track at the same time
required((solved_schedule_begin(TRAIN2,TRACK) >= solved_schedule_end(TRAIN1,TRACK)) \/
	(solved_schedule_begin(TRAIN1,TRACK) >= solved_schedule_end(TRAIN2,TRACK))) :-
	current_schedule_begin(TRAIN1,TRACK,B1),
	current_schedule_begin(TRAIN2,TRACK,B2),
	train(TRAIN1), train(TRAIN2), 
	TRAIN1 != TRAIN2,
	route_track(TRAIN1,TRACK),
	route_track(TRAIN2,TRACK).