module student

sig Time {}


abstract sig Student {
        passed : Course -> Time,
        current : Course lone -> Time,
        labs : Lab -> Time,
        exams : Course -> Time,
        isWorking : set Time
}

sig PosgradeStudent  extends Student {
        firstDegree : some Career
}

sig Career {}

sig GradeStudent extends Student{}


sig Course {
        labsC : some Lab
}
sig optional in Course {}


sig Lab {
        type : one TypeLab
}


abstract sig TypeLab {}
one sig Theorical, Practical extends TypeLab{}


-- fact {       labs in Course lone -> Lab }


-- all courses have at least one laboratory 
fact {all c : Course |  #(c.labsC) >=1 }

fact {all c : Course |  c = optional => Practical in c.labsC.type }

fact {all c : Course | some l : Lab  | l in c.labsC && l.type = Theorical }


pred isEnrolled [s : Student, t,t' : Time] {
        #(s.current.t) >= 1
}

pred enroll [s : Student, c : Course, t,t' : Time] {
        #(s.current.t) = 0
        ! (c in s.passed.t)
        
        current.t' = current.t + s -> c
        passed.t' = passed.t
        labs.t' = labs.t
        exams.t' = exams.t
}

pred lab [s : Student, l : Lab, t,t' : Time] {
        #(s.current.t) >= 1
        ! (l in (s.labs.t))
        l in (s.current.t).labsC

        passed.t' = passed.t
        current.t' = current.t
        labs.t' = labs.t + s -> l
        exams.t' = exams.t
}

pred approve [s : Student, t,t' : Time] {
        #(s.current.t) >= 1
        ! (s.current.t in s.exams.t)

        passed.t' = passed.t
        current.t' = current.t
        labs.t' = labs.t
        exams.t' = exams.t + s -> s.current.t
}

pred pass [s : Student, t,t' : Time] {
        #(s.current.t) >= 1
        s.current.t in s.exams.t
        s.current.t.labsC in (s.labs.t)

        exams.t' = exams.t
        labs.t' = labs.t
        passed.t' = passed.t + s -> s.current.t
        current.t' = current.t - s -> Course
}

pred quit [s : Student, t,t' : Time] {
        #(s.current.t) >= 1
        
        exams.t' = exams.t - s -> s.current.t
        labs.t' = labs.t - s -> (s.current.t).labsC
        passed.t' = passed.t
        current.t' = current.t - s -> Course
}

pred fail [s : Student, t,t' : Time] {
        #(s.current.t) >= 1
        
        exams.t' = exams.t - s -> s.current.t
        labs.t' = labs.t - s -> (s.current.t).labsC
        passed.t' = passed.t
        current.t' = current.t - s -> Course
}

--run{}