(*The Scheduler module holds the current schedule object which is what has been generated
from the three databases.  It also holds the generateSchedule operation which is how the databases
are combined to create a sechedule*)
(*Written by Garrett Garcia except the NewsPrint operation and NewsPrintSchedule object, which were written by Matt Anderson *)
module Scheduler;

from RoomDB import all;
from CourseDB import all;
from InstructorDB import all;
export all;

object PreviousState is CurrentSchedule;

object Clipboard is
	components: string;
	description: (*
		The clipboard holds a selection of cut or copied text.
	*);
end Clipboard;

object Selection is
	components: start_position:integer and end_position:integer and
	context:string;
	description: (*
		The workspace text selection is the defined as the starting and ending
		character positions in current workspace text context.
	*);
end Selection;

object SelectionContext is
	components: string;
	description: (*
		SelectionContext is the text context in which the user makes a
		selection.
	*);
end SelectionContext;

object Schedule is 
	components: sched:CurrentSchedule and rdb:RoomDB and cdb:CourseDB and idb:InstructorDB;
	description: (*
		The Schdedule object stores all data that is used in the program
	*);
end Schedule;

object CurrentSchedule is 
	components: qual:Quality and v:View and secs:Section*;
	description: (*
		The CurrentSchedule object holds the information for the last generated schedule.  It also
		contains the quality rating and information and how the schedule is to be shown on screen.
	*);
end CurrentSchedule;

object Quality is 
	components: iQual:InstructorQuality* and NumberOfTBAs and NumerOfSTAFFs;
	description: (*
		The quality of the schedule is determined by the average of all of the individual instructor 
		Qualities combined with the number of TBA's in the schedule and the number of STAFF teachers
		in the schedule.
	*);
end Quality;

object InstructorQuality is integer
	description: (*
		This object is the rating (0-100) of the quality of that instructor's schedule.  The quality
		is determined by How many classes he got that he put in his preferences, how many of the times
		he got that he put in his preferences, the distance between classes that are scheduled right 
		after each other, and what percentage of his WTU's were used.
	*);
end InstructorQuality;

object NumberOfStaffs is integer
	description: (*
		Holds the number of STAFF teachers in the currentSchedule
	*);
end NumberOfStaffs;

object NumberOfTBAs is integer
	description: (*
		Holds the number of TBA times or rooms in the currentSchedule
	*);
end NumberOfSTBAs;

object View is 
	components: np: NewsPrintSchedule, br:byRoom or bi:byInstructor or bc:byCourse;
	description: (*
		Contains information about how the schedule should be shown on screen.
	*);
end View;

(*object NewsPrintSchedule was done by Matt*)
object NewsPrintSchedule is 
	description: (*
		This is the is the schedule saved in the newsprint format
	*);

end NewsPrintSchedule;

object byRoom
	description: (*
		Indicates that the data is being displayed sorted by Rooms
	*);
end byRoom;

object byInstructor 
	description: (*
		Indicates that the data is being displayed sorted by Instructor
	*);
end byRoom;

object byCourse
	description: (*
		Indicates that the data is being displayed sorted by Course
	*);
end byCourse;

object Section is 
	components: days:Day* and st:StartTime and l:Length and sn:SectionNumber 
		and schedCourse:Course and schedRoom:Room and schedInstructor:Instructor and locked:locked;
	description: (*
		Each section holds a class section that is being taught, Including which days it is taught
		the start time of the class to the minute, the length of the class to the minute and the section 
		number.
	*);
end Section; 
		
object Day is 
	components: sun:Sunday or mon:Monday or tues:Tuesday or wed:Wednesday or thurs:Thursday or fri:Friday or sat:Saturday;
	description: (*
		Holds the days of the week.
	*);
end;

object Sunday
	description: (* One of the seven days of the week. *);
end;

object Monday
    description: (* One of the seven days of the week. *);
end;

object Tuesday
    description: (* One of the seven days of the week. *);
end;

object Wednesday
    description: (* One of the seven days of the week. *);
end;

object Thursday
    description: (* One of the seven days of the week. *);
end;

object Friday
    description: (* One of the seven days of the week. *);
end;

object Saturday
    description: (* One of the seven days of the week. *);
end;

object StartTime is integer
	description: (*
		Contains the start time in military time format (Ex. 3:10 PM would be 1510)
	*);
end StartTime;

object Length is integer
	description: (*
		Stores the length of one class period in minutes.
	*);
end Length;

object SectionNumber is integer
	description: (*
		Stores the section number of the course.
	*);
end SectionNumber;

object locked is boolean
	description: (*
		This object tells whether or not the Section is locked.  When a section
		is locked, it can't be changed during rescheduling. *);
end locked;

(* operation NewsPrint was done by Matt*)
operation NewsPrint is
	inputs: cs:CurrentSchedule;
	outputs: ns:NewsPrintSchedule;
    description: (*
        This takes the current schedule and puts in the  common catalog form
    *);
	precondition:
	(*
	*
	* a schedule must have been created
	* 
	*)

	cs != nil;

	postcondition:
	(*
	*
	*a newsprint schedule must have been created
	*
	*)
	
	ns != nil;
		
end NewsPrint;

operation GenerateSchedule is
	inputs: rdb:RoomDB, cdb:CourseDB, idb:InstructorDB, sched:currentSchedule;
	outputs: sched':currentSchedule;
	description: (*
		Compiles all of the information in the three databases and outputs a schedule.
	*);
	precondition: 
		(* The three databases and the workspace are not nil. *)
		(rdb != nil) and
		(cdb != nil) and
		(idb != nil);
		
	postcondition: 
		(* All sections are scheduled that should be. *)
		SectionsNeeded(cdb) = SectionCount(sched'.secs) and 
		
		(* No teacher teaches at two places at the same time *)
		TeachersNotDoubleBooked(sched') and 
		
		(* No room can have two classes in it at the same time *)
		RoomsNotDoubleBooked(sched');
		
		(* All constraints in CourseDB.constraints must be followed *)
end GenerateSchedule;

(* Auxiliary helper functions *)

function SectionCount(secs:Section*)->integer = 
	#secs;

function SectionsNeeded(cdb:Course*)->integer = 
	(* Counts all of the sections that need to be scheduled*)
	if (#cdb = 0) then 0
	else
		cdb[1].sections + SectionsNeeded(cdb[2:#cdb]);

function TeachersNotDoubleBooked(sched:CurrentSchedule)->boolean =
	(* If no teacher is teaching two courses at the same time
		returns true otherwise returns false *)

	forall (schedInstructor in [1 .. #sched.secs])
		if (sched.secs[schedInstructor].st >= (sched.secs[schedInstructor+1].st)) and 
			(sched.secs[schedInstructor].st < (sched.secs[schedInstructor+1].st + sched.secs[schedInstructor+1].l))
			then false;

function RoomsNotDoubleBooked(sched:CurrentSchedule)->boolean = 
	(* Returns true if no room has two sections scheduled in it
		at the same time. *)

	forall (schedCourse in [1 .. #sched.secs])
		if (sched.secs[schedCourse].st >= (sched.secs[schedCourse+1].st)) and 
			(sched.secs[schedCourse].st < (sched.secs[schedCourse+1].st + sched.secs[schedCourse+1].l)) and
			(sched.secs[schedCourse].schedRoom = sched.secs[schedCourse+1].schedRoom)
			then false;
		
end Scheduler;