module paper/uwedv1
open paper/uwest1
open std/ord

/*
model of a student's degree 
*/

sig Student {
      suspension : option Suspension,
      stage : set Stage
}

sig Suspension {}
sig Stage {
      prev, next  : option Stage,
      level : Level,
      register : set Registration,
      results : set Result,
      taking, registered, passed, allPassed : set Module
}
{  one s : Student | this in s.stage }
fact { all s : Student {
        all t : s.stage {
-- prev and next derived from the same relationship between Levels
           t.prev = { tl : s.stage | tl.level= OrdPrev(t.level) }
           t.next = { tl : s.stage | tl.level= OrdNext(t.level) }
        }
-- one Stage per Level
        (all disj t,v : s.stage | t.level != v.level)
-- if only one Stage, it must be at the first Level 
        (some s.stage
           => one t : s.stage | t.level = Ord[Level].first )
   }
}


sig Registration {
      mod : Module
}
{ one s : Stage | 
       this in s.register 
    && sole r : s.results | r.reg = this
}
sig Result {
      reg : Registration
}
{ one s : Stage |
       this in s.results 
}

// Define derived relations

fact {  all t : Stage {
-- passed is the set of Modules with a Pass Result at this Stage
      t.passed = (t.results & Pass).reg.mod 
-- allPassed is the set of Modules passed at this and previous Stages
      t.allPassed = (t.*prev).passed
-- taking are the modules being taken but not yet examined
      t.taking = (t.register - t.results.reg).mod
-- registered are the modules which the student has registered for
      t.registered = t.register.mod
   }
}

//  Constraints to enforce integrity

disj sig Pass, Fail extends Result {}
fact { Result in Pass + Fail}

// various application constraints

disj sig Passed extends Stage {}
fact {  
-- Stage is Passed if 2 modules have been passed 
      Passed = { t : Stage | #t.passed = 2 }
}

fact {all t : Stage {
-- if Stage is not Passed, can't proceed to next Stage
      ( t !in Passed => no t.next )
-- can't register for modules unless previous Stage is Passed
      some t.registered => t.prev in Passed 
-- can't be taking a module which has been passed
      no t.taking & t.allPassed 
--  can't pass a module more than once
      #t.passed = #(t.results & Pass)  
-- cant be taking the same module twice
      #t.taking = #(t.register - t.results.reg)
-- never taking or passed more than 2 modules 
      #(t.taking + t.passed) =< 2 
-- only register for modules at the student's level
      (all m : t.registered | m.level = t.level) 
-- no excluded modules taken
      no (t.taking + t.allPassed) & (t.taking + t.allPassed).excludes 
-- all prerequistes passed
      (t.allPassed + t.taking).prereq in t.allPassed 
-- all corequistes being taken or are passed
      t.taking.coreq in t.taking
--     t.allPassed.coreq in t.allPassed   
   }
}

// define the conditions for Graduation
disj sig Graduate extends Student{}
disj sig Honours, Ordinary extends Graduate {}
fact { Graduate in Honours + Ordinary }
fact { Graduate = { s : Student | some t : s.stage |
       t.level = Ord[Level].last  && t in Passed }
}
fact { Honours  = { s : Graduate |
       no s.stage.results & Fail && no s.suspension }
}
fact { Ordinary  = { s : Graduate |
       some s.stage.results & Fail || some s.suspension }
}

// function to create interesting student Careers

fun showHonours() { some Honours }
fun showOrdinary() { some Ordinary }
fun showCoreq() {
-- some student is taking modules with corequisites
      some s: Student | some s.stage.taking.coreq
}

run showHonours for 6 but 2 Level, 1 Student
run showOrdinary for 6 but 2 Level, 1 Student
run showCoreq for 6 but 2 Level, 1 Student