ms2k
6b6588c5ac
Encode zero-orphan intent as EventuallyNonWinnerStagingCleaned and EventuallySystemQuiescent under recovery. Stop authorized attempts on FinalizeCancel and do not re-publish cancel notices after terminal so fair behaviors can reach SystemQuiescent (TLC-checked on Remora.cfg).
46 lines
1.1 KiB
INI
46 lines
1.1 KiB
INI
SPECIFICATION Spec
|
|
|
|
CHECK_DEADLOCK TRUE
|
|
|
|
\* Fair Spec + liveness under coordination faults. Fault budgets are 1 so
|
|
\* temporal checking finishes in minutes; multi-shot budgets are covered by
|
|
\* RemoraMultiShot.cfg (safety-only).
|
|
CONSTANTS
|
|
Jobs = {j1}
|
|
Workers = {w1, w2}
|
|
InitialWorkers = {w1}
|
|
NoJob = NoJob
|
|
NoWorker = NoWorker
|
|
MaxAttempts = 2
|
|
MaxProgress = 1
|
|
LeaseLimit = 1
|
|
LocalLimit = 1
|
|
GlobalLimit = 1
|
|
FaultsEnabled = TRUE
|
|
FaultServices = {"Coordination"}
|
|
MaxCoordLosses = 1
|
|
MaxPartitions = 1
|
|
|
|
INVARIANTS
|
|
TypeOK
|
|
StateConsistency
|
|
AllocatedTokensUsed
|
|
LiveProgressWellFormed
|
|
LiveProgressCompatibleWithLiveLease
|
|
AtMostOneLiveLeasePerJob
|
|
AuthorityWellFormed
|
|
CommittedResultConsistent
|
|
CancellationSafety
|
|
PermitSafety
|
|
ResumeValidity
|
|
StagingOwnership
|
|
|
|
PROPERTIES
|
|
TerminalStateIsImmutable
|
|
FencingTokensMonotonic
|
|
CommitIsFencedCAS
|
|
EventuallyDispatched
|
|
EventuallyReaped
|
|
EventuallyTerminal
|
|
EventuallyNonWinnerStagingCleaned
|
|
EventuallySystemQuiescent
|