// taken from 
// https://github.com/franklingu/collections/tree/master/Alloy/Samples

abstract sig Grade {}
one sig A, B, C, D, F extends Grade {}

abstract sig Course {
  dept : Dept
}

sig Introductory extends Course {}

sig Advanced extends Course {
  prereqs : some Course
}

sig Elective in Course {}


abstract sig Student {
  major:  lone Dept,
  taken: set Course,
  grades: taken -> one Grade 
}

sig Freshman, Sophomore, Junior, Senior extends Student {}

sig Dept {
  required : set Course,
  listing : set Course
}

fact defineListing {
  listing = ~dept
}

fact prereqsAcyclic {
  all c: Course | c not in allPrereqs[c]
}

fact allPrereqsMet{
  all s:Student | allPrereqsMet[s]
}

pred  allPrereqsMet[s:Student] {
 	no c:Advanced | (c in s.taken) &&( (not  c.^prereqs in s.taken))  
	// Intentionally we have not  checked for mark of prereqs, you may do 
	// it similar to  canGraduate
}

fun allPrereqs [cs: set Course] : set Course {
  cs.^prereqs
}

pred canGraduate [s: Student] { 
  s in Senior
  some s.major
  some s.major.required
  some s.taken & Elective
  all c: s.major.required |c in s.taken 
  all c:  s.taken | some s.grades[c] & (A + B + C)
}
pred simulate {
  all d: Dept | some d.listing & Advanced
  some s: Student | canGraduate[s]
}
run simulate for 5

pred graduateImpliesAllPrereqs {
  all s: Student | canGraduate[s] =>
    allPrereqs[s.taken] in s.taken
}

assert graduatesCorrect {
  graduateImpliesAllPrereqs
}
check graduatesCorrect for 6