scheme
    RAILROAD_STATION_ABSTRACT =
class
    type
        Way = Nat,
        Time = Nat,
        Station,
        TrainNum = Nat,
        TrainInfo = Way >< TrainNum >< Time >< Time >< Station >< Station,
        Schedule = TrainInfo-set
        /*-------------------------------------------------------------------*/
    value

        Empty: Schedule,
        GetTrainByNum: Schedule >< TrainNum -> Schedule,
        HasTrain: Schedule >< TrainNum -> Bool,
        GetTrainByWay: Schedule >< Way -> Schedule, 
        AddTrain: Schedule >< TrainInfo -~-> Schedule,
        DelTrain: Schedule >< TrainNum -~-> Schedule,
        FilterSour: Schedule >< Station -> Schedule,
        FilterDest: Schedule >< Station -> Schedule,
        FilterArr: Schedule >< Time >< Time -> Schedule,
        FilterDep: Schedule >< Time >< Time -> Schedule

    axiom
        
        /*GetTrainByNum*/
        all tn: TrainNum 
            :- GetTrainByNum(Empty, tn) is Empty,
        all tn, tn1: TrainNum, sch: Schedule, w: Way, t1, t2: Time, s1, s2: Station
            :- GetTrainByNum(AddTrain(sch, (w, tn, t1, t2, s1, s2)), tn) is 
                if tn = tn1 then {(w, tn1, t1, t2, s1, s2)}
                            else GetTrainByNum(sch, tn)
                end,

        /*HasTrain*/
        all tn: TrainNum, sch: Schedule
            :- HasTrain(sch, tn) is GetTrainByNum(sch, tn) ~= Empty,

        /*GetTrainByWay*/
        all w: Way
            :- GetTrainByWay(Empty, w) is Empty,
        all tn: TrainNum, sch: Schedule, w, w1: Way, t1, t2: Time, s1, s2: Station
            :- GetTrainByWay(AddTrain(sch, (w1, tn, t1, t2, s1, s2)), w) is 
                if w = w1 then GetTrainByWay(sch, w) union {(w1, tn, t1, t2, s1, s2)}
                          else GetTrainByWay(sch, w)
                end,

        /*AddTrain*/
        all ti: TrainInfo
            :- AddTrain(Empty, ti) is {ti},
        all sch: Schedule, w, w1: Way, tn, tn1: TrainNum, t1, t2, t11, t22: Time, s1, s2, s11, s21: Station
            :- AddTrain(sch union {(w1, tn1, t11, t22, s11, s21)}, (w, tn, t1, t2, s1, s2)) is 
                if tn1 ~= tn /\ (w1 ~= w 
                                \/ (((t22 >= t11) /\ (t2 >= t1) /\ ((t2 < t11) \/ (t1 > t22)))
                                    \/ ((t22 < t11) /\ (t2 > t1) /\ (t2 < t11) /\ (t1 > t22))
                                    \/ ((t22 >= t11) /\ (t2 < t1) /\ (t2 < t11) /\ (t1 > t22)))
                                ) 
                   then AddTrain(sch, (w, tn, t1, t2, s1, s2)) union {(w1, tn1, t11, t22, s11, s21)}
                   else sch union {(w1, tn1, t11, t22, s11, s21)}
                end,

        /*DelTrain*/
        all sch: Schedule, tn: TrainNum
            :- DelTrain(sch, tn) is sch \ GetTrainByNum(sch, tn),

        /*FilterSour*/
        all st: Station
            :- FilterSour(Empty, st) is Empty,
        all sch: Schedule, st, s1, s2: Station, t1, t2: Time, tn: TrainNum, w: Way
            :- FilterSour(sch union {(w, tn, t1, t2, s1, s2)}, st) is 
                if s1 = st then FilterSour(sch, st) union {(w, tn, t1, t2, s1, s2)}
                           else FilterSour(sch, st)
                end,

        /*FilterDest*/
        all st: Station
            :- FilterDest(Empty, st) is Empty,
        all sch: Schedule, st, s1, s2: Station, t1, t2: Time, tn: TrainNum, w: Way
            :- FilterSour(sch union {(w, tn, t1, t2, s1, s2)}, st) is 
                if s2 = st then FilterSour(sch, st) union {(w, tn, t1, t2, s1, s2)}
                           else FilterSour(sch, st)
                end,

        /*FilterArr*/
        all tz1, tz2: Time
            :- FilterArr(Empty, tz1, tz2) is Empty,
        all sch: Schedule, s1, s2: Station, t1, t2, tz1, tz2: Time, tn: TrainNum, w: Way
            :- FilterArr(sch union {(w, tn, t1, t2, s1, s2)}, tz1, tz2) is 
                if (((tz1 <= tz2) /\ (tz1 <= t1) /\ (tz2 >= t1)) 
                    \/ ( (tz1 > tz2) /\ ((tz1 <= t1) \/ (tz2 >= t1))))
                  then FilterArr(sch, tz1, tz2) union {(w, tn, t1, t2, s1, s2)}
                  else FilterArr(sch, tz1, tz2)
                end,                           

        /*FilterDep*/
        all tz1, tz2: Time
            :- FilterDep(Empty, tz1, tz2) is Empty,
        all sch: Schedule, s1, s2: Station, t1, t2, tz1, tz2: Time, tn: TrainNum, w: Way
            :- FilterArr(sch union {(w, tn, t1, t2, s1, s2)}, tz1, tz2) is 
                if (((tz1 <= tz2) /\ (tz1 <= t2) /\ (tz2 >= t2)) 
                    \/ ( (tz1 > tz2) /\ ((tz1 <= t2) \/ (tz2 >= t2))))
                  then FilterArr(sch, tz1, tz2) union {(w, tn, t1, t2, s1, s2)}
                  else FilterArr(sch, tz1, tz2)
                end

end