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

sig SysState {
      taking, passed : set Module,
      level : option Level,
      event : option Event,
      available : set Module,
      smode : Smode
}

sig Smode{}
static disj sig Initial, Active,Suspended, Ordinary, Honours extends Smode {}
sig Final extends Smode {}
fact {Final = Ordinary + Honours }



//  Event instances 

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

fact {ModuleEvent in Take + Fail + Pass + Toggle}
fact { all e : Event | some s: SysState | e in s.event}
      
//  Pre-conditions

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

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

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

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

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

// Actions 

fun doStudInitial(s :SysState) {
      no s.taking
      no s.passed
      no s.level
      no s.event
      s.smode in Initial
}

fun doModInitial(s : SysState) {
      all m : Module | m in s.available
}

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

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

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

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

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

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

fun doNothing (s,s' :SysState) {
      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 UnivProcess {
      doStudInitial(Ord[SysState].first)
      doModInitial(Ord[SysState].first)
      Ord[SysState].last.smode in Final
      all s : SysState - Ord[SysState].last |
         let s' = OrdNext(s) |
           some e : Event {
              studTrans(s,s',e)
              all m : Module | modTrans(m,s,s',e)
              s'.event = e
           }
}


//  define the  Student transitions 
fun studTrans (s,s' : SysState, e :Event) {

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



fun modTrans(mod : Module, s,s' : SysState, e : Event) {
     e in Take && e.m = mod  =>  mod !in s'.available
     else 
       e in Toggle && e.m = mod && mod in s.available =>
          mod !in s'.available
     else
       e in Toggle && e.m = mod && mod !in s.available =>
          mod in s'.available
     else 
        mod in s.available =>  mod in s'.available
     else 
        mod !in s.available => mod !in s'.available
}

fun showHonoursCareer()  { 
      Ord[SysState].last.smode in Honours
      some SysState.event & Toggle
}

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

assert inv1 {  all s :SysState  {
-- 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) 
-- no excluded modules taken
      no (s.taking + s.passed) & (s.taking + s.passed).excludes
-- all prerequistes passed
      (s.passed + s.taking).prereq in s.passed  
  }  
}

assert noSuspension {
      Ord[SysState].last.smode in Honours =>
      no s: SysState | s.smode in Suspended 
}

run showHonoursCareer for 8 but 1 Level, 4 Module
run showFailCareer for 8 but 1 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: SysState | #s.taking =< 2 }
check only2 for 12 but 2 Level, 6 Module