model ATC {

	domain {fixed Flight, fixed Track, fixed Sector}

	state {
		tracks (~sector): static Sector! -> static Track

		controls (~controlled): Sector! -> Flight
		watches     (~watched): Sector+ -> Flight
		advise      (~advised): Sector? -> Flight

		currentTrack: Flight -> Track!
		nextTrack:    Flight -> Track!
		thirdTrack:   Flight -> Track!
		fourthTrack:  Flight -> Track!
	}

	inv properControl {
		all f: Flight |
			f.controlled = f.currentTrack.sector &&
			f.watched    = (f.currentTrack + f.nextTrack +
					    f.thirdTrack   + f.fourthTrack).sector
	}

	cond noCurrentConflict {
		no f1, f2: Flight |
			f1 != f2 && f1.currentTrack = f2.currentTrack
	}

	cond noNextConflict {
		no f1, f2: Flight |
			f1 != f2 && f1.nextTrack = f2.nextTrack
	}

	cond properAdvisory {
		all s: Sector |
			(all f1: s.advise |
				(f1 in s.watches - s. controls &&
				 f1.thirdTrack.sector = s))
			&&
			(all f1, f2: s.watches - s.controls |
				(f1 != f2 && f1.thirdTrack = f2.thirdTrack &&
				 f1.thirdTrack.sector = s) ->
					(f1 in s.advise || f2 in s.advise))
	}
	
	op amendTrajectories(s: Sector!) {
		all f1, f2: s.controls + s.advise |
			f1 != f2 -> f1.nextTrack' != f2.nextTrack'

		all f1: s. controls + s.advise |
			all f2: s.watches - s.controls - s.advise |
				f1.nextTrack' != f2.thirdTrack

		all f: s.controls |
			f.nextTrack'.sector = f.thirdTrack.sector &&
			(f.thirdTrack.sector != s  && no f.advised ->
				f.nextTrack' = f.thirdTrack) &&
			f.thirdTrack' = f.fourthTrack
	}

	op amendAll {
		all s: Sector | amendTrajectories(s)
	}

	op adviseFlights(s: Sector!) {
		(all f1: s.advise' |
			(f1 in s.watches &&
			 f1.nextTrack.sector != s &&
			 f1.fourthTrack.sector = s))
		&&
		(all f1, f2: s.watches |
			(f1 != f2 && f1.fourthTrack = f2.fourthTrack &&
			 f1.nextTrack.sector != s && f2.nextTrack.sector != s &&
			 f1.fourthTrack.sector = s) ->
				(f1 in s.advise' || f2 in s.advise'))
	}

	op adviseAll {
		all s: Sector | adviseFlights(s)
	}

	op flightsMove {
		all f: Flight | f.currentTrack' = f.nextTrack
	}

	assert properAdvisoryAssert {
		adviseAll && amendAll && flightsMove -> properAdvisory'
	}

	assert noCurrentConflictAssert {
		noNextConflict && flightsMove -> noCurrentConflict'
	}

	assert noNextConflictAssert {
		properAdvisory && amendAll -> noNextConflict'
	}

	assert safeFlightAssert {
		noNextConflict && properAdvisory &&
		adviseAll && amendAll && flightsMove
			-> noCurrentConflict' && noNextConflict' && properAdvisory'
	}

}