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

scheme TravelImplicit=
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)) as res
			post h*3600 + m*60 + s = res,

		/* 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) as res
			post toSeconds(t1) - toSeconds(t2) = res,

		/* check if a moment is in a range */
		isInTimeRange: Time >< TimeRange -> Bool
		isInTimeRange(t, (t1, t2)) as res
			post res = ((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)) as res
			post gateList = res,


		/* ********************************************************************************** */
		/*                         Functions with a concrete travel							  */
		/* get travel start station */
		getTravelStart: Travel -> Start
		getTravelStart((st, des, gt, bT, dT)) as res
			post st = res,

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

		/* get travel gate */
		getTravelGate: Travel -> Gate
		getTravelGate((st, des, gt, bT, dT)) as res
			post res = gt,

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

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

		/* change start station */
		newTravelStart: Travel >< Start -~-> Travel
		newTravelStart((st, des, gt, bT, dT), newStart) as  res
			post (newStart, des, gt, bT, dT) = res
		pre gt isin getStationGateList(newStart),

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

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

		/* check conflict of one travel with a travel-list */
		isTravelCorrect: Travel >< TravelList -> Bool
		isTravelCorrect((st, des, gt, bT, dT), trlist) as res
			post res = ~(exists t : Travel :- (t isin trlist) /\ (getTravelGate(t) = gt) /\
								(isInTimeRange(getTravelBoardingTime(t), (bT, dT)) \/ isInTimeRange(getTravelDepartureTime(t), (bT, dT)))),


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

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


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

		/* ********************************************************************************** */
		/*                                get useful info									  */
		/* all travels from a station */
		getTravelsFrom: Start >< TravelList -> Travel-set
		getTravelsFrom(st, trlist) as res
			post ((all tr: Travel :- tr isin trlist /\ getTravelStart(tr) = st => tr isin res) /\
					~(exists tr: Travel :- tr isin res /\ tr ~isin trlist)),

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

		/* all travels to a station */
		getTravelsTo: Destination >< TravelList -~-> Travel-set
		getTravelsTo(des, trlist) as res
			post ((all tr: Travel :- tr isin trlist /\ getTravelDestination(tr) = des => tr isin res)
					/\ ~(exists tr: Travel :- tr isin res /\ tr ~isin trlist)),

		/* all travels from a station in a time range */
		getTravelsInDepartureTimeRangeTo: Start >< TimeRange >< TravelList -> Travel-set
		getTravelsInDepartureTimeRangeTo(des, timeRange, trlist) as res
			post let x = getTravelsTo(des, trlist) in
				 ((all tr: Travel :- tr isin x /\ isInTimeRange(getTravelDepartureTime(tr), timeRange) => tr isin res)
					/\ ~(exists tr: Travel :- tr isin res /\ tr ~isin trlist))
			end,


		/* all travels that start from a gate */
		getTravelsFromAGate: Gate >< TravelList -~-> Travel-set
		getTravelsFromAGate (g, trlist) as res
		post ((all tr: Travel :- tr isin trlist /\ getTravelGate(tr) = g => tr isin res)
				/\ ~(exists tr: Travel :- tr isin res /\ tr ~isin trlist)),

		/* get full info of a travel from a station to a station */
		getTravelInfo: Start >< Destination >< TravelList -~-> Travel-set
		getTravelInfo(st, des, trlist) as res
		post ((all tr: Travel :- tr isin trlist /\ getTravelStart(tr) = st /\ getTravelDestination(tr) = des => tr isin trlist)
				/\ ~(exists tr: Travel :- tr isin res /\ tr ~isin trlist)), 

		/* ********************************************************************************** */
		/*                         replace a travel with new info							  */
		/* replace start station */
		replaceStart: Travel >< Start >< TravelList -~-> TravelList
		replaceStart(tr, newStart, trlist) as res
		post let x = newTravelStart(tr, newStart) in 
			(tr ~isin res /\ (x isin res) /\ ((res \ {x}) << trlist))
			end
		pre tr isin trlist,

		/* replace destination station */
		replaceDestination: Travel >< Destination >< TravelList -~-> TravelList
		replaceDestination(tr, newDes, trlist) as res
		post let x = newTravelDestination(tr, newDes) in
			 (tr ~isin res /\ ( x isin res) /\ res \ {x} << trlist)
			 end
		pre tr isin trlist,

		/* replace gate */
		replaceGate: Travel >< Gate >< TravelList -~-> TravelList
		replaceGate(tr, newGate, trlist) as res
		post let x = newTravelGate(tr, newGate) in
			(tr ~isin res /\ (x isin res) /\ res \ {x} << trlist)
			end
		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) as res
		post let x = newTravelBoardingTime(tr, newBT) in
			(tr ~isin res /\ x isin res /\ res \ {x} << trlist)
			end
		pre tr isin trlist /\ isTravelCorrect(newTravelBoardingTime(tr, newBT), trlist \ {tr}),

		/* replace departure time */
		replaceDepartureTime: Travel >< Time >< TravelList -~-> TravelList
		replaceDepartureTime(tr, newDT, trlist) as res
		post let x = newTravelDepartureTime(tr, newDT) in
				((x isin res) /\ res \ {x} << trlist)
			end
		pre tr isin trlist /\ isTravelCorrect(newTravelDepartureTime(tr, newDT), trlist \ {tr}),

		/* replace entirely a travel */
		replaceTravel: Travel >< Travel >< TravelList -~-> TravelList
		replaceTravel(tr, newTravel, trlist) as res
		post (tr ~isin res /\ newTravel isin res /\ res \ {newTravel} << trlist)
		pre tr isin trlist /\ newTravel ~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) as res
		post (res \ trlist = {tr})
		pre tr ~isin trlist /\ isTravelCorrect(tr, trlist),

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