---- MODULE IdentityRenewalVariantMC ----
EXTENDS RuntimeChecksMC
DefectBodyIdentityRenewalVariant(t, id, zone, loc, hiddenDestination, actor) ==
    LET old == t.obj[id]
        renew == old.zone # zone
        objectiveAreaTransfer == old.zone \in ObjectiveZones /\ zone \in ObjectiveZones
        row == [old EXCEPT !.zone = zone, !.loc = loc,
                          !.placedBy = IF old.form = "Card" /\ old.zone # "Play" /\
                                          zone = "Play" THEN actor ELSE @,
                          !.host = IF old.zone = zone THEN @ ELSE NoHost,
                          !.face = RelocatedFace(old, zone),
                          !.deployed = IF old.zone = zone THEN @ ELSE FALSE,
                          !.activated = IF old.zone = zone THEN @ ELSE FALSE,
                          !.marks = IF renew THEN {} ELSE @]
        newId == IF renew THEN t.next ELSE id
        base == IF renew
                THEN [Remove(t, {id}) EXCEPT
                        !.obj = Put(@, newId, row), !.next = @ + 1]
                ELSE [t EXCEPT !.obj[id] = row]
        family == {id} \cup Desc(t, id)
        successors == [i \in family |->
                        t.next + Cardinality({j \in family : j < i})]
        objectiveCompletionRows == [i \in family |->
            [t.obj[i] EXCEPT !.zone = zone,
              !.face = RelocatedFace(t.obj[i], zone),
              !.loc = IF i = id THEN loc ELSE successors[t.obj[i].host],
              !.host = IF i = id THEN NoHost ELSE successors[t.obj[i].host],
              !.deployed = FALSE, !.activated = FALSE, !.marks = {}]]
        objectiveCompletionIds == {successors[i] : i \in family}
        objectiveCompletionObjects == [n \in objectiveCompletionIds |->
            objectiveCompletionRows[CHOOSE i \in family : successors[i] = n]]
        rebound == IF renew /\ objectiveAreaTransfer
                   THEN [Remove(t, family) EXCEPT
                     !.obj = [i \in DOMAIN @ \cup objectiveCompletionIds |->
                               IF i \in objectiveCompletionIds THEN objectiveCompletionObjects[i] ELSE @[i]],
                     !.next = @ + Cardinality(family),
                     !.pendingRetire = @ \cup
                          {successors[i] : i \in t.pendingRetire \cap family},
                     !.reveals = {v \in @ : v.object \notin family}]
                   ELSE base
        moved == IF renew /\ ~objectiveAreaTransfer
                 THEN [rebound EXCEPT !.pendingRetire = @ \cup Desc(t, id)]
                 ELSE rebound
    IN [state |-> [moved EXCEPT !.reveals =
                     {v \in @ : v.object # id \/
                       (~renew /\ old.zone = zone /\ old.loc = loc)}],
        successor |-> IF renew /\ objectiveAreaTransfer THEN successors[id] ELSE newId]
ControlFirstVariables == <<caseNo,pc,s>>
====