CONSTANTS
    G1 = g1
    G2 = g2
    P1 = p1
    P2 = p2
    A1 = incarnation1
    A2 = incarnation2
    NoArtifact = noArtifact
    Generations <- GenerationsFixture
    Preparations <- PreparationsFixture
    Artifact = artifact

SPECIFICATION Spec
CHECK_DEADLOCK FALSE

INVARIANTS
    TypeOK
    PrepareOwnershipConsistent
    ArtifactIncarnationConsistent
    SelectionBindingConsistent
    LiveOwnedStageNotRecoverable
    LostOwnedStageRecoverable
    LostIntentRecoverable
    PublishedOwnedStageReusable
    LeaseBindingConsistent
    MountedGenerationLeased
    LeasedArtifactPublished
    GCReclaimExcludesLeases
    GCReclaimExcludesSelections
    SelectedArtifactStable
    CompletedReclaimConverges
    ReplacementOnlyDuringGC
    ForeignStagePreserved