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

scheme TravelExplicit=
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
		/* constant empty */
		emptyTravelList: TravelList = {},
		emptyStation: Station,

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

		/* ********************************************************************************** */
		/*							    Functions with time									  */
		/* change a time to seconds */
		toSeconds: Time -> Int
		toSeconds((h, m, s)) is h*3600 + m*60 + s,

		/* 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
		compareTime(t1, t2) is toSeconds(t1) - toSeconds(t2),

		/* check if a moment is in a range */
		isInTimeRange: Time >< TimeRange -> Bool
		isInTimeRange(t, (t1, t2)) is compareTime(t1, t) <= 0 /\ compareTime(t, t2) <= 0,


		/* ********************************************************************************** */
		/*                          Functions with bus stations								  */
		/* get gate list of a bus station */
		getStationGateList: Station -> Gate-list
		getStationGateList((name, gateList)) is gateList,

		/* ********************************************************************************** */
		/*                         Functions with a concrete travel							  */
		/* change start station */
		newTravelStart: Travel >< Start -~-> Travel
		newTravelStart((st, des, gt, bT, dT), newStart) is (newStart, des, gt, bT, dT)
		pre gt isin getStationGateList(newStart),

		/* change destination station */
		newTravelDestination: Travel >< Destination -> Travel
		newTravelDestination((st, des, gt, bT, dT), newDes) is (st, newDes, gt, bT, dT),

		/* change gate */
		newTravelGate: Travel >< Gate -~-> Travel
		newTravelGate((st, des, gt, bT, dT), newGate) is (st, des, newGate, bT, dT)
		pre newGate isin getStationGateList(st),

		/* change boarding time */
		newTravelBoardingTime: Travel >< Time -~-> Travel
		newTravelBoardingTime((st, des, gt, bT, dT), newBT) is (st, des, gt, newBT, dT)
		pre compareTime(newBT, dT) < 0,

		/* change departure time */
		newTravelDepartureTime: Travel >< Time -~-> Travel
		newTravelDepartureTime((st, des, gt, bT, dT), newDT) is (st, des, gt, bT, newDT)
		pre compareTime(bT, newDT) < 0,

		/* get travel start station */
		getTravelStart: Travel -> Start
		getTravelStart((st, des, gt, bT, dT)) is st,

		/* get travel destination station */
		getTravelDestination: Travel -> Destination
		getTravelDestination((st, des, gt, bT, dT)) is des,

		/* get travel gate */
		getTravelGate: Travel -> Gate
		getTravelGate((st, des, gt, bT, dT)) is gt,

		/* get travel boarding time */
		getTravelBoardingTime: Travel -> Time
		getTravelBoardingTime((st, des, gt, bT, dT)) is bT,

		/* get travel departure time */
		getTravelDepartureTime: Travel -> Time
		getTravelDepartureTime((st, des, gt, bT, dT)) is dT,

		/* check conflict of one travel with a travel-list */
		isTravelCorrect: Travel >< TravelList -> Bool
		isTravelCorrect(tr, trlist) is
			let dT = getTravelDepartureTime(tr) in
				let bT = getTravelBoardingTime(tr) in
					all t : Travel :- t isin trlist /\ getTravelGate(t) = getTravelGate(tr) =>
						let dt = getTravelDepartureTime(t) in
							let bt = getTravelBoardingTime(t) in
								~isInTimeRange(bt, (bT, dT)) /\ ~isInTimeRange(dt, (bT, dT))
							end
						end
				end
			end,		


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

		/* ********************************************************************************** */
		/*                                get useful info									  */
		/* all travels from a station */
		getTravelsFrom: Start >< TravelList -> Travel-set
		getTravelsFrom(st, trlist) is
			{ tr | tr: Travel :- tr isin trlist /\ getTravelStart(tr) = st },

		/* all travels from a station in a time range */
		getTravelsInDepartureTimeRangeFrom: Start >< TimeRange >< TravelList -> Travel-set
		getTravelsInDepartureTimeRangeFrom(st, timeRange, trlist) is
			let res = getTravelsFrom(st, trlist) in
				{ tr | tr: Travel :- tr isin res /\ isInTimeRange(getTravelDepartureTime(tr), timeRange) }
			end,
			

		/* all travels to a station */
		getTravelsTo: Destination >< TravelList -~-> Travel-set
		getTravelsTo(des, trlist) is
			{ tr | tr: Travel :- tr isin trlist /\ getTravelDestination(tr) = des },

		/* all travles to a station in a time range */
		getTravelsInDepartureTimeRangeTo: Destination >< TimeRange >< TravelList -~-> Travel-set
		getTravelsInDepartureTimeRangeTo(des, timeRange, trlist) is
			let res = getTravelsTo(des, trlist) in
				{ tr | tr: Travel :- tr isin res /\ isInTimeRange(getTravelDepartureTime(tr), timeRange) }
			end,

		/* all travels that start from a gate */
		getTravelsFromAGate: Gate >< TravelList -~-> Travel-set
		getTravelsFromAGate (g, trlist) is
			{ tr | tr: Travel :- tr isin trlist /\ getTravelGate(tr) = g },

		/* get full info of a travel */
		getTravelInfo: Start >< Destination >< TravelList -~-> Travel-set
		getTravelInfo(st, des, trlist) is
			getTravelsTo(des, getTravelsFrom(st, trlist)),


		/* ********************************************************************************** */
		/*                         replace a travel with new info							  */
		/* replace start station */
		replaceStart: Travel >< Start >< TravelList -~-> TravelList
		replaceStart(tr, newStart, trlist) is
			(trlist \ {tr}) union {newTravelStart(tr, newStart)}
		pre tr isin trlist,

		/* replace destination station */
		replaceDestination: Travel >< Destination >< TravelList -~-> TravelList
		replaceDestination(tr, newDes, trlist) is
			(trlist \ {tr}) union {newTravelDestination(tr, newDes)}
		pre tr isin trlist,

		/* replace gate */
		replaceGate: Travel >< Gate >< TravelList -~-> TravelList
		replaceGate(tr, newGate, trlist) is
			(trlist \ {tr}) union {newTravelGate(tr, newGate)}
		pre tr isin trlist /\ isTravelCorrect(newTravelGate(tr, newGate), trlist \ {tr}),

		/* replace boarding time */
		/* new boarding time must not conflict with other travel in the gate */
		replaceBoardingTime: Travel >< Time >< TravelList -~-> TravelList
		replaceBoardingTime(tr, newBT, trlist) is
			(trlist \ {tr}) union {newTravelBoardingTime(tr, newBT)}
		pre tr isin trlist /\ isTravelCorrect(newTravelBoardingTime(tr, newBT), trlist \ {tr}),

		/* replace departure time */
		replaceDepartureTime: Travel >< Time >< TravelList -~-> TravelList
		replaceDepartureTime(tr, newDT, trlist) is
			(trlist \ {tr}) union {newTravelDepartureTime(tr, newDT)}
		pre tr isin trlist /\ isTravelCorrect(newTravelDepartureTime(tr, newDT), trlist \ {tr}),

		/* replace entirely a travel */
		replaceTravel: Travel >< Travel >< TravelList -~-> TravelList
		replaceTravel(tr, newTravel, trlist) is
			(trlist \ {tr}) union {newTravel}
		pre newTravel ~isin trlist /\ tr isin trlist /\ isTravelCorrect(newTravel, trlist \ {tr}),

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

		/* add a new travel */
		addTravel: Travel >< TravelList -~-> TravelList
		addTravel(tr, trlist) is (trlist union {tr})
		pre tr ~isin trlist /\ isTravelCorrect(tr, trlist),

		/* delete a travel */
		deleteTravel: Travel >< TravelList -~-> TravelList
		deleteTravel(tr, trlist) is (trlist \ {tr})
		pre tr isin trlist
end