SPECIFICATION Spec

CONSTANTS
    Clients = {c1, c2}
    MaxVersion = 3

INVARIANT TypeOK
INVARIANT ActiveDeployed
INVARIANT PromptImpliesWaiting
INVARIANT WaitingNewer
INVARIANT AcceptedImpliesWaiting

PROPERTY Safety

CHECK_DEADLOCK FALSE