SPECIFICATION Spec

CONSTANTS
    Clients = {c1, c2}
    MaxVersion = 3

INVARIANT TypeOK
INVARIANT ActiveDeployed
INVARIANT WaitingNewer

PROPERTY Safety

CHECK_DEADLOCK FALSE