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
    Rejected = Rejected
    FirstObservation = FirstObservation
    ReplayObservation = ReplayObservation
    ConflictObservation = ConflictObservation

INVARIANTS
    TypeOK
    RecordEffectConsistency
    RevisionCountsEffects
    ObservationConsistent

PROPERTIES
    RecordsAppendOnly
    EffectsApplyAtMostOnce
    RevisionMonotonic