note description: "Philosoper that thinks and then eats using two assigned forks when they are not used by anybody." legal: "See notice at end of class."; status: "See notice at end of class."; date: "$Date$" revision: "$Revision$" class PHILOSOPHER inherit REPEATABLE rename repeat as live redefine act end create make feature -- Initialization make (philosopher: NATURAL; left, right: separate FORK; round_count: NATURAL) -- Initialize with ID of `philosopher', forks `left' and `right', and for `round_count' times to eat. require valid_id: philosopher >= 1 valid_times_to_eat: round_count >= 1 do id := philosopher left_fork := left right_fork := right times_to_eat := round_count ensure id_set: id = philosopher left_fork_set: left_fork = left right_fork_set: right_fork = right times_to_eat_set: times_to_eat = round_count end feature -- Access id: NATURAL -- Philosopher's id. feature -- Status report after: BOOLEAN -- do Result := times_to_eat = 0 end feature -- Measurement times_to_eat: NATURAL -- How many times does it remain for the philosopher to eat? feature -- Basic operations act -- do think eat (left_fork, right_fork) end forth -- do times_to_eat := times_to_eat - 1 end eat (left, right: separate FORK) -- Eat, having acquired `left' and `right' forks. do -- Take forks. left.pick (Current) right.pick (Current) -- Eat. delay (200) -- Put forks back. left.put (Current) right.put (Current) end think -- Think ... for a short time. do delay (400) end feature {NONE} -- Access left_fork: separate FORK -- Left fork used for eating. right_fork: separate FORK -- Right fork used for eating. feature {NONE} -- Timing delay (milliseconds: INTEGER_64) -- Delay execution by `milliseconds'. do (create {EXECUTION_ENVIRONMENT}).sleep (milliseconds * 1_000_000) end invariant valid_id: id >= 1 note copyright: "Copyright (c) 2012, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end