scheme
    RAILROAD_STATION_NEW =           
class
    type
        Way = Nat,
        Time = Nat,
        Station,
        TrainNum = Nat,
        TrainInfo = Way >< TrainNum >< Time >< Time >< Station >< Station,
        Schedule = TrainInfo-set
        /*-------------------------------------------------------------------*/
    value
	  HasTrain: Schedule >< TrainNum -> Bool
        HasTrain(sch, tn) is (exists (w1, tn1, t1, t2, s1, s2): TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ tn1 = tn),

        GetTrainByNum: Schedule >< TrainNum -> TrainInfo-set
        GetTrainByNum(sch, tn) is {(w1, tn1, t1, t2, s1, s2)|(w1, tn1, t1, t2, s1, s2): TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ tn1 = tn},

        GetTrainByWay: Schedule >< Way -> TrainInfo-set
        GetTrainByWay(sch, w) is {(w1, tn1, t1, t2, s1, s2)|(w1, tn1, t1, t2, s1, s2): TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ w1 = w},
           
        AddTrain: Schedule >< TrainInfo -~-> Schedule
        AddTrain(sch, (w, tn, t1, t2, s1, s2)) is (sch union {(w, tn, t1, t2, s1, s2)})
            pre ~HasTrain(sch, tn) /\ WayEmpty(sch, t1, t2, w),

        WayEmpty: Schedule >< Time >< Time >< Way -> Bool
        WayEmpty(sch, t1, t2, w) is (all (w1, tn1, t11, t22, s1, s2): TrainInfo :- (w1, tn1, t11, t22, s1, s2) isin sch /\ w = w1 => 
					 ( ((t22 >= t11) /\ (t2 >= t1) /\ ((t2 < t11) \/ (t1 > t22)))
                            \/ ((t22 < t11) /\ (t2 > t1) /\ (t2 < t11) /\ (t1 > t22))
                            \/ ((t22 >= t11) /\ (t2 < t1) /\ (t2 < t11) /\ (t1 > t22)) )  ),

        DelTrain: Schedule >< TrainNum -~-> Schedule
        DelTrain(sch, tn) is (sch \ {(w1, tn1, t1, t2, s1, s2)|(w1, tn1, t1, t2, s1, s2):TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ tn1 = tn})
			pre HasTrain(sch, tn), 

        FilterSour: Schedule >< Station -> Schedule
        FilterSour(sch, st) is {(w1, tn1, t1, t2, s1, s2)|(w1, tn1, t1, t2, s1, s2): TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ st = s1},

        FilterDest: Schedule >< Station -> Schedule
        FilterDest(sch, st) is {(w1, tn1, t1, t2, s1, s2)|(w1, tn1, t1, t2, s1, s2): TrainInfo :- (w1, tn1, t1, t2, s1, s2) isin sch /\ st = s2},

        FilterArr: Schedule >< Time >< Time -> Schedule
        FilterArr(sch, t1, t2) is {(w, tn, t11, t22, s1, s2)|(w, tn, t11, t22, s1, s2): TrainInfo :- (w, tn, t11, t22, s1, s2) isin sch /\ 
					(((t1 <= t2) /\ (t1 <= t11) /\ (t2 >= t11)) 
					\/ ( (t1 > t2) /\ ((t1 <= t11) \/ (t2 >= t11))))},

        FilterDep: Schedule >< Time >< Time -> Schedule
        FilterDep(sch, t1, t2) is {(w, tn, t11, t22, s1, s2)|(w, tn, t11, t22, s1, s2): TrainInfo :- (w, tn, t11, t22, s1, s2) isin sch /\ 
					(((t1 <= t2) /\ (t1 <= t22) /\ (t2 >= t22)) 
					\/ ( (t1 > t2) /\ ((t1 <= t22) \/ (t2 >= t22))))}

end