module paper/uwedn
open std/ord
open paper/uwest1

sig StudState {
      taking, passed : set Module,
      level : option Level,
      event : option Event
}

disj sig Init, Intermediate, Final extends StudState {}
sig Initial extends Init {}
disj sig Active, Suspended extends Intermediate {}
fact {Intermediate in Active + Suspended }
disj sig Ordinary, Honours extends Final {}
fact {Final in Ordinary + Honours }



//  Event instances 

sig Event {}
disj sig  Enrol, ME, Suspend, Reinstate extends Event{}
fact {Event in Enrol + ME  + Suspend + Reinstate}
sig ModuleEvent extends ME {
      m : Module
}
disj sig  Take, Fail, Pass extends ModuleEvent {}

fact {ModuleEvent in Take + Fail + Pass }
fact { all e : Event | some s: StudState | e in s.event}

//  Pre-conditions

fun canTake (m : Module, s: StudState) {
      m !in (s.passed + s.taking) 
      m !in (s.passed+s.taking).excludes 
      m.prereq in s.passed
      m.level = s.level
      #s.taking < 2
}

fun canSit (m : Module, s : StudState) {
      m in s.taking 
}

fun canProgress (s : StudState) {
      #{ m : s.passed | m.level = s.level } = 2 
      s.level!=Ord[Level].last 
      no s.taking
}

fun canGraduate (s : StudState ) {
      #{ m : s.passed | m.level = s.level } = 2 
      s.level=Ord[Level].last 
      no s.taking
}
fun canGraduateHonours (s :StudState) {
-- can only finish with Honours if never Suspended and no module Failed
      canGraduate(s)
      no OrdPrevs(s) & Suspended
      no OrdPrevs(s).event & Fail
}

fun canGraduateOrdinary (s :StudState) {
-- Ordinary if ever Suspended or module Failed
      canGraduate(s)
      some OrdPrevs(s) & Suspended || some OrdPrevs(s).event & Fail
}

// Actions 

fun doInitial(s :StudState) {
      no s.taking
      no s.passed
      no s.level
      no s.event
      s in Initial
}

fun doEnrol ( s,s' : StudState ) {
      s'.level=Ord[Level].first 
      no s'.passed 
      no s'.taking   
}

fun doTake (m : Module, s, s' : StudState) {
      s'.taking = s.taking + m
      s'.passed = s.passed 
      s'.level = s.level
}

fun doPass (m : Module, s, s' : StudState) {
      s'.taking = s.taking - m
      s'.passed = s.passed + m 
      s'.level = s.level
}

fun doFail (m: Module , s, s' : StudState) {
      s'.taking = s.taking - m 
      s'.passed = s.passed 
      s'.level = s.level
}

fun doProgress(s,s' : StudState) {
      s'.level = OrdNext(s.level) 
      s'.passed = s.passed 
      s'.taking = s.taking
}

fun doGraduate (s,s' : StudState) {
      s'.passed = s.passed 
      no s'.taking 
      s'.level = s.level
}

fun doNothing (s,s' :StudState) {
      s'.passed = s.passed 
      s'.taking = s.taking
      s'.level = s.level
}

// define the initial state , final state and the ordering 
// at each step, some Event occurs

fact StudentProcess {
      doInitial(Ord[StudState].first)
      Ord[StudState].last in Final
      all s : StudState - Ord[StudState].last |
         let s' = OrdNext(s) |
           some e : Event |
              doStep(s,s',e)
}


//  define the  Student transitions 
fun doStep (s,s' : StudState, e :Event) {

--Initial  ---- Enrol   -->   Active
      s in Initial && e in Enrol &&
         doEnrol(s,s') && s' in Active  && s'.event=e
--Active  --- Take(m)  -->  Active
   || s in Active && e in Take && canTake(e.m,s) &&
         doTake(e.m,s,s') && s' in Active && s'.event=e
--Active  --- Pass(m)  --> Active
   || s in Active && e in Pass && canSit(e.m,s) &&
         doPass(e.m,s,s') && s' in Active && s'.event=e
--Active  --- Fail(m)  --> Active
   || s in Active && e in Fail && canSit(e.m,s) &&
         doFail(e.m,s,s') && s' in Active && s'.event=e
--Active  -- [canprogress]  --> Active
   || s in Active  && canProgress(s) &&
         doProgress(s,s') && s' in Active && no s'.event
--Active   -- Suspend --> Suspended
   || s in Active && e in Suspend &&
         doNothing(s,s') && s' in Suspended && s'.event=e
--Suspended -- Reinstate --> Active
   || s in Suspended && e in Reinstate &&
         doNothing(s,s') && s' in Active && s'.event=e
--Active  -- [canGradateHonours] --> Honours 
   || s in Active  && canGraduateHonours(s) &&
         doGraduate(s,s') && s' in Honours && no s'.event 
--Active  -- [canGradateOrdinary] --> Ordinary 
   || s in Active  &&  canGraduateOrdinary(s) && 
         doGraduate(s,s') && s' in Ordinary && no s'.event
--Final  -- any --> Final (final stutter step due to Ord implementation)
   || s in Final &&
         doNothing(s,s') && s' in Final && no s'.event  
}

fun showHonoursCareer()  { 
      Ord[StudState].last in Honours 
}

fun showFailCareer()  { 
      Ord[StudState].last  in Final       
      Fail in StudState.event 
}

assert inv1 {  all s :StudState  {
-- can't be taking a module which has been passed
      no s.taking & s.passed  
-- never taking more than 2 modules 
      #s.taking =< 2 
-- only taking modules at the student's level
      (all m : s.taking | m.level = s.level) 
-- all prerequistes passed
      (s.passed + s.taking).prereq in s.passed  
  }  
}
assert noexcluded{ 
-- no excluded modules taken when finished
      let s = Ord[StudState].last |
      no (s.taking + s.passed) & (s.taking + s.passed).excludes 
}
check noexcluded for 12 but 2 Level, 4 Module

assert noSuspension {
      Ord[StudState].last in Honours =>
      no StudState & Suspended 
}

run showHonoursCareer for 12 but 2 Level, 4 Module
run showFailCareer for 16 but 2 Level, 4 Module

check noSuspension for 14 but 2 Level, 4 Module
check inv1 for 12 but 1 Level, 4 Module

assert only2 { all s: StudState | #s.taking =< 2 }
check only2 for 12 but 2 Level, 6 Module 

-- fact {  some s:Module | some s.excludes }