--------------------------- MODULE ObjectIdentity ---------------------------
EXTENDS Naturals, FiniteSets, Sequences

(* Original finite teaching model. Physical identity persists; an occurrence
   identifier is retired on an area change or an explicitly hidden move.
   This schema has no hosts, counters, controllers or information projections. *)

PhysicalItems == {"item-a", "item-b"}
Areas == {"Display", "Private"}
Positions == {1, 2}
Marks == {"UseBound"}
EmptyMap == [key \in {} |-> key]
Without(mapping, keys) == [key \in DOMAIN mapping \ keys |-> mapping[key]]
Put(mapping, key, value) ==
    [index \in DOMAIN mapping \cup {key} |-> IF index = key THEN value ELSE mapping[index]]
ObjectRow(physical, area, position, marks) ==
    [physical |-> physical, area |-> area, position |-> position, marks |-> marks]
FirstRow == ObjectRow("item-a", "Display", 1, {"UseBound"})
StationaryRow == ObjectRow("item-b", "Display", 2, {})
InitialIdentity ==
    [live |-> [id \in {1, 2} |-> IF id = 1 THEN FirstRow ELSE StationaryRow],
     past |-> EmptyMap, next |-> 3, successors |-> EmptyMap,
     reference |-> 1, explicitLineage |-> <<1>>]

LiveOccurrence(before, id) == id \in DOMAIN before.live
NeedsRenewal(before, id, area, hidden) == before.live[id].area # area \/ hidden
ResolveReference(before, id) ==
    IF LiveOccurrence(before, id) THEN before.live[id] ELSE "NoLiveObject"

RelocateObject(before, id, area, position, hidden) ==
    LET old == before.live[id]
        renew == NeedsRenewal(before, id, area, hidden)
        successor == IF renew THEN before.next ELSE id
        row == [old EXCEPT !.area = area, !.position = position,
                          !.marks = IF renew THEN {} ELSE @]
        after == IF renew THEN
            [before EXCEPT !.live = Put(Without(@, {id}), successor, row),
                           !.past = Put(@, id, old), !.next = @ + 1,
                           !.successors = Put(@, id, successor)]
          ELSE [before EXCEPT !.live[id] = row]
    IN [state |-> after, successor |-> successor, renewed |-> renew]

CanFollowExplicitSuccessor(before) ==
    /\ before.reference \in DOMAIN before.successors
    /\ before.successors[before.reference] \in DOMAIN before.live
FollowExplicitSuccessor(before) ==
    LET successor == before.successors[before.reference]
    IN [before EXCEPT !.reference = successor,
                      !.explicitLineage = Append(@, successor)]

IdentityType(before, maximum) ==
    /\ before.next \in 3..(maximum + 1)
    /\ DOMAIN before.live \subseteq 1..maximum
    /\ DOMAIN before.past \subseteq 1..maximum
    /\ \A id \in DOMAIN before.live : before.live[id] \in
           [physical : PhysicalItems, area : Areas, position : Positions, marks : SUBSET Marks]
    /\ \A id \in DOMAIN before.past : before.past[id] \in
           [physical : PhysicalItems, area : Areas, position : Positions, marks : SUBSET Marks]
    /\ DOMAIN before.successors \subseteq DOMAIN before.past
    /\ \A id \in DOMAIN before.successors : before.successors[id] \in 1..maximum
    /\ before.reference \in 1..maximum
    /\ before.explicitLineage \in Seq(1..maximum)
    /\ Len(before.explicitLineage) \in 1..maximum

PhysicalUniqueness(before) ==
    \A left, right \in DOMAIN before.live :
        before.live[left].physical = before.live[right].physical => left = right

=============================================================================