module MainRoomDB;

export all;

object RoomDB is
	components: Room*;
    description: (*
         the collection of all the Rooms
    *); 
end RoomDB;
object Room is 
	components: bn:buildingNum and rn:roomNum and capacity and isSmartRoom and isLab
and loc:Location and ra:RoomAvailability;
    description: (*
         the information for a Room.
    *);
end Room;


object buildingNum is integer
	description: (*
			* This is the Building Number of the room.
	*);
end;

object roomNum is integer
	description: (*
         the room number of the room
    *);
end;

object capacity is integer
	description: (*
         the capacity number of the room
    *);
end;

object isSmartRoom is boolean
	description: (*
         true if the room is a smart room
    *);
end;

object isLab is boolean
	description: (*
        true if the room is a lab
    *);
end;

object numOfComputers is integer
    description: (*
        the number of computers  in the room
    *);
end;


object Location is
	components: xCoord, yCoord;
	description:(*
			this is the coordinate of the room
	*);
end Location;
object xCoord is integer
	description: (*
			This is the x coordinate on the Map
	*);
end;
object yCoord is integer
	description: (*
			This is the y coordinate on the Map
	*);
end;

object RoomAvailability is
	components: RoomTimeSlot*;
	description:(*
			this is the times the room is available
	*);
end RoomAvailability;

object RoomTimeSlot is 
	components: Hour and Day and isAvailable;
	description:(*
			This is the a specific time and day that a room may or may not be available
	*);
end RoomTimeSlot;
object Hour is integer
	description:(*
			this is an hour block of any given day
	*);
end;
object isAvailable is boolean
	description:(*
			true if the room is available
	*);
end;
object Day is 
	components: Sunday or Monday or Tuesday or Wendnesday or Thursday or Friday or
Saturday;
	description:(*
			the days that a room can be available
	*);
end Day;
object Sunday is string
	description:(*
			this a day that a room could be available
	*);
end;
object Monday is string
	description:(*
			this a day that a room could be available
	*);
end Monday;
object Tuesday is string
	description:(*
			this a day that a room could be available
	*);
end;
object Wendnesday is string
	description:(*
			this a day that a room could be available
	*);
end;
object Thursday is string
	description:(*
			this a day that a room could be available
	*);
end;
object Friday is string
	description:(*
			this a day that a room could be available
	*);
end;
object Saturday is string
	description:(*
			this a day that a room could be available
	*);
end;

object CurrentSelection is integer
	description:(*
			this the number of the current room that is selected in the database
	*);
end;

operation SaveRoom is
	inputs: bn:buildingNum, rn:roomNum, cap:capacity, sr:isSmartRoom, lab:isLab,
	NC:numOfComputers, RDB:RoomDB, RM:Room, cs:CurrentSelection;
	outputs: RDB':RoomDB, RM':Room;
    description: (*
        This operation will save either a new room, or new changes to an existing room. 
    *);
	precondition:
	(*
	*
	*All the fields must be filled in
	*There cant already be a room in the database with the same Building Number and Room Number 
	*unless that room is selected in the db
	* 
	*)
	((not (bn = nil)) and (not (rn = nil)) and (not (cap = nil)) and (not (NC = nil)) and cs = nil)
	or 
	((not (bn = nil)) and (not (rn = nil)) and (not (cap = nil)) and (not
	(NC = nil)) and (not (cs= nil)) and
          (exists (RM'' in RDB) ((RM''.bn = bn) and (RM''.rn = rn))));

	postcondition:
	(*
	*
	*There is a new room added to the RoomDB
	*
	*)
	RM' in RDB';
		
end SaveRoom;

operation DeleteRoom is
	inputs: RDB:RoomDB, RM:Room, cs:CurrentSelection;
	outputs: RDB':RoomDB, RM':Room;
    description: (*
        This will delete a room in the room database
    *);
	precondition:
	(*
	*a room must be selected
	*)
	cs != nil;

	postcondition:
	(*
	*
	*The room must be removed from the RoomDB
	*
	*)
        (forall (RDB':RoomDB)
            (RM' in RDB') iff ((not (RM' = RM)) and (RM' in RDB)));


end DeleteRoom;



operation SaveAvailability is
	inputs: RDB:RoomDB, RM:Room, RA:RoomAvailability;
	outputs: RDB':RoomDB, RA':RoomAvailability;
    description: (*
        This will save the  availability of a room
    *);
	precondition:
	(*
	*
	*);


	postcondition:
	(*
	*
	*The RoomAvailability must be saved
	*
	*)
	(exists (RM'' in RDB) ((RM''.ra = RA')));

end SaveAvailability;


operation SaveLocation is
	inputs: LC:Location, RDB:RoomDB, RM:Room;
	outputs: RDB':RoomDB, LC':Location;
    description: (*
        this will save the location of a room
    *);
	precondition:
	(*
	*
	*All fields must be filled in
	*
	*)
	not (LC = nil);

	postcondition:
	(*
	*
	*The Location must be saved
	*
	*)
	(exists (RM'' in RDB) ((LC' = RM.loc)));

end SaveLocation;

end MainRoomDB;