note
	description:

		"List of requests"

	copyright: "Copyright (c) 2005, Andreas Leitner and others"
	license: "Eiffel Forum License v2 (see forum.txt)"
	date: "$Date$"
	revision: "$Revision$"

class AUT_REQUEST_LIST

create

	make,
	make_default

feature {NONE} -- Initialization

	make (a_list: like list; a_first_index: like first_index; a_last_index: like last_index)
			-- Create new list.
		require
			a_list_not_void: a_list /= Void
			no_request_void: not a_list.has (Void)
			a_first_index_large_enough: a_first_index >= 1
			a_first_index_small_enough: a_first_index <= a_list.count
			a_last_index_large_enough: a_last_index >= 1
			a_last_index_small_enough: a_last_index <= a_list.count and a_last_index >= a_first_index
		do
			list := a_list
			first_index := a_first_index
			last_index := a_last_index
		ensure
			list_set: list = a_list
			first_index_set: first_index = a_first_index
			last_index_set: last_index = a_last_index
		end

	make_default (a_list: like list)
			-- Create new witness.
		do
			make (a_list, 1, a_list.count)
		end

feature -- Access

	count: INTEGER
			-- Number of requests
		do
			Result := last_index - first_index + 1
		ensure
			definition: Result = (last_index - first_index + 1)
		end

	item (an_index: INTEGER): AUT_REQUEST
			-- `an_index'-th request
		require
			an_index_large_enough: an_index >= 1
			an_index_small_enough: an_index <= count
		do
			Result := list.item (first_index + an_index - 1)
		ensure
			request_not_void: Result /= Void
			definition: Result = list.item (first_index + an_index - 1)
		end

	request_list: DS_LIST [AUT_REQUEST]
			-- List of all requests
		local
			arrayed_list: DS_ARRAYED_LIST [AUT_REQUEST]
			i: INTEGER
		do
			from
				create arrayed_list.make (count)
				i := 1
			until
				i > count
			loop
				arrayed_list.force_last (item (i))
				i := i + 1
			end
			Result := arrayed_list
		ensure
			request_list_not_void: Result /= Void
			no_request_void: not Result.has (Void)
			counts_match: count = Result.count
		end

	fresh_request_list: DS_LIST [AUT_REQUEST]
			-- Fresh (as in requests without responses) list of all requests
		local
			arrayed_list: DS_ARRAYED_LIST [AUT_REQUEST]
			i: INTEGER
		do
			from
				create arrayed_list.make (count)
				i := 1
			until
				i > count
			loop
				arrayed_list.force_last (item (i).fresh_twin)
				i := i + 1
			end
			Result := arrayed_list
		ensure
			request_list_not_void: Result /= Void
			no_request_void: not Result.has (Void)
			counts_match: count = Result.count
		end

	all_but_i_requests (i: INTEGER): DS_LIST [AUT_REQUEST]
			-- List of all requests except the `i'-th
		require
			i_big_enough: i >= 1
			i_small_enough: i <= count
		local
			arrayed_list: DS_ARRAYED_LIST [AUT_REQUEST]
			j: INTEGER
		do
			from
				create arrayed_list.make (count - 1)
				j := 1
			until
				j > count
			loop
				if i /= j then
					arrayed_list.force_last (item (j))
				end
				j := j + 1
			end
			Result := arrayed_list
		ensure
			request_list_not_void: Result /= Void
			no_request_void: not Result.has (Void)
			counts_match: count - 1= Result.count
		end

	all_but_i_requests_fresh (i: INTEGER): DS_LIST [AUT_REQUEST]
			-- Fresh (as in requests without responses) list of all requests except the `i'-th
		require
			i_big_enough: i >= 1
			i_small_enough: i <= count
		local
			arrayed_list: DS_ARRAYED_LIST [AUT_REQUEST]
			j: INTEGER
		do
			from
				create arrayed_list.make (count - 1)
				j := 1
			until
				j > count
			loop
				if i /= j then
					arrayed_list.force_last (item (j).fresh_twin)
				end
				j := j + 1
			end
			Result := arrayed_list
		ensure
			request_list_not_void: Result /= Void
			no_request_void: not Result.has (Void)
			counts_match: count - 1= Result.count
		end

feature {NONE} -- Implementation

	list: DS_INDEXABLE [AUT_REQUEST]
			-- Full list of requests

	first_index: INTEGER
			-- Index of first request of `history' that belong to this witness

	last_index: INTEGER
			-- Index of last request of `history' that belongs to this witness

invariant

	list_not_void: list /= Void
	no_request_void: not list.has (Void)
	first_index_large_enough: first_index >= 1
	first_index_small_enough: first_index <= list.count
	last_index_large_enough: last_index >= 1
	last_index_small_enough: last_index <= list.count and last_index >= first_index

end