SPECIFICATION SafetySpec

CHECK_DEADLOCK FALSE

CONSTANTS
    Jobs = {j1}
    Workers = {w1}
    InitialWorkers = {w1}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 1
    MaxProgress = 1
    LeaseLimit = 1
    ReservationLimit = 1
    LocalLimit = 1
    GlobalLimit = 1
    FaultsEnabled = FALSE
    FaultServices = {}
    MaxCoordLosses = 0
    MaxPartitions = 0
    MaxCredentialIntents = 2

INVARIANTS
    TypeOK
    CredentialLifecycleWellFormed
    NoOrphanSecrets