indexing
	description: "A simple token dispenser"
	author: "Bernd Schoeller and others"
	date: "$Date$"
	revision: "$Revision$"

class
	TOKEN_DISPENSER

create
	make

feature{NONE} -- Initialization

	make is
			-- Initialization
		do
			create issued_tokens.make
			generate_token
		end

feature -- Model

	model: MML_SET[TOKEN] is
			-- Set of tokens
		do
			create {MML_DEFAULT_SET[TOKEN]}Result.make_empty
			from issued_tokens.start until issued_tokens.off loop
				Result := Result.extended (issued_tokens.item)
				issued_tokens.forth
			end
		end

feature -- Access

	last_token: TOKEN
		-- Last token that was generated

feature -- Generation

	generate_token is
			-- Generate a new token.
		do
			create last_token
			issued_tokens.extend (last_token)
		ensure
			new_token: not (old model).contains (last_token)
			model_update: model |=| old model.extended (last_token)
		end

feature -- Status report

	has_generated (a_token: TOKEN): BOOLEAN is
			-- Was the token `a_token' generated by this dispenser?
		do
			Result := issued_tokens.has (a_token)
		ensure
			model_contract: Result = model.contains (a_token)
		end

feature{NONE} -- Implementation

	issued_tokens: LINKED_LIST [TOKEN]

invariant
	model_has_last_token: model.contains (last_token)
end