MACHINE Registeration(DEPARTMENTS) EXTENDS Regulations(DEPARTMENTS) SEES Bool_TYPE SETS RESPONSE = { OK, StudentNotRegistered, StudentAlreadyRegistered, CourseAlreadyExists, MaxUnitsExceeds, CourseAlreadyTaken, CourseDoesntExist, CoursePrqNotSatisfied, CourseAlreadyPassed } OPERATIONS response <-- AddStudent(department, student, on_probation, passed_courses) = PRE department : DEPARTMENTS & student : STUDENTS & on_probation : BOOL & passed_courses <: COURSE_IDS THEN IF student : students THEN response := StudentAlreadyRegistered ELSE RegulationsAddStudent(department, student, on_probation, passed_courses) || response := OK END END; response <-- AddCourse(department, course, group, capacity) = PRE department : DEPARTMENTS & course : COURSE_IDS & group : NAT1 & capacity : NAT1 THEN IF {course |-> group} |-> department : departments_courses THEN response := CourseAlreadyExists ELSE RegulationsAddCourse(department, course, group, capacity) || response := OK END END; response <-- TakeCourse(student, course, group) = PRE course : COURSE_IDS & group : NAT1 & student : STUDENTS & student_max_units(student) + course_units(course) <= student_max_units(student) THEN IF student /: students THEN response := StudentNotRegistered ELSE IF course : student_courses(student) THEN response := CourseAlreadyTaken ELSE IF {course |-> group} : dom(departments_courses) THEN response := CourseDoesntExist ELSE IF course : student_courses(student) THEN response := CourseAlreadyPassed ELSE IF #crs.(crs : course_prerequisites(course) & crs : student_passed_courses(student)) THEN response := CoursePrqNotSatisfied ELSE VAR ii IN ii <-- CheckMaxUnits(student, course) || IF ii = FALSE THEN response := MaxUnitsExceeds ELSE RegulationsTakeCourse(student, course, group) || response := OK END END END END END END END END END