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

        GetTrainByNum: Schedule >< TrainNum -> Schedule
        /*пусть будет всюду вычислимой - если что, пустое множество получится*/

        GetTrainByNum(sch, tn) as new
            post (all (w, tn1, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn1, t1, t2, s1, s2) isin new) 
                     => (((w, tn1, t1, t2, s1, s2) isin sch) /\ (tn1 = tn))  
                    )
                 /\ (
                        (((w, tn1, t1, t2, s1, s2) isin sch) /\ (tn1 = tn)) 
                     => ((w, tn1, t1, t2, s1, s2) isin new) 
                    ) 

                 ),


        HasTrain: Schedule >< TrainNum -> Bool
        HasTrain(s,n) is (card GetTrainByNum(s,n) > 0),

        /*-------------------------------------------------------------------*/

        GetTrainByWay: Schedule >< Way -> Schedule
        /*пусть будет всюду вычислимой - если что, пустое множество получится*/

        GetTrainByWay(sch, w) as new
            post (all (w1, tn, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w1, tn, t1, t2, s1, s2) isin new)
                     => (((w1, tn, t1, t2, s1, s2) isin sch) /\ (w1 = w))  
                    )
                 /\ (
                        (((w1, tn, t1, t2, s1, s2) isin sch) /\ (w1 = w))
                     => ((w1, tn, t1, t2, s1, s2) isin new) 
                    ) 

                 ),

        /*-------------------------------------------------------------------*/

        AddTrain: Schedule >< TrainInfo -~-> Schedule
        /*предусловие - путь свободен и такого поезда нет*/

        AddTrain(sch, (w, tn, t1, t2, s1, s2)) as new
            post (all (w1, tn1, t11, t21, s11, s21): TrainInfo :- 
                    (
                        ((w1, tn1, t11, t21, s11, s21) isin new)
                     => (((w1, tn1, t11, t21, s11, s21) isin sch) 
                        \/ (w1 = w) /\ (tn = tn1) /\ (t1 = t11) 
                                    /\ (t2 = t21) /\ (s1 = s11) /\ (s2 = s21))  
                    )
                 /\ (
                        (((w1, tn1, t11, t21, s11, s21) isin sch) 
                        \/ (w1 = w) /\ (tn = tn1) /\ (t1 = t11) 
                                    /\ (t2 = t21) /\ (s1 = s11) /\ (s2 = s21)) 
                     => ((w1, tn1, t11, t21, s11, s21) isin new) 
                    )

                 )
            pre ~HasTrain(sch, tn) /\ WayEmpty(sch, t1, t2, w),

        /*-------------------------------------------------------------------*/

        WayEmpty: Schedule >< Time >< Time >< Way -> Bool
        /*путь свободен*/

        WayEmpty(sch, t1, t2, w) as b
            post b = (all (w1, tn, t11, t22, s1, s2): TrainInfo :-
                (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)))),

        /* мое условие: можешь проверить, правильно ли это :)
           я считаю, что время - это кол-во минут, прошедших после полуночи

            WayEmpty(sch, t1, t2, w) as
                 (all (w1, tn, t11, t22, s1, s2): TrainInfo :-
                (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) as new
            post (all (w, tn1, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn1, t1, t2, s1, s2) isin new)
                     => (((w, tn1, t1, t2, s1, s2) isin sch) 
                        /\ (tn ~= tn1))  
                    )
                 /\ (
                        (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (tn ~= tn1)) 
                     => ((w, tn1, t1, t2, s1, s2) isin new) 
                    )

                 )
            pre HasTrain(sch, tn),

        /*-------------------------------------------------------------------*/

        FilterSour: Schedule >< Station -> Schedule
        /*выборка по первой станции (отправления)*/

        FilterSour(sch, st) as new
            post (all (w, tn, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn, t1, t2, s1, s2) isin new)
                     => (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (st = s1))  
                    )
                 /\ (
                        (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (st = s1)) 
                     => ((w, tn, t1, t2, s1, s2) isin new) 
                    )

                 ),
    
        /*-------------------------------------------------------------------*/

        FilterDest: Schedule >< Station -> Schedule
        /*выборка по второй станции (назначения)*/

        FilterDest(sch, st) as new
            post (all (w, tn, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn, t1, t2, s1, s2) isin new)
                     => (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (st = s2))  
                    )
                 /\ (
                        (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (st = s2)) 
                     => ((w, tn, t1, t2, s1, s2) isin new) 
                    )

                 ),
    
        /*-------------------------------------------------------------------*/

        FilterArr: Schedule >< Time >< Bool -> Schedule
        /*выборка по времени прибытия ("до" либо "после" указанного)*/

        FilterArr(sch, t, after) as new
            post (all (w, tn, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn, t1, t2, s1, s2) isin new)
                     => (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (after /\ (t1 >= t) \/ ~after /\ (t1 <= t)) )  
                    )
                 /\ (
                        (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (after /\ (t1 >= t) \/ ~after /\ (t1 <= t)) )  
                     => ((w, tn, t1, t2, s1, s2) isin new) 
                    )

                 ),
    
        /*-------------------------------------------------------------------*/

        FilterDep: Schedule >< Time >< Bool -> Schedule
        /*выборка по времени отправления ("до" либо "после" указанного)*/

        FilterDep(sch, t, after) as new
            post (all (w, tn, t1, t2, s1, s2): TrainInfo :- 
                    (
                        ((w, tn, t1, t2, s1, s2) isin new)
                     => (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (after /\ (t2 >= t) \/ ~after /\ (t2 <= t)) )  
                    )
                 /\ (
                        (((w, tn, t1, t2, s1, s2) isin sch) 
                        /\ (after /\ (t2 >= t) \/ ~after /\ (t2 <= t)) )  
                     => ((w, tn, t1, t2, s1, s2) isin new) 
                    )

                 )

end