(*
 * This example illustrates the formal specification for a basic scheduling
 * operation.  The primary output requirement for the operation is that it
 * schedules an event at the earliest available time in a range of possible
 * times.  Availability is defined by a booked-event list associated with the
 * rooms in which events can be scheduled.  The fact that an event is scheduled
 * at a selected time is defined as follows: (1) the start time of the event is
 * set to the selected time; (2) the event is included in a scheduled events
 * database; and (3) the room of the event is booked for the selected time.
 *
 * For simplicity, the time of an event is specified by a single integer start
 * time.  We will assume that all events have a fixed duration, say one hour,
 * and that start times are specified at one-hour intervals.  The reader is
 * invited to extend the specification to allow events to have an arbitrary
 * start time and duration.
 *)

obj Event =  time:Time and rm:Room and info:EventInfo;
    (* An event has a start time, room, and other info we dont care about
     * here. *)

obj EventDB =  Event*;
    (* An event DB is a list of events. *)
  
obj Room =  name:Name and booked:Time* and RoomInfo;
    (* A room has a name, booked time list, and other info we dont care about
     * here. *)

obj Time =  integer;
    (* A time is a single integer, assumed to represent an hourly start time
     * for meetings with a fixed one-hour duration. *)

obj Name =  string;
obj EventInfo;		(* We don't care about this here. *)
obj RoomInfo;		(* Ditto. *)


(*
 * The schedule operation is defined per the requirements discussed above.  The
 * given start/end times specify the earliest and latest possible times at
 * which the event can be scheduled.
 *)
op Schedule(edb:EventDB, starttime:Time, endtime:Time,
	info:EventInfo, room:Room)-> (edb':EventDB, room':Room)

    pre:    
	(*
	 * There is at least one time that is between the given start time and
         * end time at which the room is available.
	 *)
	exists (time:Time) (
	    InRange(time, starttime, endtime)
		and
	    RoomAvailable(room, time)
	);

    post:    
	(*
	 * An event is properly added to the output db at the "best" time,
	 * where "best" means the earliest possible time between the given
	 * start time and end time at which the given room is available.
	 *
	 * Also, the room in which the event is scheduled is booked for the
	 * event's time.
	 *)

	(* The event is properly added to the event db. *)
	forall (e:Event)
	    (e in edb') iff ((e in edb)	  (* Standard anti-spurious rqmnt *)
		    or 
		ScheduledAtBestTime(e, starttime, endtime, room))

	    and

	(* The event's room is booked for the event's time. *)
	not RoomAvailable(room', e.time)

	    and

	(* The event info is that given in the input. *)
	(e.info = info);
	
end Schedule;


(*
 * A given event is scheduled at the best time.
 *)
function ScheduledAtBestTime(e:Event,
	starttime:Time, endtime:Time, room:Room)-> boolean = (

    (*
     * The scheduled time is between the given start time and end time.
     *)
    InRange(e.time, starttime, endtime)

	and

    (*
     * The room is available at the scheduled time.
     *)
    RoomAvailable(room, e.time)

	and

    (*
     * The scheduled time is the earliest possible.
     *)
    IsEarliest(e.time, starttime, endtime, room)

);


(*
 * For a given time, no other in-range, non-booked time is earlier.
 *)
function IsEarliest(time:Time, starttime:Time, endtime:Time, room:Room)->
	boolean = (

    not (
	exists (time':Time) (
	    InRange(time', starttime, endtime)
		and
	    RoomAvailable(room, time')
		and
	    (time' < time)
	)
    )
);


(*
 * Alternative version of IsEarliest.  This version constructs a list of
 * possible times for a given room.
 *)
function IsEarliestAlt(time:Time, starttime:Time, endtime:Time, room:Room)->
	boolean = (

    not (
	exists (time' in  PossibleTimes(starttime, endtime, room)) (
	    (time' < time)
	)
    )
);


(*
 * A given time is between a given start time and end time.
 *)
function InRange(time:Time, starttime:Time, endtime:Time)->boolean =
    (time >= starttime) and (time <= endtime);


(*
 * A given room is available at a given time.  Since the room object contains a
 * list of UNavailable times, the logic is negative.  I.e., a room is available
 * at time t means there is no time on the booked list equal to t.
 *)
function RoomAvailable(room:Room, time:Time) -> boolean =
    not (exists (bookedtime in room.booked) time = bookedtime);


(*
 * Construct a list of possible event times for a given room, where possible
 * means the time is non-booked for the room and in the given start/end time
 * range.
 *)
function PossibleTimes(starttime:Time, endtime:Time, room:Room)->Time* = (
    if (starttime > endtime)
    then []
    else 
	if RoomAvailable(room, starttime)
	then starttime + PossibleTimes(starttime+1, endtime, room)
	else PossibleTimes(starttime+1, endtime, room)
);

obj TimeList =  Time*;