------------------------- MODULE PreparedLower -------------------------
EXTENDS FiniteSets, TLC

(***************************************************************************
Artifact-level refinement for concurrent prepared-lower publication,
materializer-loss recovery, generation leases, State Anchor use, and reclaim.
***************************************************************************)

CONSTANTS
    Generations,
    Preparations,
    Artifact,
    NoArtifact,
    G1,
    G2,
    P1,
    P2,
    A1,
    A2

ASSUME
    /\ Generations = {G1, G2}
    /\ G1 # G2
    /\ Preparations = {P1, P2}
    /\ P1 # P2
    /\ NoArtifact # Artifact
    /\ A1 # A2
    /\ NoArtifact \notin {A1, A2}
    /\ Artifact \notin {A1, A2}

ArtifactStates == {"Absent", "Published"}
ArtifactIncarnations == {A1, A2}
StageStates == {"Absent", "Owned", "Foreign"}
MaterializerStates == {"Absent", "Live", "Lost"}
GenerationsFixture == {G1, G2}
PreparationsFixture == {P1, P2}

VARIABLES
    artifactState,
    artifactIncarnation,
    stageState,
    prepareIntent,
    materializerState,
    leases,
    selectionBinding,
    mounts,
    artifactBinding,
    gcObservation,
    replacementPresent,
    foreignObserved

FreshArtifactIncarnations ==
    ArtifactIncarnations \ {gcObservation[g] : g \in Generations}

vars == <<
    artifactState,
    artifactIncarnation,
    stageState,
    prepareIntent,
    materializerState,
    leases,
    selectionBinding,
    mounts,
    artifactBinding,
    gcObservation,
    replacementPresent,
    foreignObserved
>>

Init ==
    /\ artifactState = "Absent"
    /\ artifactIncarnation = NoArtifact
    /\ stageState = [p \in Preparations |-> "Absent"]
    /\ prepareIntent = [p \in Preparations |-> FALSE]
    /\ materializerState = [p \in Preparations |-> "Absent"]
    /\ leases = {}
    /\ selectionBinding = [g \in Generations |-> NoArtifact]
    /\ mounts = {}
    /\ artifactBinding = [g \in Generations |-> NoArtifact]
    /\ gcObservation = [g \in Generations |-> NoArtifact]
    /\ replacementPresent = FALSE
    /\ foreignObserved = FALSE

BeginPrepare(p) ==
    /\ artifactState = "Absent"
    /\ stageState[p] = "Absent"
    /\ ~prepareIntent[p]
    /\ materializerState[p] = "Absent"
    /\ prepareIntent' = [prepareIntent EXCEPT ![p] = TRUE]
    /\ materializerState' = [materializerState EXCEPT ![p] = "Live"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
        selectionBinding, mounts, artifactBinding, gcObservation,
        replacementPresent, foreignObserved>>

CreateOwnedStage(p) ==
    /\ stageState[p] = "Absent"
    /\ prepareIntent[p]
    /\ materializerState[p] = "Live"
    /\ stageState' = [stageState EXCEPT ![p] = "Owned"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
        materializerState, leases, selectionBinding, mounts, artifactBinding,
        gcObservation, replacementPresent, foreignObserved>>

LoseMaterializer(p) ==
    /\ prepareIntent[p]
    /\ materializerState[p] = "Live"
    /\ materializerState' = [materializerState EXCEPT ![p] = "Lost"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, leases, selectionBinding, mounts, artifactBinding,
        gcObservation, replacementPresent, foreignObserved>>

PublishArtifact(p) ==
    /\ artifactState = "Absent"
    /\ FreshArtifactIncarnations # {}
    /\ stageState[p] = "Owned"
    /\ prepareIntent[p]
    /\ materializerState[p] = "Live"
    /\ artifactState' = "Published"
    /\ artifactIncarnation' \in FreshArtifactIncarnations
    /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
    /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
    /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
    /\ UNCHANGED <<leases, selectionBinding, mounts, artifactBinding,
        gcObservation, replacementPresent, foreignObserved>>

ReusePublishedArtifact(p) ==
    /\ artifactState = "Published"
    /\ stageState[p] = "Owned"
    /\ prepareIntent[p]
    /\ materializerState[p] = "Live"
    /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
    /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
    /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, leases,
        selectionBinding, mounts, artifactBinding, gcObservation,
        replacementPresent, foreignObserved>>

RecoverUnmaterializedIntent(p) ==
    /\ stageState[p] = "Absent"
    /\ prepareIntent[p]
    /\ materializerState[p] = "Lost"
    /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
    /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
        selectionBinding, mounts, artifactBinding, gcObservation,
        replacementPresent, foreignObserved>>

RecoverOwnedStage(p) ==
    /\ stageState[p] = "Owned"
    /\ prepareIntent[p]
    /\ materializerState[p] = "Lost"
    /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
    /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
    /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
    /\ UNCHANGED <<artifactState, artifactIncarnation, leases,
        selectionBinding, mounts, artifactBinding, gcObservation,
        replacementPresent, foreignObserved>>

ObserveForeignStage(p) ==
    /\ stageState[p] = "Absent"
    /\ ~prepareIntent[p]
    /\ materializerState[p] = "Absent"
    /\ stageState' = [stageState EXCEPT ![p] = "Foreign"]
    /\ foreignObserved' = TRUE
    /\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
        materializerState, leases, selectionBinding, mounts, artifactBinding,
        gcObservation, replacementPresent>>

RefuseForeignStage(p) ==
    /\ stageState[p] = "Foreign"
    /\ UNCHANGED vars

SelectPublishedArtifact(g) ==
    /\ artifactState = "Published"
    /\ g \notin leases
    /\ selectionBinding[g] = NoArtifact
    /\ selectionBinding' =
        [selectionBinding EXCEPT ![g] = artifactIncarnation]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, mounts, artifactBinding,
        gcObservation, replacementPresent, foreignObserved>>

ReleaseSelection(g) ==
    /\ selectionBinding[g] # NoArtifact
    /\ g \notin leases
    /\ selectionBinding' = [selectionBinding EXCEPT ![g] = NoArtifact]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, mounts, artifactBinding,
        gcObservation, replacementPresent, foreignObserved>>

AcquireLease(g) ==
    /\ artifactState = "Published"
    /\ g \notin leases
    /\ selectionBinding[g] = artifactIncarnation
    /\ leases' = leases \cup {g}
    /\ selectionBinding' = [selectionBinding EXCEPT ![g] = NoArtifact]
    /\ artifactBinding' = [artifactBinding EXCEPT ![g] = Artifact]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState, prepareIntent,
        materializerState, mounts, gcObservation, replacementPresent,
        foreignObserved>>

MountStateAnchor(g) ==
    /\ g \in leases
    /\ artifactBinding[g] = Artifact
    /\ g \notin mounts
    /\ mounts' = mounts \cup {g}
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, selectionBinding,
        artifactBinding, gcObservation, replacementPresent, foreignObserved>>

UnmountStateAnchor(g) ==
    /\ g \in mounts
    /\ mounts' = mounts \ {g}
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, selectionBinding,
        artifactBinding, gcObservation, replacementPresent, foreignObserved>>

ReleaseLease(g) ==
    /\ g \in leases
    /\ g \notin mounts
    /\ leases' = leases \ {g}
    /\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, selectionBinding, mounts,
        gcObservation, replacementPresent, foreignObserved>>

ObserveGCCandidate(g) ==
    /\ artifactState = "Published"
    /\ leases = {}
    /\ \A selected \in Generations :
        selectionBinding[selected] = NoArtifact
    /\ gcObservation[g] = NoArtifact
    /\ gcObservation' =
        [gcObservation EXCEPT ![g] = artifactIncarnation]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, selectionBinding, mounts,
        artifactBinding, replacementPresent, foreignObserved>>

PublishReplacementDuringGC ==
    /\ artifactState = "Published"
    /\ \E g \in Generations :
        gcObservation[g] = artifactIncarnation
    /\ (IF artifactIncarnation = A1 THEN A2 ELSE A1)
        \in FreshArtifactIncarnations
    /\ ~replacementPresent
    /\ replacementPresent' = TRUE
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, selectionBinding, mounts,
        artifactBinding, gcObservation, foreignObserved>>

ReclaimObservedArtifact(g) ==
    /\ artifactState = "Published"
    /\ gcObservation[g] = artifactIncarnation
    /\ leases = {}
    /\ \A selected \in Generations :
        selectionBinding[selected] = NoArtifact
    /\ mounts = {}
    /\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
    /\ artifactIncarnation' =
        IF replacementPresent
        THEN IF artifactIncarnation = A1 THEN A2 ELSE A1
        ELSE NoArtifact
    /\ gcObservation' =
        [gcObservation EXCEPT ![g] = NoArtifact]
    /\ replacementPresent' = FALSE
    /\ UNCHANGED <<stageState, prepareIntent, materializerState, leases,
        selectionBinding, mounts, artifactBinding, foreignObserved>>

ConvergeCompletedReclaim(g) ==
    /\ gcObservation[g] # NoArtifact
    /\ \/ artifactState = "Absent"
       \/ gcObservation[g] # artifactIncarnation
    /\ gcObservation' =
        [gcObservation EXCEPT ![g] = NoArtifact]
    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
        prepareIntent, materializerState, leases, selectionBinding, mounts,
        artifactBinding, replacementPresent, foreignObserved>>

Next ==
    \/ (\E p \in Preparations : BeginPrepare(p))
    \/ (\E p \in Preparations : CreateOwnedStage(p))
    \/ (\E p \in Preparations : LoseMaterializer(p))
    \/ (\E p \in Preparations : PublishArtifact(p))
    \/ (\E p \in Preparations : ReusePublishedArtifact(p))
    \/ (\E p \in Preparations : RecoverUnmaterializedIntent(p))
    \/ (\E p \in Preparations : RecoverOwnedStage(p))
    \/ (\E p \in Preparations : ObserveForeignStage(p))
    \/ (\E p \in Preparations : RefuseForeignStage(p))
    \/ (\E g \in Generations : SelectPublishedArtifact(g))
    \/ (\E g \in Generations : ReleaseSelection(g))
    \/ (\E g \in Generations : AcquireLease(g))
    \/ (\E g \in Generations : MountStateAnchor(g))
    \/ (\E g \in Generations : UnmountStateAnchor(g))
    \/ (\E g \in Generations : ReleaseLease(g))
    \/ (\E g \in Generations : ObserveGCCandidate(g))
    \/ PublishReplacementDuringGC
    \/ (\E g \in Generations : ReclaimObservedArtifact(g))
    \/ (\E g \in Generations : ConvergeCompletedReclaim(g))

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

TypeOK ==
    /\ artifactState \in ArtifactStates
    /\ artifactIncarnation \in ArtifactIncarnations \cup {NoArtifact}
    /\ stageState \in [Preparations -> StageStates]
    /\ prepareIntent \in [Preparations -> BOOLEAN]
    /\ materializerState \in [Preparations -> MaterializerStates]
    /\ leases \subseteq Generations
    /\ selectionBinding \in
        [Generations -> ArtifactIncarnations \cup {NoArtifact}]
    /\ mounts \subseteq Generations
    /\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
    /\ gcObservation \in
        [Generations -> ArtifactIncarnations \cup {NoArtifact}]
    /\ replacementPresent \in BOOLEAN
    /\ foreignObserved \in BOOLEAN

PrepareOwnershipConsistent ==
    \A p \in Preparations :
        /\ prepareIntent[p] <=> materializerState[p] # "Absent"
        /\ stageState[p] = "Owned" => prepareIntent[p]
        /\ stageState[p] = "Foreign" =>
            /\ ~prepareIntent[p]
            /\ materializerState[p] = "Absent"

ArtifactIncarnationConsistent ==
    (artifactState = "Absent") <=> (artifactIncarnation = NoArtifact)

SelectionBindingConsistent ==
    \A g \in Generations :
        selectionBinding[g] # NoArtifact =>
            /\ artifactState = "Published"
            /\ selectionBinding[g] = artifactIncarnation
            /\ g \notin leases

LiveOwnedStageNotRecoverable ==
    \A p \in Preparations :
        materializerState[p] = "Live" => ~ENABLED RecoverOwnedStage(p)

LostOwnedStageRecoverable ==
    \A p \in Preparations :
        /\ materializerState[p] = "Lost"
        /\ stageState[p] = "Owned"
        => ENABLED RecoverOwnedStage(p)

LostIntentRecoverable ==
    \A p \in Preparations :
        /\ materializerState[p] = "Lost"
        /\ stageState[p] = "Absent"
        => ENABLED RecoverUnmaterializedIntent(p)

PublishedOwnedStageReusable ==
    \A p \in Preparations :
        /\ artifactState = "Published"
        /\ materializerState[p] = "Live"
        /\ stageState[p] = "Owned"
        => ENABLED ReusePublishedArtifact(p)

LeaseBindingConsistent ==
    \A g \in Generations :
        (g \in leases) <=> (artifactBinding[g] = Artifact)

MountedGenerationLeased ==
    /\ mounts \subseteq leases
    /\ \A g \in mounts : artifactBinding[g] = Artifact

LeasedArtifactPublished ==
    leases # {} => artifactState = "Published"

GCReclaimExcludesLeases ==
    \A g \in Generations :
        ENABLED ReclaimObservedArtifact(g) =>
            /\ leases = {}
            /\ mounts = {}

GCReclaimExcludesSelections ==
    \A g \in Generations :
        ENABLED ReclaimObservedArtifact(g) =>
            \A selected \in Generations :
                selectionBinding[selected] = NoArtifact

SelectedArtifactStable ==
    \A g \in Generations :
        selectionBinding[g] # NoArtifact =>
            \A observer \in Generations :
                ~ENABLED ReclaimObservedArtifact(observer)

CompletedReclaimConverges ==
    \A g \in Generations :
        /\ gcObservation[g] # NoArtifact
        /\ \/ artifactState = "Absent"
           \/ gcObservation[g] # artifactIncarnation
        => /\ ENABLED ConvergeCompletedReclaim(g)
           /\ ~ENABLED ReclaimObservedArtifact(g)

ReplacementOnlyDuringGC ==
    replacementPresent =>
        \E g \in Generations :
            gcObservation[g] = artifactIncarnation

ForeignStagePreserved ==
    foreignObserved => \E p \in Preparations : stageState[p] = "Foreign"

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