SPECIFICATION Spec
CONSTANTS
MaxEpoch = 2
MaxRetries = 2
Tagged = TRUE
Safe = TRUE
AllowRemoval = TRUE
AllowFailure = TRUE
AllowRetry = TRUE
RetryStageSet = {"prepare", "promotion", "cleanup"}
INVARIANTS TypeOK PromotionRequiresAcceptance DeclaredPromotionRetained DeclaredCandidateRetained CleanupObservedMeansGone RetryPreservesTagIdentity RetryAcknowledgedAfterCreation CleanupExcludesCopy
CHECK_DEADLOCK FALSE