// This example is part of the Christmas story:
//
//   How Formal Methods Save Christmas
//      by Jan O. Ringert
//
//   http://christmas.formal-methods.net/
//

module SecretSanta

abstract sig Employee {
	gender : one Gender,
	department : one Department,
	officePartners : set Employee,
	isSecretSantaOf : one Employee
}
abstract sig Secretary, Manager, Programmer, Writer extends Employee {}
abstract sig Intern extends Employee {	supervisor : one Employee }

enum Gender {male, female}
enum Department {Accounting, IT, Marketing, HR}

fact OfficePartnersAreOfficePartners {
	all disj e1, e2 : Employee |
		e1 in e2.officePartners implies e1.officePartners + e1 = e2.officePartners + e2
}

//////////////////////////////////
// Basic rules of the game
//////////////////////////////////

fact SecretSantaNotSelf {
	no e : Employee | 
		e.isSecretSantaOf = e
}

fact EverybodyHasASecretSanta {
	all e : Employee | 
		some se: Employee |	
			se.isSecretSantaOf = e
}

//////////////////////////////////
// The four rules of the company
//////////////////////////////////

fact NoInternSecretSantaOfDirectSupervisor {
	no i : Intern |
		i.isSecretSantaOf = i.supervisor
}

fact NoITEmployeeIsSecretSantaOfFemale {
	no e : Employee |
		e.department = IT and e.isSecretSantaOf.gender = female
}

fact AllManagersGetPresentsFromSecretaries {
	Manager in Secretary.isSecretSantaOf
}

fact NoSecretSantaInSameOffice {
	all e : Employee |
		e not in e.isSecretSantaOf.officePartners
}

//////////////////////////////////
// The given employee list
//////////////////////////////////

one sig Abigail extends Manager {} {
	gender = female
	department = IT
	no officePartners
}

one sig Jon extends Manager {} {
	gender = male
	department = Accounting
	no officePartners
}

one sig Andrew extends Secretary {} {
	gender = male
	department = IT
	officePartners = Anna
}

one sig Anna extends Secretary {} {
	gender = female
	department = Accounting
	officePartners = Andrew
}

one sig Max extends Intern {} {
	gender = male
	department = IT
	officePartners = Jane + Otto
	supervisor = Jane
}

one sig Jane extends Programmer {} {
	gender = female
	department = IT
	officePartners = Otto + Max
}

one sig Otto extends Writer {} {
	gender = male
	department = Marketing
	officePartners = Max + Jane
}

one sig Tom extends Writer {} {
	gender = male
	department = Marketing
	no officePartners
}

run {} for 0