(****
 *
 * Module TestTaking defines the objects and operations that can be
 * performed by an end user - either a proctor or a test taker.
 *
 *
 *)

module TestTaking;

from QuestionBank import all;
from Question import all;
from TestGrading import all;
from Publishing import all;
from AdvancedTest import Duration, TestTitle, RawTest;
export all;

object Server is serverAddress:ServerAddress and publishedTest:PublishedTest* and user:User*
   description: 
   (*
      A server from our point of view is just a repository of tests.
   *);
end Server;

object TestRequest is
   components: testName:TestName and userName:UserName and password:Password;
   description: 
   (*
       A TestRequest represents an attempt to get a particular test from
       the server to take.
   *);
end TestRequest;

object TestName is string
   description: (* The name of the test, given at creation time. *);
end TestName;

object TakenTest inherits from PublishedTest is
   components: asnweredQuestion:AnsweredQuestion* and userName:UserName and time:Time;
   description: (*
      A TakenTest is a test that has been completed.  The test
      can be of any type - standard, timed, etc.
   *);
end TakenTest;

object AnsweredQuestion inherits from Question is
   components: studentResponse:StudentResponse;
   description: (*
      A SubmittedQuestion is a a question combined with the response of the taker.
   *);
end AnsweredQuestion;

object StudentResponse is tfResponse:TFResponse or mcResponse:MCResponse or matchResponse:MatchResponse or fibResponse:FIBResponse or essayResponse:EssayResponse or ecResponse:ECResponse or numericalResponse:NumericalResponse
   description: (*
      Determined by value of questions type - the student's answer
   *);
end;

object TFResponse is isTrue:IsTrue
   description: (*
      IsTrue is imported from Question module.  Flags if the user chose true or false.
   *);
end TFResponse;

object NumericalResponse is real
   description: (*
      The student's answer in decimal form.
   *);
end NumericalResponse;

object MCResponse is 
   components: numSelected:NumSelected and selectedMCResponse:SelectedMCResponse*;
   description: (*
      Store the number of answers that the student selected, and the individual answers.
   *);
end MCResponse;

object NumSelected is integer
   description: (*
      The number of selected responses in a multiple choice answered question.
   *);
end NumSelected;

object SelectedMCResponse is string
   description: (*
      The text of the multiple choice option that was selected.
   *);
end SelectedMCResponse;

object MatchResponse is matches:Matches*
   description: (*
      The Subject and Definition - defined in Question module - that describes the selected matches.
   *);
end MatchResponse;

object FIBResponse is word:Word*
   description: (*
      An ordered list of words that should be used to fill in the blanks of this question.
   *);
end FIBResponse;

object Word is string;

object EssayResponse is studentEssay:StudentEssay
   description: (*
      The complete text as entered by the user.
   *);
end EssayResponse;

object StudentEssay is string;

object ECResponse is codeSegment:CodeSegment
   description: (*
      The complete code segment, including any "starter" code.
   *);
end ECResponse;

object CodeSegment is string; 

operation AnswerQuestion is
   inputs: sr:StudentResponse, q:Question, p:PublishedTest;
   outputs: p':PublishedTest;
   precondition: 
      (* The Question is on the current test *)
      q in p.question
         and 

      (* The Question and Answer are of the same type *)
      sr?tfResponse iff q.questionType?trueOrFalse
         and
      sr?mcResponse iff q.questionType?multipleChoice
         and
      sr?matchResponse iff q.questionType?matching
         and
      sr?fibResponse iff q.questionType?fillInTheBlanks
         and
      sr?essayResponse iff q.questionType?essay
         and
      sr?ecResponse iff q.questionType?embeddedCode
         and
      sr?numericalResponse iff q.questionType?numerical
         and

      (* Preconditions for each specific type *)
      if (sr?mcResponse) then
         (sr.mcResponse.numSelected <= q.questionAnswer.multipleChoiceAnswer.numResponses)   
      and
      if (sr?matchResponse) then
         (#(sr.matchResponse.matches) <= q.questionAnswer.matchingAnswer.numMatches)
      and
      if (sr?fibResponse) then
         (#(sr.fibResponse.word) <= #(q.questionAnswer.fillInTheBlanksAnswer.fillInTheBlanksProcessed.blank));
      
   postcondition: 
      (* q is now on the test in a derived form, and is associated with the response. *)
      exists (q':AnsweredQuestion) ((q' in p'.question) and
         (q' ~= q.<AnsweredQuestion except (q'.studentResponse = sr)));

   description: (*
      AnswerQuestion marks a given answer as the students response to a
      particular question or changes their previous answer.
   *);
end AnswerQuestion;

operation SubmitTest is
   inputs: un:UserName, time:Time, p:PublishedTest;
   outputs: t':TakenTest;
   precondition:
      (* Some person has completed this test *)
      un != nil
         and
    
      (* The time has not yet expried if this is a timed test *)
      time <= p.duration;

   postcondition: 
      (* The test is the same tes with the derived properties added *)
      t' ~= p.<TakenTest except (t'.userName = un) and (t'.time = time)
         and

      (* All the questions are of type AnsweredQuestion but otherwise
         equivalent to their origianl PublishedQuestion forms *)
      forall (q':Question)
         ((q' in t'.question) iff (q' in p.question)
            and
         q'?<AnsweredQuestion);

   description: (*
      When a student completes a test, he submits it for grading.  This results
      in a Test object that is aware of the Answers that exist for the questions.
      The test is also aware of which questions were not answered.
   *);
end SubmitTest;

operation GetTest is
   inputs: tr:TestRequest, s:Server, date:Date, time:Time;
   outputs: pt:PublishedTest;
   precondition: 
       (* All fields are required *)
       tr.userName != nil
          and
       tr.password != nil
          and
       tr.testName != nil
          and

       (* The test exists on the server *)
       exists (p in s.publishedTest)
          ((p.testtitle = tr.testName)
             and
          UserHasAccess(tr.userName, p, date, time));
   postcondition: 
       (* This test is one of the tests from the server, and is the
          one that was requested *)
       pt in s.publishedTest
          and
       pt.testtitle = tr.testName;
   description: (*
      The GetTest operation will fetch an existing test from the server for the
      user to take.
   *);
end GetTest;

operation ViewGrade is
   inputs: tr:TestRequest, s:Server;
   outputs: g:GradedTest;
   precondition: 
       (* All fields are required *)
       tr.userName != nil
          and
       tr.password != nil
          and
       tr.testName != nil
          and

       (* The test exists on the server *)
       exists (p in s.publishedTest)
          ((p.testtitle = tr.testName and p?<GradedTest)
             and
          UserHasAccess(tr.userName, p, nil, nil));
   postcondition: 
       g in s.publishedTest
          and
       g.testtitle = tr.testName;
   description: (*
      The ViewGrade operation gets a previosulyt graded test from the server an
      allows the user to view it.
   *);
end ViewGrade;

operation ForceSubmit is
   inputs: un:UserName, pt:PublishedTest;
   outputs: t:TakenTest;
   precondition:
       (* Some person has taken this test *) 
       un != nil;
   postcondition: 
       (* The test user name and time have been updated *)
       t.userName = un and t.time =  pt.duration
          and
          
       forall (q':Question)
         ((q' in t.question) iff (q' in pt.question)
            and
         q'?<AnsweredQuestion);
   description: (*
      When a user runs out of time, his test is automatically submitted to the
      server.
   *);
end ForceSubmit;

function UserHasAccess(un:UserName, pt:PublishedTest, date:Date, time:Time) ->
   boolean = (
      exists (s in pt.userConstraints.classRoster.student)
         (un = s)
         and
      InRange(pt.timeConstraints, date, time)
);

(* The modeling of time and dates is too excessive to accurately model
   the in range function.  To sum up, it should return true if the
   given date and time fall between the start and end date and time
   in the TimeConstraints object. *)
function InRange(tn:TimeConstraints, date:Date, time:Time) ->
   boolean = (
      1 = 1
);
end TestTaking;