note
	description: "[
			Helper ghost objects that prevent container items from unwanted modifications.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	status: ghost
	model: locked, equivalence
	manual_inv: true
	false_guards: true
	explicit: "all"

class
	V_LOCK [G -> ANY]

feature -- Access

	locked: MML_SET [G]
			-- All locked items (might be shared between multiple `observers').
		note
			guard: in_use_still_locked
			status: ghost
		attribute
			check is_executable: False then end
		end

	equivalence: MML_RELATION [G, G]
			-- Cache of object equality relation on items from `locked'.
		note
			guard: no_new_pairs
			status: ghost
		attribute
			check is_executable: False then end
		end

feature -- Basic operations

	lock (item: G)
			-- Add `item' and its subjects to `locked'.
		note
			status: setter
		require
			wrapped: is_wrapped
			item_wrapped: item.is_wrapped
			subjects_wrapped: ∀ s: item.subjects ¦ s.is_wrapped
			not_current: item /= Current and not item.subjects [Current]
		do
			unwrap
			add_equivalences (item)
			locked := locked & item
			set_owns (owns & item + item.subjects)
			wrap
		ensure
			locked_effect: locked = old locked & item
			owns_effect: owns = old owns & item + item.subjects
			observers_effect: observers = old observers
			wrapped: is_wrapped
			modify (Current)
			modify_field ("owner", [item, item.subjects, owns])
		end

	unlock (item: G)
			-- Remove `item' that is not in use and its subjects from `locked'.
		note
			status: setter
		require
			wrapped: is_wrapped
			item_locked: locked [item]
			not_in_use: ∀ o: observers ¦ attached {V_LOCKER [G]} o as c and then not c.locked [item]
			not_subject: ∀ o: locked ¦ not o.subjects [item] and o.subjects.is_disjoint (item.subjects)
		do
			unwrap
			locked := locked / item
			set_owns (owns / item - item.subjects)
			wrap
		ensure
			locked_effect: locked = old locked / item
			owns_effect: owns = old owns / item - item.subjects
			item_wrapped: item.is_wrapped
			wrapped: is_wrapped
			modify (Current)
			modify_field ("owner", [item, owns])
		end

	add_client (c: V_LOCKER [G])
			-- Add `c' to `observers'.
		require
			c_exists: c /= Void
			wrapped: is_wrapped
		do
			unwrap
			set_observers (observers & c)
			wrap
		ensure
			wrapped: is_wrapped
			observers_effect: observers = old observers & c
			modify_model ("observers", Current)
		end

feature -- Specification

	in_use_still_locked (new_locked: like locked; o: ANY): BOOLEAN
			-- All items that are in use by any of the `observers' are still in `new_locked'. (Update guard).
		note
			status: functional, nonvariant
		do
			Result := attached {V_LOCKER [G]} o as l and then
				∀ x: locked - new_locked ¦ not l.locked [x]
		end

	no_new_pairs (new_eq: like equivalence; o: ANY): BOOLEAN
			-- `new_eq' does not introduce any new pairs compared to `equivalence' on the elements of `locked'. (Update guard).
		note
			status: functional, nonvariant
		do
			Result := ∀ x: locked ¦ ∀ y: locked ¦
						not equivalence [x, y] implies not new_eq [x, y]
		end

	set_has (s: MML_SET [G]; v: G): BOOLEAN
			-- Does `s' contain an element equal to `v' under object equality?
		note
			status: functional, nonvariant, static
		require
			v_exists: v /= Void
			set_non_void: s.non_void
			reads (s, v)
		do
			Result := ∃ x: s ¦ v.is_model_equal (x)
		end

	set_item (s: MML_SET [G]; v: G): G
			-- Element of `s' that is equal to `v' under object equality.
		note
			status: nonvariant, static
			explicit: contracts
		require
			v_exists: v /= Void
			v_in_set: set_has (s, v)
			set_non_void: s.non_void
			reads (s, v)
		local
			s1: MML_SET [G]
		do
			from
				s1 := s
				Result := s1.any_item
			invariant
				s1 [Result]
				∃ x: s1 ¦ v.is_model_equal (x)
				s1 <= s
				decreases (s1)
			until
				Result.is_model_equal (v)
			loop
				s1 := s1 / Result
				check ∃ x: s1 ¦ v.is_model_equal (x) end
				Result := s1.any_item
			end
		ensure
			result_in_set: s [Result]
			equal_to_v: Result.is_model_equal (v)
		end

feature {NONE} -- Implementation

	add_equivalences (x: G)
			-- Add equivalences between `locked' and a new item `x' to `equivalence'.
		note
			status: setter
		require
			open: is_open
			x_wrapped: x.is_wrapped
			locked_wrapped: ∀ a: locked ¦ a.is_wrapped
			inv_holds: inv
			new_item: not locked [x]
		local
			s: like locked
			y: G
		do
			equivalence := equivalence.extended (x, x)
			from
				s := locked
			invariant
				s <= locked
				equivalence [x, x]
				∀ a: (locked - s) ¦ equivalence [x, a] = x.is_model_equal (a) and equivalence [a, x] = x.is_model_equal (a)
				inv
				decreases (s)
			until
				s.is_empty
			loop
				y := s.any_item
				if x.is_model_equal (y) then
					equivalence := equivalence.extended (x, y)
					equivalence := equivalence.extended (y, x)
				else
					equivalence := equivalence.removed (x, y)
					equivalence := equivalence.removed (y, x)
				end
				s := s / y
			end
		ensure
			still_holds: inv
			equivalences_added: ∀ a: locked & x ¦ equivalence [x, a] = x.is_model_equal (a) and equivalence [a, x] = x.is_model_equal (a)
			modify_field ("equivalence", Current)
		end

invariant
	locked_non_void: locked.non_void
	owns_definition: ∀ x: locked ¦ owns [x] and x.subjects <= owns
	equivalence_definition: ∀ x: locked ¦ ∀ y: locked ¦ equivalence [x, y] = x.is_model_equal (y)
	default_subjects: subjects ~ create {MML_SET [ANY]}
	observrs_are_lockers: ∀ o: observers ¦ attached {V_LOCKER [G]} o

note
	copyright: "Copyright (c) 1984-2021, 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