IdentityRenewalVariantMC

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 13 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

ControlFirstVariables · operator

reference-profile · input revision 2 · CC0 1.0

ControlFirstVariables == <<caseNo,pc,s>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, caseNo, pc

DefectBodyIdentityRenewalVariant · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Desc, NoHost, ObjectiveZones, Put, RelocatedFace, Remove