developers.als

sig FriendGroup {
	members: set Developer
}

sig Developer {
	// Each Developer is only working on zero or more Projects
	project: set Project,

	// The set of languages the developer enjoys using.
	// `some` means that there is at least one language in this set
	languages: some Language
}

sig Project {
	// The language that this project is implemented in
	language: Language
}

fact ProjectFacts {
	// Require that each project has at least one happy developer
	all p: Project | some d: Developer | d.project = p and isHappy [d]
	
}

// By being `abstract`, it means we won't have any instances of "Language",
// we'll only have instances of things that extend "Language
abstract sig Language {}

// By using `one`, we are instructing Alloy to always generate
// exactly one Python instance, one Java instance, and one Go instance
// This is sort of similar to an enumeration, or a constant
one sig Python, Java, Go extends Language {}

pred isHappy (d: Developer) {
	let team = {p: Developer  - d| p.project = d.project} | {
		d.project.language in d.languages
		or (some group: FriendGroup | d in group.members and some team & group.members)
	}
}

pred happy () {
	// Developers are only happy if they are working with 
	// a friend, or if they enjoy the language of their project
	all d: Developer | isHappy [d]
}

pred success () {
	// Projects are only successful if one at least one
	// of its developers enjoys using the project's language
	all p: Project | some d: Developer | d.project = p and p.language in d.languages
}

pred veryHappy () {
	// A developer is very happy if they are working with
	// friends AND they enjoy their project's language
	all d: Developer | let team = {p: Developer  -d| p.project = d.project} |  {
		d.project.language in d.languages
		and (some group: FriendGroup | d in group.members and some team & group.members)
	}
}


check { 
	happy
}

check {
	success
}

check HappyLeadsToSuccess {
	// Happy developers lead to successful projects
	happy implies success
}

check SuccessLeadsToHappiness {
	// Successful projects lead to happy developers
	success implies happy
}

check EveryProjectHasDevelopers {
	all p: Project | some d: Developer | d.project = p
}

run AtLeastOneDeveloperIsOnMoreThanOneProject {
	some d: Developer | #d.project > 1
	success
}

run happy
run success
run veryHappy