2026-07-11 18:54:23 +09:00
|
|
|
CONSTANTS
|
|
|
|
|
G1 = g1
|
|
|
|
|
G2 = g2
|
2026-07-21 23:46:54 +09:00
|
|
|
P1 = p1
|
|
|
|
|
P2 = p2
|
2026-07-22 00:58:23 +09:00
|
|
|
A1 = incarnation1
|
|
|
|
|
A2 = incarnation2
|
2026-07-11 18:54:23 +09:00
|
|
|
NoArtifact = noArtifact
|
|
|
|
|
Generations <- GenerationsFixture
|
2026-07-21 23:46:54 +09:00
|
|
|
Preparations <- PreparationsFixture
|
2026-07-22 00:58:23 +09:00
|
|
|
Artifact = artifact
|
2026-07-11 18:54:23 +09:00
|
|
|
|
|
|
|
|
SPECIFICATION Spec
|
|
|
|
|
CHECK_DEADLOCK FALSE
|
|
|
|
|
|
|
|
|
|
INVARIANTS
|
|
|
|
|
TypeOK
|
2026-07-21 23:46:54 +09:00
|
|
|
PrepareOwnershipConsistent
|
2026-07-22 00:58:23 +09:00
|
|
|
ArtifactIncarnationConsistent
|
|
|
|
|
SelectionBindingConsistent
|
2026-07-21 23:46:54 +09:00
|
|
|
LiveOwnedStageNotRecoverable
|
|
|
|
|
LostOwnedStageRecoverable
|
|
|
|
|
LostIntentRecoverable
|
|
|
|
|
PublishedOwnedStageReusable
|
2026-07-11 18:54:23 +09:00
|
|
|
LeaseBindingConsistent
|
|
|
|
|
MountedGenerationLeased
|
|
|
|
|
LeasedArtifactPublished
|
|
|
|
|
GCExcludesLeases
|
2026-07-22 00:58:23 +09:00
|
|
|
GCExcludesSelections
|
|
|
|
|
SelectedArtifactStable
|
2026-07-11 18:54:23 +09:00
|
|
|
ReplacementOnlyDuringGC
|
|
|
|
|
ForeignStagePreserved
|
