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


Analysed Constructs

Hypertext Constructs Page

On-line Help

Help Contents Page
Index

Document Last Updated: Tue Jul 12 02:02:48 2005

B-Toolkit Release 5.1.12