SetOperators.als

/*
Name = {(G0),(A0),(A1)}
Alias = {(A0),(A1)}
Group = {(G0)}
RecentlyUsed = {(G0),(A1)}
*/
abstract sig Name {}
sig Alias extends Name {}
sig Group extends Name {}
sig RecentlyUsed in Name {}

fun Union []:set Name {
	Alias + Group	
}

fun Intersection []: set Name {
	Alias & RecentlyUsed
}

fun Difference []: set Name {
	Name - RecentlyUsed
}

pred Subset [] {
	RecentlyUsed in Name
}

pred Equality [] {
	Name = Group + Alias
}

fact example {
	#Name = 3
	#RecentlyUsed = 2
	some g:Group | g in RecentlyUsed
}

pred show [] {
	Subset[]
	Equality[]
}

run show for exactly 2 Alias, exactly 1 Group