/*															                  */
/*	author: Tran Duc Hieu													  */
/*	group: 422																  */
/*	email: antiw@lvk.cs.msu.su												  */
/*	date: 22.Oct.2006														  */
/*																			  */

scheme TravelAbstract=
class
	type
		/* station type */
		Gate = Int,
		StationName = Text,
		Station = StationName >< Gate-list,
		Start = Station,
		Destination = Station,

		/* type time */
		Hour = {| h: Int :- h >=0 /\ h <= 23 |},
		Minute = {| m: Int :- m >= 0 /\ m <= 59 |},
		Second = {| s: Int :- s >= 0 /\ s <= 59 |},
		Time = Hour >< Minute >< Second,
		TimeRange = Time >< Time,
		BoardingTime = Time,
		DepartureTime = Time,

		Travel = Start >< Destination >< Gate >< BoardingTime >< DepartureTime,
		TravelList = Travel-set
	value
		emptyTravelList: TravelList,
		emptyStation: Station,

		/* ********************************************************************************** */
		/*                                AGENT FUNCTIONS									  */
		/* ********************************************************************************** */

		/* ********************************************************************************** */
		/*							    Functions with time									  */
		/* change a time to seconds */
		toSeconds: Time -> Int,

		/* comparision of 2 moment t1, t2, return:
		     - a negative number if t1 < t2
		     - zero if t1 = t2
			 - a positive number if t1 > t2
		 */
		compareTime: Time >< Time -> Int,

		/* check if a moment is in a range */
		isInTimeRange: Time >< TimeRange -> Bool,


		/* ********************************************************************************** */
		/*                          Functions with bus stations								  */
		/* get gate list of a bus station */
		getStationGateList: Station -> Gate-list,


		/* ********************************************************************************** */
		/*                         Functions with a concrete travel							  */
		/* change start station */
		newTravelStart: Travel >< Start -~-> Travel,

		/* change destination station */
		newTravelDestination: Travel >< Destination -> Travel,

		/* change gate */
		newTravelGate: Travel >< Gate -~-> Travel,

		/* change boarding time */
		newTravelBoardingTime: Travel >< Time -~-> Travel,

		/* change departure time */
		newTravelDepartureTime: Travel >< Time -~-> Travel,

		/* get travel start station */
		getTravelStart: Travel -> Start,

		/* get travel destination station */
		getTravelDestination: Travel -> Destination,

		/* get travel gate */
		getTravelGate: Travel -> Gate,

		/* get travel boarding time */
		getTravelBoardingTime: Travel -> Time,

		/* get travel departure time */
		getTravelDepartureTime: Travel -> Time,

		/* check conflict of one travel with a travel-list */
		isTravelCorrect: Travel >< TravelList -> Bool,


		/* ********************************************************************************** */
		/*									PUBLIC FUNCTIONS								  */
		/* ********************************************************************************** */

		/* ********************************************************************************** */
		/*                                get useful info									  */
		/* all travels from a station */
		getTravelsFrom: Start >< TravelList -> Travel-set,			

		/* all travels to a station */
		getTravelsTo: Destination >< TravelList -~-> Travel-set,

		/* all travles to a station in a time range */
		getTravelsInDepartureTimeRangeTo: Destination >< TimeRange >< TravelList -~-> Travel-set,

		/* all travels that start from a gate */
		getTravelsFromAGate: Gate >< TravelList -~-> Travel-set,

		/* get full info of a travel */
		getTravelInfo: Start >< Destination >< TravelList -~-> Travel-set,


		/* ********************************************************************************** */
		/*                         replace a travel with new info							  */
		/* replace start station */
		replaceStart: Travel >< Start >< TravelList -~-> TravelList,

		/* replace destination station */
		replaceDestination: Travel >< Destination >< TravelList -~-> TravelList,

		/* replace gate */
		replaceGate: Travel >< Gate >< TravelList -~-> TravelList,

		/* replace boarding time */
		/* new boarding time must not conflict with other travel in the gate */
		replaceBoardingTime: Travel >< Time >< TravelList -~-> TravelList,

		/* replace departure time */
		replaceDepartureTime: Travel >< Time >< TravelList -~-> TravelList,

		/* replace entirely a travel */
		replaceTravel: Travel >< Travel >< TravelList -~-> TravelList,

		/* ********************************************************************************** */
		/*						ADD/DELETE A TRAVEL FROM A TRAVEL-LIST						  */

		/* add a new travel */
		addTravel: Travel >< TravelList -~-> TravelList,

		/* delete a travel */
		deleteTravel: Travel >< TravelList -~-> TravelList
end