module paper/uwest1
open std/ord

sig Level {}
sig Module {
      disj prereq, coreq, excludes : set Module,
      level : Level
}

fact {
-- module cant exclude itself
       all m : Module | m !in m.excludes
-- module cant be coreq of itself
       no Module$coreq & iden[Module]
-- no cycles in prerequites
       no m : Module | m in m.^prereq
}

-- define a generic condition for an equivalence relation

fun Equivalence [t] (r : t->t) {
      iden[t] in r   -- reflexive
      r.r in r       -- transitive
      ~r = r         -- symmetric
}


fact {
-- coreqs are an equivalence relation if the module itself is included
      Equivalence (Module$coreq + iden[Module])
-- prereqs must be at a lower level
      all m: Module {
         all p : m.prereq | OrdLT(p.level, m.level)
-- coreqs must be at the same level
         all c : m.coreq | c.level = m.level
      }
}

fun showRich () {
      some m: Module | some m.coreq 
      some m: Module | some m.prereq
      some m: Module | some m.excludes
}
-- define the set of all modules which are required for module m
fun allreq(m : Module) : set Module {
 --      result = (m + m.coreq).*prereq     -- m.*r = m + m.^r
         result = m.*(prereq+coreq)
}

fact { all m : Module |
-- excluded modules must not be required, directly or indirectly
      no (allreq(m) & m.excludes)
}


run showRich for 6 but 2 Level


fact reverse { all m : Module |
-- module must not be excluded by modules required 
      no (allreq(m).excludes & m)
}

-- check reverse for 6 but 2 Level