MACHINE Department(DEPARTMENTS) SETS STUDENTS; COURSE_IDS VARIABLES students_departments, departments_courses, course_capacity INVARIANT students_departments : STUDENTS +-> DEPARTMENTS & departments_courses : ( COURSE_IDS <-> NAT1 ) +-> DEPARTMENTS & course_capacity : (COURSE_IDS <-> NAT1 ) +-> NAT & dom(departments_courses) = dom(course_capacity) DEFINITIONS students == dom(students_departments) INITIALISATION students_departments, departments_courses, course_capacity := {},{},{} OPERATIONS DepartmentAddStudent(department, new_student) = PRE new_student : STUDENTS & department : DEPARTMENTS & new_student /: students THEN students_departments := students_departments \/ {new_student |-> department} END; DepartmentAddCourse(department, new_course, new_group, capacity) = PRE new_course : COURSE_IDS & new_group : NAT1 & department : DEPARTMENTS & capacity : NAT1 & {new_course |-> new_group} /: dom(departments_courses) THEN departments_courses := departments_courses \/ {{new_course |-> new_group} |-> department} || course_capacity := course_capacity \/ {{new_course |-> new_group} |-> capacity} END; DepartmentTakeCourse(course, group) = PRE course : COURSE_IDS & group : NAT1 & /* if course exists */ {course |-> group} : dom(departments_courses) & /* if course is not filled */ course_capacity({course |-> group}) > 1 THEN /* decrement course capacity */ course_capacity := course_capacity <+ {{course |-> group} |-> (course_capacity({course |-> group}) - 1)} END END