SPECIFICATION Spec

CONSTANTS
    Replicas = {r0, r1, r2}
    Coordinator = r0
    Keys = {k1}
    MaxWrites = 2
    MaxEvicts = 2
    NoVal = NoVal

INVARIANT TypeOK
INVARIANT EpochVerUnique
INVARIANT AckedImpliesHeldUnlessDoomed
INVARIANT CoordinatorHoldsOwnCommits
INVARIANT EpochAgreement

PROPERTY NoServedRegression

CHECK_DEADLOCK FALSE