(****
 *
 * Module Publishing defines the objects and operations related to publishing a
 * test to a specific server with user and time constraints.
 *
 *)

module Publishing;

  from TestGrading import Student, ServerAddress, UserName, Password;
  from AdvancedTest import RawTest, ClassName;
  from QuestionBank import Question;
  from TestGrading import User;
  from TestTaking import Server;
  export all;

  object PublishingInfo is
    components: serverInfo:ServerInfo and timeConstraints:TimeConstraints and userConstraints:UserConstraints;
    description: (*
      Publishing info allows a user to send a specific test to a server where
      users can take the test.
    *);
  end PublishingInfo;

  object Time is integer;
  
  object PublishedTest inherits from RawTest
    components: timeConstraints:TimeConstraints and userConstraints:UserConstraints and publishedQuestion:PublishedQuestion*;
    description: (*
      A Published test is a RawTest with the added Time and User
      constraints that were specified at the time of publishing.
    *);
  end PublishedTest;

  object PublishedQuestion inherits from Question
    components: ptsAvailable:PtsAvailable;
    description: (*
      A PublishedQuestion is a regular question from the database with an added point value.
    *);
  end PublishedQuestion;
  
  object ServerInfo is 
    components: testFile:TestFile and serverAddress:ServerAddress and userName:UserName and password:Password;
    description: (*
		The server details allow the user to publish a specific TestFile to a
		ServerAddress with authentication via UserName and Password.
    *);
  end ServerInfo;

  object TimeConstraints is 
    components: startDate:StartDate and endDate:EndDate and startTime:StartTime and endTime:EndTime;
    description: (*
		The TimeConstraints allows the user to specify a StartDate and EndDate
		for a published test along with a StartTime and EndTime.
    *);
  end TimeConstraints;

  object UserConstraints is 
    components: className:ClassName* and classRoster:ClassRoster and testRoster:TestRoster;
    description: (*
		The UserConstraints allows the user to specify a certain TestRoster
		by selecting users from the ClassRoster list.
    *);
  end UserConstraints;

  object TestFile is 
    components: rawTest:RawTest;
    description: (*
      This file is a test on a users computer that will be published.
    *);
  end TestFile;
  
  object PtsAvailable is integer
    description: (*
      Points available is a set integer determining how much the question 
      is worth in relation to the overall test.
    *);
  end PtsAvailable;
  
  object StartDate is Date
    description: (*
      Date at which the published test will become available for users 
      to take.
    *);
  end StartDate;

  object EndDate is Date
    description: (*
      Date at which the published test will no longer be available for 
      users to take.
    *);
  end EndDate;

  object StartTime is Time and AmOrPm
    description: (*
	  Start time is the specific time which the test will be abailable on
	  the entered Start Date.
    *);
  end StartTime;

  object EndTime is Time and AmOrPm
    description: (*
      End time is the specific time which the test will no longer be available 
      on the entered End Date
    *);
  end EndTime;

  object AmOrPm is am:AM or pm:PM
    description: (* Standard suffix used in 12-hour time value. *);
  end AmOrPm;

  object AM
    description: (* The 12-hour time suffix indicating a morning time. *);
  end;

  object PM
    description: (* The 12-hour time suffix indicating an afternoon time. *);
  end;

  object Date is month:MonthName and number:DateNumber and year:Year
    description: (*
        A Date is the basic unit of calendar time keeping, consisting of a month
        numeric date, and year.
    *);
  end Date;

  object MonthName is jan:January or feb:February or mar:March or apr:April or
        may:May or jun:June or jul:July or aug:August or sep:September or
        oct:October or nov:November or dec:December
    description: (* One of the twelve months of the year. *);
  end MonthName;

  object January
    description: (* One of the twelve months of the year. *);
  end;

  object February
    description: (* One of the twelve months of the year. *);
  end;

  object March
    description: (* One of the twelve months of the year. *);
  end;

  object April
    description: (* One of the twelve months of the year. *);
  end;

  object May
    description: (* One of the twelve months of the year. *);
  end;

  object June
    description: (* One of the twelve months of the year. *);
  end;

  object July
    description: (* One of the twelve months of the year. *);
  end;

  object August
    description: (* One of the twelve months of the year. *);
  end;

  object September
    description: (* One of the twelve months of the year. *);
  end;

  object October
    description: (* One of the twelve months of the year. *);
  end;

  object November
    description: (* One of the twelve months of the year. *);
  end;

  object December
    description: (* One of the twelve months of the year. *);
  end;

  object DateNumber is integer
    description: (* The numeric value of the date in a month, between 1 and 31. *);
  end DateNumber;

  object Year is integer
    description: (* The four-digit year number. *);
  end Year;

  object ClassRoster is student:Student*
    description: (* Class roster is the list of students in the specific class. *);
  end ClassRoster;

  object TestRoster is student:Student*
    description: (* Test roster is the list of students that have permissin to take the test. *);
  end TestRoster;

  operation PublishToServer is
    inputs: server:Server and serverInfo:ServerInfo and userConstraints:UserConstraints and timeConstraints:TimeConstraints;
    outputs: publishedTest:PublishedTest;
    precondition: (* 
                     Login to the given server to publish the test. If the user name
                     and password exist on the server's user list, then publish the test
                     with the given properties, otherwise nil.
                  *)
                  exists (user in server.user) (user.userName = serverInfo.userName) and (user.password = serverInfo.password)
                      and
                  (* Make sure the user specifies a test to be published. *)
                  serverInfo.testFile!=nil
                      and
                  (* Make sure the user specifies a userName. *)
                  serverInfo.userName!=nil
                      and
                  (* Make sure the user specifies a password. *)
                  serverInfo.password!=nil
                      and
                  (* Make sure the user specifies a server address. *)
                  serverInfo.serverAddress!=nil;
                  
    postcondition: (* Make sure the published test on the server accurately
                      has the same time constraints as the dialog. *)
                   publishedTest.timeConstraints=timeConstraints
                       and
                   (* Make sure the published test on the server accurately
                      has the same user constraints as the dialog. *)
                   publishedTest.userConstraints=userConstraints;
                   
    description: (*
      The PublishToServer operation will publish a raw test with the specific
      entered PublishingInfo.
    *);
  end PublishToServer;

end Publishing;