(****
 *
 * Module Schedule defines the objects and operations related to scheduling
 * appointments, meetings, events, and tasks in the calendar system.
 *
 *)

module Schedule;

  from CalendarDB import CalendarDB;
  export Event;

  define operation attribute trigger:Trigger = UserTriggered;
  (*
   * The trigger attribute is used to specify by what means an operation
   * triggered.  See the desciption of the Trigger object for further details.
   *)

  object ScheduledItem
    components: Appointment or Meeting or Task or Event;
    description: (*

    *);
  end ScheduledItem;

  object Event
    components: Title and StartDate and EndDate and RecurringInfo;
    description: (*
        An Event is the most generic type of scheduled item.  The three other
        types of scheduled items -- Appointments, Meetings and Tasks -- are
        specializations of Event.
    *);
  end Event;

  object Appointment extends Event
    components: StartTime and Duration and Location and AppointmentSecurity and
        AppointmentPriority and AppointmentRemindInfo and Details;
    description: (*
        An Apppointment adds a number of components to a generic Event.  Each
        of these components is described further below.
    *);
  end Appointment;

  object Meeting extends Event
    components: StartTime and Duration and Location and MeetingSecurity and
        AppointmentPriority and AppointmentRemindInfo and Attendees and
        Details and Minutes;
    description: (*
	Like an Appointment, a Meeting adds components to a generic Event.  A
        Meeting differs from an Appointment as follows: (1) Security for an
        appointment includes a private option that is not available for
        meetings; see the definition of the two forms of security below.  (2)
        Meetings have Attendees and Minutes components, appointments do not.
        These extra components represent the fact that a meeting is to be
        scheduled for more than one person, whereas an appointment is for a
        single user.  Hence, scheduling a meeting involves checking more than
        one user calendar and finding a common time among all attendees.  See
        the ScheduleMeeting operation below for further details.
    *);
  end Meeting;

  object MeetingRequest
    components: Title and EarliestStartDate and LatestStartDate and
        EarliestEndDate and LatestEndDate and EarliestStartTime and
        LatestStartTime and Durattion and RecurringInfo and Category and
        Location and MeetingSecurity and AppointmentPriority and
        AppointmentRemindInfo and Attendees and Details;
    description: (*
        A meeting request is used to specify a range of possible meeting times
        when requesting a meeting to be scheduled.  A meeting request has
        basically the same fields as a meeting, excpet (1) the start date, end
        date and start time components are broken into two parts each, to allow
        the user to specify a range of dates and times for scheduling purposes;
        (2) the request has no minutes field, since it is not an actual
        meeting to be held, but rather a request for a potential meeting to be
        held.  See the ScheduleMeeting operation for further details on how
        meeting requests are handled.
    *);
  end MeetingRequest;

  object Task extends Event
    components: Location and Security and TaskPriority and TaskRemindInfo and
         CarryOverFlag and CompletedFlag and Details;
    description: (*
        Like an Apppointment, a Task adds a number of components to a generic
        Event.  A task differs from an appointment as follows: (1) Appointments
        have start and end times, tasks do not.  (2) For appointments, the
        priority is either must or optional; for tasks, priority is a positive
        integer indicating the relative priority of a task compared to other
        tasks.  (3) For appointments, reminders can be set to occur at hour or
        minute granularity; for tasks, the smallest graularity of reminder is a
        day.  (4) Tasks have carry over and completed flags, appointments do
        not.
    *);
  end Appointment;

  object AppointmentPriority
    components: Must or Optional;
    description: (*
        An AppointmentPriority indcates whether an appointment is a must or if
        it is optional, and therefore reschedulable.  This information can be
        used to indicate the general importance of an appointment to the user.
        The more specific use of appointment priority is in the ScheduleMeeting
        operation, where the meeting scheduler can elect to consider optional
        appointments as allowable times for a meeting.
    *);
  end AppointmentPriority;

  object TaskPriority = integer
    description: (*
        A TaskPrioity is a positive integer that defines the priority of one
        task relative to others.
    *);
  end TaskPriority;

  axiom forall (tp: TaskPriority) tp >= 0;

  object Title = string
    description: (*

    *);
  end Title;

  object StartDate = Date
    description: (*

    *);
  end StartDate;

  object EndDate = Date
    description: (*

    *);
  end EndDate;

  object StartTime = Time
    description: (*

    *);
  end StartTime;

  object Duration = TimeLength
    description: (*

    *);
  end Duration;

  object RecurringInfo
    components: IsRecurring and Interval and IntervalDetails;
    description: (*

    *);
  end RecurringInfo;

  object IsRecurring = boolean
    description: (*

    *);
  end IsRecurring;

  obj Interval
    components: Weekly or Biweekly or Monthly or Yearly or
        OtherInterval;
    description: (*

    *);
  end Interval;

  object IntervalDetails
    components: WeeklyDetails or MonthlyDetails or YearlyDetails;
    description: (*
        
    *);
  end IntervalDetails;

  object WeeklyDetails
    components: OnSun and OnMon and OnTues and OnWed and OnThu and OnFri and
        OnSat;
    description: (*

    *);
  end WeeklyDetails;

  object MonthlyDetails
    components: MonthlyDayDetails or MonthlyDateDetails;
    description: (*
        
    *);
  end MonthlyDetails;

  object MonthlyDayDetails
    components: FirstWeekDetails and SecondWeekDetails and ThirdWeekDetails and
        FourthWeekDetails and FifthWeekDetails and LastWeekDetails;
    description: (*
        
    *);
  end MonthlyDayDetails;

  object MonthlyDateDetails
    components: Monthly
    description: (*
        
    *);
  end MonthlyDateDetails;

  object OnSun = boolean;
  object OnMon = boolean;
  object OnTue = boolean;
  object OnWed = boolean;
  object OnThu = boolean;
  object OnFri = boolean;
  object OnSat = boolean;

  object Category
    components: string and StdColor;
    description: (*

    *);
  end Category;

  object Location = string
    description: (*

    *);
  end Location;

  object AppointmentSecurity
    components: Public or PublicTitle or Confidential or Private;
    description: (*
        AppointmentSecurity is one of four possible levels, each of which is
        described further below.  The level specifies the degree of visibity a
        scheduled item has to other users.  For an appointment, task, or event,
        "other users" are defined as all users other than the user on whose
        calender the scheduled item appears.  For a meeting, "other users" are
        defined as all users not on the attendee list of the meeting.
    *);
  end Security;

  object Public
    description: (*
        Public security means other users can see the scheduled item and all
        the information about the item.
    *);
  end Public;

  object PublicTitle
    description: (*
        PublicTitle security means other users can see the title of the
        scheduled item but none of the other information about the item.
    *);
  end Public;

  object Confidential
    description: (*
        Confidential security means other users can only see that a user is
        unavailable for the time period of a scheduled item; no other
        information about the scheduled item is visible.  Since confidential
        security applies to a specific time period, it is meaningful only for
        appointments and meetings, not for tasks or events; tasks and events do
        not have specific time components.
    *);
  end;

  object Private
    description: (*
        Private security means other users see no information at all about a
        scheduled item, not even that the item is scheduled.  Note that private
        security hides a scheduled item from the ScheduleMeeting operation,
        q.v., so that a meeting may be scheduled at the same time as a private
        apppointement.  It is up to the user to handle this situation by
        accepting or refusing the scheduled meeting.  Given the nature of
        private security, it does not apply to meetings.  I.e., only
        appointments can have private security.
    *);
  end;

  object RemindInfo
    components: OnScreen or BeepOnly or Email;
    description: (*
        
    *);
  end RemindInfo;

  object Details = string
    description: (*
	
    *);
  end Details;

  operation ScheduleAppointment(
    inputs: CalendarDB, Appointment;
    outputs: cdb':CalendarDB;
    preconditions: ;
    postconditions: ;
    description: (*
	
    *);
  end ScheduleAppointment;

  operation ScheduleTask
    inputs: ;
    outputs: ;
    preconditions: ;
    postconditions: ;
    description: (*
	
    *);
  end ScheduleTask;

  operation ScheduleMeeting
    inputs: ;
    outputs: ;
    preconditions: ;
    postconditions: ;
    description: (*
	
    *);
  end ScheduleMeeting;

  operation ScheduleEvent
    inputs: ;
    outputs: ;
    preconditions: ;
    postconditions: ;
    description: (*
        
    *);
  end ScheduleEvent;

  object Trigger
    components: UserTriggered or SystemTriggered;
    description: (*
        Trigger defines the two types of operation trigger -- user or system.
        In this specification it is assmed that all operations for which NO
        explicit trigger attribute is specified, the end user triggers the
        operation.  The only other form of operation trigger in this
        specification is SystemTriggered, which indicates that an operation
        triggered externally by the underlying operating system, not explicitly
        by the user.

        The purpose of specifying a trigger is make clear how event reminders
        are generated.  Speccifically, event reminders are to be triggered
        whether or not the calendar tool is operational at the time the
        reminder is set to be sent.
    *);
  end Trigger;

  Change(  

  object UserTriggered;
  object SystemTriggered;

end Schedule;