/*
 *	Author: Tran Duc Hieu
 *	Group:	422
 *	Email:	antiw@lvk.cs.msu.su
 *	Date:	11.Nov.2006
 */

scheme TravelAlgebraic=
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
		/* constants */
		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 TravelList							  */
		/* add a new travel to a travel list */
		/* Pre: travel is not in travelList */
		addTravel: Travel >< TravelList -~-> TravelList,

		/* delete a travel from a travel list */
		/* Pre: travel is in travelList */
		deleteTravel: Travel >< TravelList -~-> TravelList,


		/* ********************************************************************************** */
		/*                         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 departure time */
		getTravelDepartureTime: Travel -> Time,

		/* get ... */
		getTravelBoardingTime: Travel -> Time,

		/* conflict ? */
		isTravelCorrect: Travel >< TravelList -> Bool,


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

		/* ********************************************************************************** */
		/*                         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 */
		replaceBoardingTime: Travel >< Time >< TravelList -~-> TravelList,

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

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

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

		/* all travels from a station in a time range */
		getTravelsInDepartureTimeRangeFrom: Start >< TimeRange >< 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,

		/* get full info of a travel */
		getTravelInfo: Start >< Destination >< TravelList -~-> Travel-set
		/* When adding a new travel, the gate must be free in [boardingTime..departureTime] of the new travel */
		/*- added travel must be in travelist */
	axiom
		/* empty */
		emptyTravelList is {},
		exists x: StationName :- emptyStation is (x, <..>),

		/* getStationGateList & emptyStation */
		getStationGateList(emptyStation) is <..>,

		/* ********************************************************************************** */
		/*								 emptyTravelList									  */
		/* getTravelsFrom & emptyTravelList */
		all st: Start :- all timeRng: TimeRange:- getTravelsFrom(st, emptyTravelList) = {}
			/\ getTravelsInDepartureTimeRangeFrom(st, timeRng, emptyTravelList) = {},

		/* getTravelsTo & emptyTravelList */
		all des: Start :- all timeRng: TimeRange:- getTravelsTo(des, emptyTravelList) = {}
			/\ getTravelsInDepartureTimeRangeTo(des, timeRng, emptyTravelList) = {},

		/* isTravelCorrect & emptyTravelList */
		all tr: Travel :- isTravelCorrect(tr, emptyTravelList) = true,

		/* addTravel & emptyTravelList */
		all tr: Travel :- addTravel(tr, emptyTravelList) = {tr},

		/* ********************************************************************************** */
		/*								 time functions										  */
		/* compareTime */
		all x, y: Time :- compareTime(x, y) ~= 0 => compareTime(x, y) * compareTime(y, x) <0,
		all x, y: Time :- compareTime(x, y) = 0 => compareTime(y, x) = 0,

		/* ********************************************************************************** */
		/* 
		   concrete travels:
		   newTravelStart, newTravelDestination, newTravelGate, newTravelBoardingTime, newTravelDepartureTime
		 */
		all tr: Travel :- (newTravelStart(tr, getTravelStart(tr)) = tr
				/\ newTravelDestination(tr, getTravelDestination(tr)) = tr
				/\ newTravelGate(tr, getTravelGate(tr)) = tr
				/\ newTravelBoardingTime(tr, getTravelBoardingTime(tr)) = tr
				/\ newTravelDepartureTime(tr, getTravelDepartureTime(tr)) = tr),

		/* replaceXXX */
		all st: Start :- all des: Destination :- all gt: Gate :- all bT: Time :- all dT: Time
					  :- all trlist: TravelList :- trlist ~= emptyTravelList
			/\ replaceStart((st, des, gt, bT, dT), st, trlist) = trlist
			/\ replaceDestination((st, des, gt, bT, dT), des, trlist) = trlist
			/\ replaceGate((st, des, gt, bT, dT), gt, trlist) = trlist
			/\ replaceBoardingTime((st, des, gt, bT, dT), bT, trlist) = trlist
			/\ replaceDepartureTime((st, des, gt, bT, dT), dT, trlist) = trlist,

		/* getTravelsFrom & addTravel */
		all tr: Travel :- all trlist: TravelList :- 
			tr ~isin trlist /\ tr isin getTravelsFrom(getTravelStart(tr), addTravel(tr, trlist)),

		/* getTravelsFrom & replaceStart */
		all tr: Travel :- all st: Start :- all trlist : TravelList :-
			getTravelStart(tr) ~= st /\ tr isin trlist /\ tr isin getTravelsFrom(st, replaceStart(tr, st, trlist)),

		/* getTravelsTo & addTravel */
		all tr: Travel :- all trlist: TravelList :-
			tr ~isin trlist /\ tr isin getTravelsTo(getTravelDestination(tr), addTravel(tr, trlist)),

		/* getTravelsTo & replaceDestination */
		all tr: Travel :- all trlist: TravelList :- all des: Destination :-
			getTravelDestination(tr) ~= des /\ tr isin trlist /\ tr isin getTravelsTo(des, replaceDestination(tr, des, trlist)),

		/* addTravel & deleteTravel */
		all tr: Travel :- all trlist: TravelList :- 
			if (tr ~isin trlist) then
				deleteTravel(tr, addTravel(tr, trlist)) = trlist
			else
				addTravel(tr, deleteTravel(tr, trlist)) = trlist
			end,

		/* isTravelCorrect & deleteTravel */
		all tr: Travel :- all trlist: TravelList :-
			tr isin trlist /\ isTravelCorrect(tr, deleteTravel(tr, trlist)) = true
end