// From class, Feburary 12th 2014 sig TimeSlot {} sig Room{} sig Course { instructor : Faculty, roster : set Student, when : TimeSlot, where : Room, tas: set Student // NEW } // NEW fact NoOverlapTAs { all c : Course | no (c.tas & c.roster) } run {#tas > 0} for 3 // NEW // Alloy can do higher-order quantification in some limited // situations. The "lone" below won't run, but "some" will. // (We'll discuss the details of why "some" works in March.) pred Foo { // lone c : some Course | some c.roster some c : some Course | some c.roster } run Foo sig Faculty { office : Room, advisees: set Student } sig Student { schedule : set Course } sig GradStudent extends Student { office: Room } fact InjectiveWhen { when.~when in iden } // All NEW ////////////////////// fact LotsOfTAs { all c : Course | div[#c.roster, 2] = #c.tas } fact NoTACycles { no iden & ^(~roster . tas) } pred EvenNumberStudents[c: Course] { rem[#c.roster, 2] = 0 } // Bug here: not in fact what this predicate says. // Duplicates are included... fact ThreeStudentsEnrolled { (sum c : Course | #c.roster) = 3 }