module Test;
   from Question import all;
   from QuestionBank import Bank, ValidUsers;

   export GeneratedTest;
 
   object DateTime;

   object GeneratedTest is
      description: (*
         The GeneratedTest object is a collection of questions that have not 
         yet been published as a test. It is this object that is produced as
         output of the test generation wizard.
      *);

      components: questions:ID*;

   end GeneratedTest;

   obj ProctoredEnv is
      description: (* Administrative options for proctored environments.  *);

      components:
      (* The user name/ID of the proctor administering the test *)
      proctor:User and 
            
      (* The number of minutes students receive to complete the test *)
      timeLimit:integer and

      (* A boolean flag determining whether students may access other
         applications while taking this test. *)
      isLimitedAccess:boolean;
   end ProctoredEnv;

   obj TakeHomeEnv is
      description: (* Administrative options for take-home environments. *);
      components:
         (* The time and date when the test is due *) 
         dueDate:Date and

         (* Instructions for the test-taker. *)
         studentInstructions:string and

         assigned:Roster;
   end TakeHomeEnv;

   obj PracticeEnv is
      description: (* Administrative options for practice environments. *);
      components: assigned:Roster;
   end PracticeEnv;

   obj AdminEnv is
      description: (*
         AdminEnv defines the administrative environment in which the test will
         be taken. The possible environments are proctored, take-home, and
         practice; each is described by different set of components.
      *);

      components: 
         studentInstr:string and 
         env:(proc:ProctoredEnv or home:TakeHomeEnv or pract:PracticeEnv);
   end AdminOpts;

   operation ManualAdd is
      inputs: t:GeneratedTest and adds:ID*;
      outputs: t':GeneratedTest;

      description: (* Add questions to the given test. 
      *);

      precondition:
         (* The questions being added are not already on the test. *)
         (forall (addid in adds) 
            (not (exists (qid in t.questions) addid = qid)));

      postcondition:
         (* The new test is the old questions plus those added. *)
         (forall (id:ID)
            id in t'.questions iff ((id in adds) or (id in t.questions))) and

         (* The ordering of questions on the new test is the old questions
            followed by the added questions. *)
         forall (ndx:integer | ndx > 0 and ndx <= #t)
            t[ndx] = t'[ndx];

   end ManualAdd;

   operation Remove is
      inputs: t:GeneratedTest and removals:ID*;
      outputs: t':GeneratedTest;

      description: (* 
         Removes the given questions from the test.
      *);

      precondition: (*
         The given questions are on the test.
      *)
      (forall (id in removals)
         (exists (qid in t.questions) id = qid));

      postcondition: (*
         The set of questions on the test is the intersection of its
         initial contents with the complement of the removed questions.
      *)
      forall (id:ID)
            (id in t'.questions iff 
             (not (id in removals) and (id in t.questions)));

   end Remove;

   object LessThan is
   end LessThan;

   object GreaterThan is
   end GreaterThan;

   object Equals is
   end Equals;

   object Relation is
      description: (*
         Defines a relationship between two entities, such as question 
         difficulties or last usages in AdditionCriteria.
      *);
      
      components: lt:LessThan or gt:GreaterThan or eql:Equals;
   end Relation;

   object AdditionCriteria is
      description: (*
         User criteria regarding attributes of questions to add to a test.
      *);

      components: ansType:AnswerArea and
         keywords:string* and
         diffRel:Relation and
         diff:integer and
         durRel:Relation and
         dur:TimeToComplete and 
         useRel:Relation and
         use:Date;
   end AdditionCriteria;

   (* True if question q contains an answer area of format f *)
   function FormatMatch(f:AnswerArea, q:FullQuestion)->boolean = (
      (* "Any" format encoded as nil *)
      f = nil or

      exists (qb in q.questionBody)
         qb?answerArea and (
            qb.answerArea?tfaa and f?tfaa or
            qb.answerArea?mcaa and f?mcaa or
            qb.answerArea?maa and f?maa or
            qb.answerArea?saa and f?saa or
            qb.answerArea?eaa and f?eaa
         );
   );

   (* True if question q meets the addition criteria crit. *)
   function MeetsCriteria(q:FullQuestion, crit:AdditionCriteria)->boolean = (
      FormatMatch(crit.ansType, q) and

      (* Matches at least one keyword *) 
      ((exists (reqk in crit.keywords)
         exists (actk in q.keywords) reqk = actk)) and

      (* Of requested length *)
      (crit.dur = nil or (* "Any" duration encoded as nil *)
         (crit.durRel?lt and crit.dur < q.timeToComplete or
          crit.durRel?gt and crit.dur > q.timeToComplete or
          crit.durRel?eql and crit.dur = q.timeToComplete)) and

      (* Of requested difficulty *)
      (crit.diff = nil or (* "Any" difficulty encoded as nil *)
      (crit.diffRel?lt and crit.diff < q.difficulty or
       crit.diffRel?gt and crit.diff > q.difficulty or
       crit.diffRel?eql and crit.diff = q.difficulty)) and

      (* Meets last usage requirements *)
      (crit.use = nil or (* "Any" last usage encoded as nil *)
      (crit.useRel?lt and crit.use < q.dateLastUsed or
       crit.useRel?gt and crit.use > q.dateLastUsed or
       crit.useRel?eql and crit.use = q.dateLastUsed));
   );

   operation AutoAdd is
      inputs: crit:AdditionCriteria and t:GeneratedTest and bank:Bank;
      outputs: t':GeneratedTest;

      description: (*
         Add questions to test t according to criteria crit.
      *);

      precondition: (*
         A question in the question bank matches the user criteria.
      *)
      exists (q in bank) MeetsCriteria(q, crit) and
         (not exists (id in t) id = q.id);
         
      postcondition: (* The t' contains the old questions and a question
         meeting the criteria.
      *)
      (forall (q in bank)
         (q.id in t' iff q.id in t or MeetsCriteria(q, crit))) and

      (* The ordering of questions on the new test is the old questions
         followed by the added questions.
      *)
      forall (ndx:integer | ndx > 0 and ndx <= #t)
        t[ndx] = t'[ndx];

   end AutoAdd;

   function Replaceable(old:ID, new:ID, bank:Bank)->boolean = (
      let dDiff = bank[old].difficulty - bank[new].difficulty;

      (* Share a keyword *)
      (exists (ok in bank[old].keywords)
         exists (nk in bank[new].keywords) ok = nk) and

      (* Relevant to same course *)
      (bank[old].class = bank[new].class) and

      (* Question difficulties within two points *)
      (dDiff >= -2 and dDiff <= 2);
   );

   operation Replace is
      inputs: toReplace:ID* and t:GeneratedTest and qb:Bank;
      outputs: t':GeneratedTest;

      description: (* Replaces given questions on a test with other questions
        having similar attributes. 
      *);

      precondition:
         (forall (id in toReplace) 
            (* Question to replace is on the old test. *)
            (id in t) and

            (* A replacement exists *)
            (exists (q in qb) Replaceable(id, q.id, qb)));

      postcondition:
         (* The new test is old test, with the given questions replaced. *)
         (forall (id:ID)
            id in t' iff (id in t and not (id in toReplace)) and
            exists (q in qb) Replaceable(id, q.id, qb)) and

         (* This operation did not replace two questions with the same 
            question.
         *)
         UniqueQuestions(t') and

         (* The ordering is unchanged. *)
         (forall (ndx:integer | ndx > 0 and ndx <= #t)
            t[ndx] = t'[ndx] or 
             (t'[ndx] in toReplace and Replaceable(t[ndx], t'[ndx], qb)));

   end Replace;

   function UniqueQuestions(t:GeneratedTest)->boolean = 
   (
      #t = 1 or 
      
     (forall (i:integer | i > 0 and i < #t) t[i] != t[i+1]) and 
     UniqueQuestions(t[2:#t]);
   );

   obj Proctored;
   obj TakeHome;
   obj Practice;

   obj AdminOptDlg is
      description: (* The dialog through which users specify input
         administrative options *);
      components: 
         (* Radio buttons *)
         env:(proctored:Proctored or
          takeHome:TakeHome or 
          practice:Practice) and

         timeLimit:integer and
         proctor:User and
         proctorInstr:string and
         dueDate:Date and
         isLimitedAccess:boolean and
         studentInstr:string;
   end AdminOptDlg;

   op ValidateAdminEnv is
      inputs: dlg:AdminOptDlg, users:ValidUsers;
      outputs: opt:AdminEnv;

      description: (* Validates user input specifying exam environment. *);
   
      precondition:
         (* Proctored environments *)
         (dlg.env?proctored and 
            dlg.timeLimit > 0 and dlg.proctor in users) or

         (* Take-Home environments *)
         (dlg.env?takeHome and dlg.dueDate != nil) or

         (* Practice environment *)
         dlg.env?practice;

      postcondition:
         dlg.studentInstr = opt.studentInstr and

         (dlg.env?proctored and 
            dlg.timeLimit = opt.env.proc.timeLimit and
            dlg.proctor = opt.env.proc.proctor and
            dlg.isLimitedAccess = opt.env.proc.isLimitedAccess) and

         (dlg.env?takeHome and
            dlg.dueDate = opt.env.home.dueDate);
   end ValidateAdminEnv;

   object LoginInfo is
      description: (* Login info to authenticate users *);
      components: user:User and passwd:string;
   end LoginInfo;

   object Roster;

   op PublishTest is
      inputs: t:GeneratedTest, qb:Bank, opts:AdminEnv, auth:LoginInfo,
              roster:Roster;
      outputs: p:PublishedTest;

      description: (* Posts a test to the server for access by proctors
         and students. *);
      
      precondition:
         (* Test contains questions *)
         #t > 0 and 
         
         (* Take home and practice tests must be available to some students *)
         (opts.env?proc or roster != nil) and

         (* The user is authentic *)
         Authentic(auth);
 
      postcondition:
         (forall (q:TestQuestion)
            q in p.questions iff (q.id in t)) and
         
         (opts.env?home and opts.env.home.assigned = roster or
          opts.env?pract and opts.env.pract.assigned = roster);         
   end PublishTest;

   obj PublishedTest is 
      description: (* A test assigned available to students or proctors. *);
      components: questions:TestQuestion* and
         opts:AdminEnv and
         publisherID:User and
         datePublished:Date and
         instr:string;
   end PublishedTest;
  
   (* Validates against server environment user authentication process. *) 
   function Authentic(login:LoginInfo)->boolean = ();
end Test;