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

class Airline ^=
abstract
	var 
		name : string,
		aircraft : set of Aircraft,
		pilots : set of Pilot,
		schedule : set of Flight;
		
	invariant
		#aircraft > 0, // ASSUMPTION: Airlines reasonably need to have at least one type of aircraft
		#pilots > 1, // Since flights need at least two pilots each, an airline cannot operate with fewer than 2 pilots
		~(exists x::pilots, y::pilots :- x.id = y.id), // There does not exist a pair of different pilots that share an ID(Unique ID constraint)
		~(exists x::schedule, y::schedule :- x.code = y.code), // Set guarentees unique object, not unique ID as per Spec
		forall x::pilots, y::aircraft :- exists z::x.flyables :- z = y;

interface
	schema !addFlight(flight : Flight)
		pre 
			flight ~in schedule,
			~(exists x::schedule :- x.code = flight.code)
		post schedule! = schedule.append(flight)
		assert flight in schedule';
		
	schema !removeFlight(flight : Flight)
		pre flight in schedule
		post schedule! = schedule.remove(flight);
	
	function fullFlights:set of Flight
		^= those f :: schedule :- f.isFull;
	
	build{!name:string, !aircraft:set of Aircraft, !pilots:set of Pilot}
		pre
			#aircraft > 0,
			#pilots > 1,
			~(exists x::pilots, y::pilots :- x.id = y.id),
			forall x::pilots, y::aircraft :- exists z::x.flyables :- z = y
		post schedule! = set of Flight{};
end;