compaction.cfg

CONSTANTS
    MessageSentLimit = 3,
    CompactionTimesLimit = 3,
    ModelConsumer = FALSE,
    ConsumeTimesLimit = 2,
    KeySpace = {"key1", "key2"},
    ValueSpace = {1, 2},
    RetainNullKey = TRUE,
    MaxCrashTimes = 1,
    ModelProducer = FALSE

CONSTANTS
    Nil = Nil,
    Compactor_In_PhaseOne = Compactor_In_PhaseOne,
    Compactor_In_PhaseTwoWrite = Compactor_In_PhaseTwoWrite,
    Compactor_In_PhaseTwoUpdateContext = Compactor_In_PhaseTwoUpdateContext,
    Compactor_In_PhaseTwoUpdateHorizon = Compactor_In_PhaseTwoUpdateHorizon,
    Compactor_In_PhaseTwoPersistCusror = Compactor_In_PhaseTwoPersistCusror,
    Compactor_In_PhaseTwoDeleteLedger = Compactor_In_PhaseTwoDeleteLedger


SPECIFICATION Spec

INVARIANTS
    TypeSafe,
    \* we can use this invariant to reproduce the ledger leak bug, which is not fixed yet
    \* CompactedLedgerLeak,
    CompactionHorizonCorrectness,
    \* we can use this invariant to reproduce the message duplication bug, which is not fixed yet
    \* DuplicateNullKeyMessage