IdentityMC

Original bounded occurrence-renewal and explicit-reference teaching model; no full-source correspondence claim.

Package identity, input revision 1. Exact prepared source; CC0 1.0.

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

moved · operator

identity · input revision 1 · CC0 1.0

moved == RelocateObject(state, id, area, position, hidden)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, RelocateObject

ImplicitFollow · constant

identity · input revision 1 · CC0 1.0

ImplicitFollow

Exact module download · Source bundle and reproduction instructions

MaxOccurrence · constant

identity · input revision 1 · CC0 1.0

MaxOccurrence

Exact module download · Source bundle and reproduction instructions

ExplicitRebind · operator

identity · input revision 1 · CC0 1.0

ExplicitRebind ==
    /\ CanFollowExplicitSuccessor(state)
    /\ state' = FollowExplicitSuccessor(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, CanFollowExplicitSuccessor, FollowExplicitSuccessor

FreshAllocation · operator

identity · input revision 1 · CC0 1.0

FreshAllocation == DOMAIN state.live \cup DOMAIN state.past = 1..(state.next - 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

HistoryStep · operator

identity · input revision 1 · CC0 1.0

HistoryStep ==
    /\ DOMAIN state.past \subseteq DOMAIN state'.past
    /\ \A id \in DOMAIN state.past : state'.past[id] = state.past[id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

Init · operator

identity · input revision 1 · CC0 1.0

Init == state = InitialIdentity

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, InitialIdentity

LivePastSeparated · operator

identity · input revision 1 · CC0 1.0

LivePastSeparated == DOMAIN state.live \cap DOMAIN state.past = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

MoveItem · operator

identity · input revision 1 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved, ImplicitFollow, MaxOccurrence, state, Areas, NeedsRenewal, Positions

Next · operator

identity · input revision 1 · CC0 1.0

Next == MoveItem \/ ExplicitRebind

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExplicitRebind, MoveItem

NoImplicitRetarget · operator

identity · input revision 1 · CC0 1.0

NoImplicitRetarget == state.reference = state.explicitLineage[Len(state.explicitLineage)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

RenewalClearsMarks · operator

identity · input revision 1 · CC0 1.0

RenewalClearsMarks == \A id \in DOMAIN state.live : id > 2 => state.live[id].marks = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

RetiredReferenceIsNotLive · operator

identity · input revision 1 · CC0 1.0

RetiredReferenceIsNotLive ==
    state.reference \in DOMAIN state.past => ResolveReference(state, state.reference) = "NoLiveObject"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, ResolveReference

Spec · operator

identity · input revision 1 · CC0 1.0

Spec == Init /\ [][Next]_state

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init, Next, state

StableHistory · operator

identity · input revision 1 · CC0 1.0

StableHistory == [][HistoryStep]_state

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HistoryStep, state

StationaryObjectFrame · operator

identity · input revision 1 · CC0 1.0

StationaryObjectFrame == state.live[2] = StationaryRow

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, StationaryRow

TypeOK · operator

identity · input revision 1 · CC0 1.0

TypeOK == IdentityType(state, MaxOccurrence)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOccurrence, state, IdentityType

UniquePhysicalItems · operator

identity · input revision 1 · CC0 1.0

UniquePhysicalItems == PhysicalUniqueness(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, PhysicalUniqueness

state · variable

identity · input revision 1 · CC0 1.0

state

Exact module download · Source bundle and reproduction instructions