SPECIFICATION Spec

CHECK_DEADLOCK TRUE

CONSTANTS
    Users = {u1, u2}
    OperationIds = {op1}
    EnabledKinds = {"put"}
    PersonalKeyNames = {personalKey}
    SharedKeys = {sharedKey}
    Contents = {content1}
    MaxObjectSize = 1
    PersonalLimit = 2
    SharedLimit = 2
    MaxPostgresLosses = 1
    MaxObjectStoreLosses = 1
    SharedPool = SharedPool
    NoObject = NoObject
    NoRecord = NoRecord
    NoOwner = NoOwner
    NoObservation = NoObservation

INVARIANTS
    TypeOK
    RecordIdentityConsistent
    PersonalRequestsUseOwnPool
    PersonalPoolsDisjoint
    FingerprintBindsRequest
    ReservationsConsistent
    LocksConsistent
    ActiveObjectConsistent
    ExternalStateConsistent
    UploadBodyConsistent
    QuotaReservationBound
    ObjectStateCovered
    ObjectQuotaBound
    AccountingAtQuiescence
    ObservationConsistent

PROPERTIES
    RecordsNeverForgotten
    RequestBindingsStable
    TerminalRecordsStable
    PostgresFailureFencesDurableState
    ObjectStoreFailureFencesObjects
    SettledEffectsDoNotMutate
    UnfinishedEventuallyTerminal
    LostUploadEventuallyTerminal