SPECIFICATION FairSpec

CHECK_DEADLOCK FALSE

CONSTANTS
    Replicas = {r1, r2}
    NoReplica = NoReplica
    AllowTakeover = FALSE
    AllowAmbiguousRelease = FALSE
    ObserverDestroysOwned = FALSE

INVARIANTS
    TypeOK
    ProviderRefreshSerialized
    CommitIsOwnerFenced
    ObserverPreservesOwnedRenewal

PROPERTIES
    TerminalSessionIsPermanent
    EventuallyTerminal