----------------------------- MODULE IdentityMC -----------------------------
EXTENDS ObjectIdentity
CONSTANTS MaxOccurrence, ImplicitFollow
ASSUME MaxOccurrence \in 3..5 /\ ImplicitFollow \in BOOLEAN
VARIABLE state
Init == state = InitialIdentity

MoveItem ==
    \E id \in DOMAIN state.live, area \in Areas, position \in Positions, hidden \in BOOLEAN :
        /\ state.live[id].physical = "item-a"
        /\ (hidden => area = "Private")
        /\ (~NeedsRenewal(state, id, area, hidden) \/ state.next <= MaxOccurrence)
        /\ LET moved == RelocateObject(state, id, area, position, hidden)
           IN state' = IF ImplicitFollow /\ moved.renewed /\ state.reference = id
                       THEN [moved.state EXCEPT !.reference = moved.successor]
                       ELSE moved.state
ExplicitRebind ==
    /\ CanFollowExplicitSuccessor(state)
    /\ state' = FollowExplicitSuccessor(state)
Next == MoveItem \/ ExplicitRebind
Spec == Init /\ [][Next]_state

TypeOK == IdentityType(state, MaxOccurrence)
LivePastSeparated == DOMAIN state.live \cap DOMAIN state.past = {}
FreshAllocation == DOMAIN state.live \cup DOMAIN state.past = 1..(state.next - 1)
UniquePhysicalItems == PhysicalUniqueness(state)
StationaryObjectFrame == state.live[2] = StationaryRow
NoImplicitRetarget == state.reference = state.explicitLineage[Len(state.explicitLineage)]
RenewalClearsMarks == \A id \in DOMAIN state.live : id > 2 => state.live[id].marks = {}
RetiredReferenceIsNotLive ==
    state.reference \in DOMAIN state.past => ResolveReference(state, state.reference) = "NoLiveObject"
HistoryStep ==
    /\ DOMAIN state.past \subseteq DOMAIN state'.past
    /\ \A id \in DOMAIN state.past : state'.past[id] = state.past[id]
StableHistory == [][HistoryStep]_state

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