48 lines
1.1 KiB
INI
48 lines
1.1 KiB
INI
|
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
|