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


Analysed Constructs

Hypertext Constructs Page

On-line Help

Help Contents Page
Index

Document Last Updated: Tue Jul 12 02:08:17 2005

B-Toolkit Release 5.1.12