// From class Feb 21 sig TimeSlot {} sig Room {} abstract sig Person {} sig Course { instructor : Faculty, roster : set Student, when : TimeSlot, where : Room, tas: set Student } { // (implicit) // all this : Course | no tas & roster #tas > 2 implies not this.inoffice one c : Course - this | instructor = c.@instructor and roster = c.@roster and when != c.@when and (this.inoffice or inoffice[c]) } // Can invoke these using dot or bracket pred Course.inoffice { some o : OfficeHolder | this.where = o.office } fun Faculty.adviseecourses: set Course { this.advisees.schedule } sig OfficeHolder in Person { office: Room } sig Faculty extends Person { advisees: set Student } { Faculty in OfficeHolder } sig GradStudent extends Student {} { GradStudent in OfficeHolder } sig Student extends Person { schedule : set Course } { no (Student - GradStudent) & OfficeHolder} // message verbosity = high will show you the atoms created // as well as upper bounds: run {} for 3 but exactly 3 Room