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

(***************************************************************************
Artifact-level refinement for prepared-lower publication, generation leases,
State Anchor use, exact-owned abandoned preparation recovery, and reclaim.
***************************************************************************)

CONSTANTS
    Generations,
    Artifact,
    NoArtifact,
    G1,
    G2,
    A1

ASSUME
    /\ Generations = {G1, G2}
    /\ G1 # G2
    /\ Artifact = A1
    /\ NoArtifact # Artifact

ArtifactStates == {"Absent", "Published"}
StageStates == {"Absent", "Owned", "Foreign"}
GenerationsFixture == {G1, G2}

VARIABLES
    artifactState,
    stageState,
    prepareIntent,
    leases,
    mounts,
    artifactBinding,
    gcRequested,
    replacementPresent,
    foreignObserved

vars == <<
    artifactState,
    stageState,
    prepareIntent,
    leases,
    mounts,
    artifactBinding,
    gcRequested,
    replacementPresent,
    foreignObserved
>>

Init ==
    /\ artifactState = "Absent"
    /\ stageState = "Absent"
    /\ prepareIntent = FALSE
    /\ leases = {}
    /\ mounts = {}
    /\ artifactBinding = [g \in Generations |-> NoArtifact]
    /\ gcRequested = FALSE
    /\ replacementPresent = FALSE
    /\ foreignObserved = FALSE

BeginPrepare ==
    /\ artifactState = "Absent"
    /\ stageState = "Absent"
    /\ ~prepareIntent
    /\ prepareIntent' = TRUE
    /\ UNCHANGED <<artifactState, stageState, leases, mounts,
        artifactBinding, gcRequested, replacementPresent, foreignObserved>>

CreateOwnedStage ==
    /\ artifactState = "Absent"
    /\ stageState = "Absent"
    /\ prepareIntent
    /\ stageState' = "Owned"
    /\ UNCHANGED <<artifactState, prepareIntent, leases, mounts,
        artifactBinding, gcRequested, replacementPresent, foreignObserved>>

PublishArtifact ==
    /\ artifactState = "Absent"
    /\ stageState = "Owned"
    /\ prepareIntent
    /\ artifactState' = "Published"
    /\ stageState' = "Absent"
    /\ prepareIntent' = FALSE
    /\ UNCHANGED <<leases, mounts, artifactBinding, gcRequested,
        replacementPresent, foreignObserved>>

RecoverOwnedStage ==
    /\ artifactState = "Absent"
    /\ stageState = "Owned"
    /\ prepareIntent
    /\ stageState' = "Absent"
    /\ prepareIntent' = FALSE
    /\ UNCHANGED <<artifactState, leases, mounts, artifactBinding,
        gcRequested, replacementPresent, foreignObserved>>

ObserveForeignStage ==
    /\ artifactState = "Absent"
    /\ stageState = "Absent"
    /\ ~prepareIntent
    /\ stageState' = "Foreign"
    /\ foreignObserved' = TRUE
    /\ UNCHANGED <<artifactState, prepareIntent, leases, mounts,
        artifactBinding, gcRequested, replacementPresent>>

RefuseForeignStage ==
    /\ stageState = "Foreign"
    /\ UNCHANGED vars

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

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

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

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

RequestGC ==
    /\ artifactState = "Published"
    /\ leases = {}
    /\ ~gcRequested
    /\ gcRequested' = TRUE
    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts,
        artifactBinding, replacementPresent, foreignObserved>>

PublishReplacementDuringGC ==
    /\ artifactState = "Published"
    /\ gcRequested
    /\ ~replacementPresent
    /\ replacementPresent' = TRUE
    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts,
        artifactBinding, gcRequested, foreignObserved>>

ReclaimArtifact ==
    /\ artifactState = "Published"
    /\ gcRequested
    /\ leases = {}
    /\ mounts = {}
    /\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
    /\ gcRequested' = FALSE
    /\ replacementPresent' = FALSE
    /\ UNCHANGED <<stageState, prepareIntent, leases, mounts,
        artifactBinding, foreignObserved>>

Next ==
    \/ BeginPrepare
    \/ CreateOwnedStage
    \/ PublishArtifact
    \/ RecoverOwnedStage
    \/ ObserveForeignStage
    \/ RefuseForeignStage
    \/ (\E g \in Generations : AcquireLease(g))
    \/ (\E g \in Generations : MountStateAnchor(g))
    \/ (\E g \in Generations : UnmountStateAnchor(g))
    \/ (\E g \in Generations : ReleaseLease(g))
    \/ RequestGC
    \/ PublishReplacementDuringGC
    \/ ReclaimArtifact

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

TypeOK ==
    /\ artifactState \in ArtifactStates
    /\ stageState \in StageStates
    /\ prepareIntent \in BOOLEAN
    /\ leases \subseteq Generations
    /\ mounts \subseteq Generations
    /\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
    /\ gcRequested \in BOOLEAN
    /\ replacementPresent \in BOOLEAN
    /\ foreignObserved \in BOOLEAN

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"

GCExcludesLeases ==
    gcRequested =>
        /\ artifactState = "Published"
        /\ leases = {}
        /\ mounts = {}

ReplacementOnlyDuringGC ==
    replacementPresent => gcRequested

ForeignStagePreserved ==
    foreignObserved => stageState = "Foreign"

OwnedStageRequiresIntent ==
    stageState = "Owned" => prepareIntent

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