note
	description	: "Representation of a hall"
	author		: "Martino Trosi & Matteo Cortonesi"
	date		: "Spring 2009"
	reviewer	: "Mohammad Seyed Alavi"
	revision	: "1.0.1"

class
	HALL

feature  -- Status report

	judge_present: BOOLEAN
			-- Is judge present?

feature {JUDGE} -- Status report

	immigrants_ready: BOOLEAN
			-- Are immigrants ready?
		do
			Result := present_immigrant_count = ready_immigrant_count
		end

	all_immigrants_sworn: BOOLEAN
			-- Have all immigrants taken oath?
		do
			Result := sworn_immigrant_count = ready_immigrant_count
		end

	has_sworn_immigrants: BOOLEAN
			-- Have any immigrants present already taken oath?
		do
			Result := sworn_immigrant_count > 0
		end

feature -- Access

	expected_immigrant_count: INTEGER
			-- Total immigrants expected for today.

	present_immigrant_count: INTEGER
			-- Immigrants currently in hall for swearing in.

feature {JUDGE} -- Status setting

	set_judge_presence (a_bool: BOOLEAN)
			-- Set judge status.
		do
			judge_present := a_bool
		ensure
			judge_present_set: judge_present = a_bool
		end

	sit_judge
			-- Sit judge.
		do
			judge_ready := True
		ensure
			judge_ready: judge_ready
		end

	confirm
			-- Confirm immigrants.
		do
			judge_ready := False
			ready_immigrant_count := 0
		ensure
			not_judge_ready: not judge_ready
		end

feature {IMMIGRANT} -- Status report

	judge_ready: BOOLEAN
			-- Is judge ready?

feature -- Basic operations

	set_expected_immigrant_count (a_count: INTEGER)
			-- Set expected immigrant count to `a_count'.
		do
			expected_immigrant_count := a_count
		end

	enter_immigrant
			-- Enter immigrant.
		do
			present_immigrant_count := present_immigrant_count + 1
		ensure
			immigrants_incremented: present_immigrant_count = old present_immigrant_count + 1
		end

	check_in
			-- Check in.
		do
			ready_immigrant_count := ready_immigrant_count + 1
		ensure
			ready_immigrants_incremented: ready_immigrant_count = old ready_immigrant_count + 1
		end

	take_oath
			-- Take oath in front of Judge.
		do
			sworn_immigrant_count := sworn_immigrant_count + 1
		ensure
			sweared_immigrants_incremented: sworn_immigrant_count = old sworn_immigrant_count + 1
		end

	leave_immigrant
			-- Leave immigrant.
		do
			present_immigrant_count := present_immigrant_count - 1
			sworn_immigrant_count := sworn_immigrant_count - 1
		ensure
			immigrants_decremented: present_immigrant_count = old present_immigrant_count - 1
			sworn_immigrant_count = old sworn_immigrant_count - 1
		end

feature {NONE} -- Implementation

	ready_immigrant_count: INTEGER
			-- How many immigrants are checked in and ready for oath?

	sworn_immigrant_count: INTEGER
			-- How many immigrants have taken oath?

invariant

	ready_immigrants_bounds: ready_immigrant_count >= 0 and ready_immigrant_count <= present_immigrant_count
	immigrants_ready: immigrants_ready = (present_immigrant_count = ready_immigrant_count)
	judge_present: judge_present implies present_immigrant_count > 0

end