module airtrafficsystem

sig Center {
	// A center contains one or more sectors
	contains : some Sector
}

sig Controller {
	// A controller works for zero or one center
	worksFor : lone Center,
	// A controller covers zero or more sectors
	covers : set Sector,
	// A controller controls zero or more aircrafts
	controls : set Aircraft
}
	
sig Aircraft {
	// An aircraft is within exactly one sector
	within : one Sector
} {
	// An aircraft is controlled by exactly one controller
	one this.~controls
}

sig Sector {
} {
	// A sector is contained by exactly one center
	one this.~contains
	// A sector is covered by one or more controllers
	some this.~covers
}

/* 
	If an aircraft is flying in a sector, then it is being controlled 
	by a controller that covers that sector.
*/
fact {
	all a : Aircraft | 
		a.within in a.~controls.covers
}

/*
	Controllers only cover sectors contained by centers they work for.
*/
fact {
	all cont : Controller |
		cont.covers in cont.worksFor.contains
}

pred Show {
	some Aircraft
}

run Show for 4