SPECIFICATION Spec

CHECK_DEADLOCK TRUE

CONSTANTS
    Claims = {c1}
    Fences = {f1, f2}
    Workers = {w1, w2}
    Operations = {op1, op2}
    NoWorker = NoWorker
    NoOwner = NoOwner
    NoRequest = NoRequest
    NoResponse = NoResponse
    Accepted = Accepted
    Rejected = Rejected

INVARIANTS
    TypeOK
    LiveLeaseMatchesAuthority
    ExecutingIsCommitted
    AcceptedResponseIsExactReplay
    ConflictIsChangedRequest
    ReapedClaimHasNoActivationEffect
    ReapedCoordinationIsClean
    RecoveryOwnsInactiveClaim

PROPERTIES
    ActivationAppliesAtMostOnce
    OperationRequestIsImmutable