MACHINE Regulations(DEPARTMENTS) CONSTANTS max_normal_student_units, max_on_prob_units, course_prerequisites, course_units PROPERTIES max_normal_student_units = 17 & max_on_prob_units = 14 & course_prerequisites : COURSE_IDS --> {COURSE_IDS} & course_units : COURSE_IDS --> NAT1 VARIABLES on_prb_students, student_courses, student_passed_courses INVARIANT on_prb_students <: STUDENTS & student_courses : students --> {COURSE_IDS} & student_passed_courses : students --> {COURSE_IDS} & on_prb_students <: students DEFINITIONS /* Max units of students, there is an exception just for students that are on probation */ student_max_units == %xx.(xx: students | max_normal_student_units ) <+ %xx.(xx: on_prb_students | max_on_prob_units) ; /* Total units of student selected courses */ student_units == %xx.(xx: students | SIGMA(student_courses(xx)). (1=1|course_units(z))) EXTENDS Department(DEPARTMENTS) SEES Bool_TYPE INITIALISATION on_prb_students, student_courses, student_passed_courses := {},{},{} OPERATIONS RegulationsAddStudent(department, student, on_probation, passed_courses) = PRE student : STUDENTS & department : DEPARTMENTS & on_probation : BOOL & passed_courses <: COURSE_IDS & student /: students THEN DepartmentAddStudent(department, student) || student_passed_courses(student) := passed_courses || student_courses(student) := {} || IF on_probation = TRUE THEN on_prb_students := on_prb_students \/ {student} END END; RegulationsAddCourse(department, course, group, capacity) = PRE course : COURSE_IDS & department : DEPARTMENTS & group : NAT1 & capacity : NAT1 & {course |-> group} /: dom(departments_courses) THEN DepartmentAddCourse(department, course, group, capacity) END; RegulationsTakeCourse(student, course, group) = PRE course : COURSE_IDS & group : NAT1 & student : students & student_max_units(student) + course_units(course) <= student_max_units(student) & course /: student_courses(student) & course /: student_passed_courses(student) & !crs.(crs : course_prerequisites(course) => (course : student_passed_courses(student))) THEN DepartmentTakeCourse(course, group) || student_courses(student) := student_courses(student) \/ {course} END; bb <-- CheckMaxUnits(student, course) = PRE student : students & course : COURSE_IDS THEN bb := bool( student_max_units(student) + course_units(course) <= student_max_units(student)) END END