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


Analysed Constructs

Hypertext Constructs Page

On-line Help

Help Contents Page
Index

Document Last Updated: Tue Jul 12 01:45:58 2005

B-Toolkit Release 5.1.12