2026-07-13 18:23:03 +09:00
|
|
|
SPECIFICATION Spec
|
|
|
|
|
|
|
|
|
|
CHECK_DEADLOCK TRUE
|
|
|
|
|
|
|
|
|
|
CONSTANTS
|
|
|
|
|
OperationScopes = {scope1}
|
|
|
|
|
EligibilityClaims = {eligibility1, eligibility2}
|
|
|
|
|
OperationIds = {op1, op2}
|
|
|
|
|
MutationKinds = {submit, renew, progress, success, failure}
|
|
|
|
|
Fingerprints = {fp1, fp2}
|
|
|
|
|
NoEligibility = NoEligibility
|
|
|
|
|
NoRecord = NoRecord
|
|
|
|
|
NoObservation = NoObservation
|
|
|
|
|
Accepted = Accepted
|
2026-07-13 18:36:32 +09:00
|
|
|
Rejected = Rejected
|
2026-07-13 18:23:03 +09:00
|
|
|
FirstObservation = FirstObservation
|
|
|
|
|
ReplayObservation = ReplayObservation
|
|
|
|
|
ConflictObservation = ConflictObservation
|
|
|
|
|
|
|
|
|
|
INVARIANTS
|
|
|
|
|
TypeOK
|
|
|
|
|
RecordEffectConsistency
|
|
|
|
|
RevisionCountsEffects
|
|
|
|
|
ObservationConsistent
|
|
|
|
|
|
|
|
|
|
PROPERTIES
|
|
|
|
|
RecordsAppendOnly
|
|
|
|
|
EffectsApplyAtMostOnce
|
|
|
|
|
RevisionMonotonic
|
