-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- File: times.d
-- Author: Arthur P. Goldberg

Times:  USING (StdEnv)

DEFINITIONS

	-- For procedures that get 1 Time_Set argument
	Time_Set_INTFACE: callmessage (
		Time_Set : Time_Set)
	constant ( Time_Set )
	exit {full};

	Time_Set_INTFACE_Receiver : inport of Time_Set_INTFACE
		{full( Time_Set )};
	Time_Set_INTFACE_Caller : outport of Time_Set_INTFACE_Receiver;


	-- For procedures that get 1 Time_Value argument
	Time_Value_INTFACE: callmessage (
		Time_Value : Time_Value)
	constant ( Time_Value )
	exit {full};

	Time_Value_INTFACE_Receiver : inport of Time_Value_INTFACE
		{full( Time_Value )};


	-- For procedures that print a Time_Value
	Time_Value_Print_INTFACE: callmessage (
		StdEnv :  StdEnv,
		Time_Value : Time_Value)
	constant ( StdEnv, Time_Value )
	exit {full};

	Time_Value_Print_INTFACE_Receiver : inport of Time_Value_Print_INTFACE
		{init( StdEnv ), full( Time_Value )};
	Time_Value_Print_INTFACE_Caller : 
		outport of Time_Value_Print_INTFACE_Receiver;


	-- For procedures that print a Time_Range
	Time_Range_Print_INTFACE: callmessage (
		StdEnv :  StdEnv,
		Time_Range : Time_Range)
	constant ( StdEnv, Time_Range )
	exit {full};

	Time_Range_Print_INTFACE_Receiver : inport of Time_Range_Print_INTFACE
		{init( StdEnv ), full( Time_Range )};
	Time_Range_Print_INTFACE_Caller : 
		outport of Time_Range_Print_INTFACE_Receiver;


	-- For procedures that print a Time_Set
	Time_Set_Print_INTFACE: callmessage (
		StdEnv :  StdEnv,
		Time_Set : Time_Set)
	constant ( StdEnv, Time_Set )
	exit {full};

	Time_Set_Print_INTFACE_Receiver : inport of Time_Set_Print_INTFACE
		{init( StdEnv ), full( Time_Set )};
	Time_Set_Print_INTFACE_Caller : 
		outport of Time_Set_Print_INTFACE_Receiver;


	-- For procedures of 2 Time_Value arguments that return a boolean
	Time_Value_Call2_Return_Boolean_INTFACE: callmessage (
		Input_Time_Value_1 : Time_Value,
		Input_Time_Value_2 : Time_Value,
		Boolean_Return : Boolean
	)
	constant ( Input_Time_Value_1, Input_Time_Value_2 )
	exit {full};

	Time_Value_Call2_Return_Boolean_INTFACE_Receiver : 
		inport of Time_Value_Call2_Return_Boolean_INTFACE
		{full( Input_Time_Value_1), full( Input_Time_Value_2 )};
	Time_Value_Call2_Return_Boolean_INTFACE_Caller : 
		outport of Time_Value_Call2_Return_Boolean_INTFACE_Receiver;


	-- For procedures of 2 Time_Value arguments that return 1 Time_Value
	Time_Value_Call2_Return1_INTFACE: callmessage (
		Input_Time_Value_1 : Time_Value,
		Input_Time_Value_2 : Time_Value,
		Output_Time_Value : Time_Value
	)
	constant ( Input_Time_Value_1, Input_Time_Value_2 )
	exit {full};

	Time_Value_Call2_Return1_INTFACE_Receiver : 
		inport of Time_Value_Call2_Return1_INTFACE
		{full( Input_Time_Value_1), full( Input_Time_Value_2 )};
	Time_Value_Call2_Return1_INTFACE_Caller : 
		outport of Time_Value_Call2_Return1_INTFACE_Receiver;


	-- For procedures that take 2 Time_Ranges and make 2 Time_Ranges,
	-- such as difference_time_ranges, intersect_time_ranges, and
	-- union_time_ranges.
	Time_Range_In2_Out2_INTFACE: callmessage (
		Input_Time_Range_1 : Time_Range,
		Input_Time_Range_2 : Time_Range,
		Output_Time_Range_1 : Time_Range,
		Output_Time_Range_2 : Time_Range
	)
	constant ( Input_Time_Range_1, Input_Time_Range_2 )
	exit {full};

	Time_Range_In2_Out2_Procedure_Receiver : 
		inport of Time_Range_In2_Out2_INTFACE
		{full( Input_Time_Range_1 ), full( Input_Time_Range_2 )};
	Time_Range_In2_Out2_Procedure_Caller : 
		outport of Time_Range_In2_Out2_Procedure_Receiver;


	-- For procedures that take 2 Time_Sets and make 1
	-- such as difference_time_sets, intersect_time_sets, and
	-- union_time_sets.
	Time_Set_In2_Out1_INTFACE: callmessage (
		Input_Time_Set_1 : Time_Set,
		Input_Time_Set_2 : Time_Set,
		Output_Time_Set : Time_Set
	)
	constant ( Input_Time_Set_1, Input_Time_Set_2 )
	exit {full};

	Time_Set_In2_Out1_Procedure_Receiver : 
		inport of Time_Set_In2_Out1_INTFACE
		{ full( Input_Time_Set_1 ), full( Input_Time_Set_2 )};
	Time_Set_In2_Out1_Procedure_Caller : 
		outport of Time_Set_In2_Out1_Procedure_Receiver;


	-- For procedures that take 1 Time_Set and make 1
	-- primarily not_time_set
	Time_Set_In1_Out1_INTFACE: callmessage (
		Input_Time_Set : Time_Set,
		Output_Time_Set : Time_Set
	)
	constant ( Input_Time_Set )
	exit {full};

	Time_Set_In1_Out1_Procedure_Receiver : 
		inport of Time_Set_In1_Out1_INTFACE { full( Input_Time_Set )};
	Time_Set_In1_Out1_Procedure_Caller : 
		outport of Time_Set_In1_Out1_Procedure_Receiver;

	-- For procedures that take 1 Time_Set and 1 Time_Range 
	-- primarily, insert_time_range_in_time_set
	Ins_TR_In_TS_INTFACE: callmessage (
		Input_Time_Range : Time_Range,
		IO_Time_Set : Time_Set
	)
	constant ( Input_Time_Range )
	exit {full};

	Ins_TR_In_TS_Procedure_Receiver : 
		inport of Ins_TR_In_TS_INTFACE
		{ full( IO_Time_Set ), full( Input_Time_Range )};
	Ins_TR_In_TS_Procedure_Caller : 
		outport of Ins_TR_In_TS_Procedure_Receiver;


-- Want the invariant that for all positions of elements e 
-- (0 <= e < sizeof(the Time_Set)) in a Time_Set
-- End_Time[e] < Begin_Time[e+1], where, by definition, 
-- End_Time[ -1 ] < Neg_Inf and Pos_Inf < Begin_Time[sizeof(the Time_Set)].
-- Idea: it might be worthwhile keeping such elements in each table.
	Time_Set: ordered table of Time_Range { full };

-- Want the invariant that Begin_Time <= End_Time for all
-- full Time_Ranges
	Time_Range: record (
		Begin_Time: Time_Value,
		End_Time: Time_Value );

	Time_Value: variant of Time_Value_Case (
		'An_Infinity' -> The_Infinity: Infinities { full },
		'Actual' -> The_Actual_Time: integer { full } );

	Infinities: enumeration (
		'Pos_Inf', 'Neg_Inf' );

	Time_Value_Case: enumeration (
		'An_Infinity', 'Actual' );

end DEFINITIONS
