scheme TravelExplicit=
class
	type
		/* boarding gate */
		Gate = Int,
		BusStation = Gate-list,
		Start = BusStation,
		Destination = BusStation,

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

		TravelID = Int,
		Travel = Start >< Destination >< Gate >< BoardingTime >< DepartureTime,
		TravelList = Travel-list
	value
		/* ********************************************************************************** */
		/* add a new travel to a travel list */
		/* Pre: travel is not in travelList */
		addTravel: Travel >< TravelList -~-> TravelList
		addTravel(tr, trlist) is

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

		/* ********************************************************************************** */
		/* 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 to a station */
		getTravelsTo: Destination >< TravelList -~-> Travel-set,

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