//*******************************************************
//* File:    /Airport.pd
//* Author:  UP696771
//* License: See /LICENSE
//* For full list of assumptions, please see /assumptions.txt
//*******************************************************
import "Flight.pd";

class Airport ^=
abstract
	var 
		name : string,
		code : string,
		flights : set of Flight;
	
	invariant 
		#code = 3, // International convention for each airport to have three letter code
		~(exists x::flights, y::flights :- x.code = y.code);
	
interface
	function flights;
	function inbound:set of Flight
		^= those f :: flights :- f.route.y = self;
		
	function outbound:set of Flight
		^= those f :: flights :- f.route.x = self;
		
	build{!name:string, !code:string}
		pre #code = 3
		post flights! = set of Flight{};
end;