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