Decaton v9 upgrade spec

UpgradeToV9.cfg

SPECIFICATION Spec

CONSTANTS
  Clients = {c1, c2}
  Processors = {proc1, proc2}
  MaxTaskID = 3
  MaxRetries = 2

INVARIANTS MetaFormatInvariant

UpgradeToV9.tla

----------------------------- MODULE UpgradeToV9 -----------------------------
EXTENDS Integers, FiniteSets, Sequences, TLC

CONSTANTS
    Clients,         \* Set of producer instances
    Processors,      \* Set of processor instances
    MaxTaskID,       \* Maximum task ID for bounded model checking
    MaxRetries       \* Maximum number of retries per task

VARIABLES
    topic,
    retryTopic,
    nextTaskID,      \* Counter for generating unique task IDs
    clientVersion, \* Maps each producer to its version (V8_OR_LOW or V9_OR_NEW)
    processorConfig, \* Maps each processor to its configuration
    processed        \* Set of successfully processed task IDs

vars == <<topic, retryTopic, nextTaskID, clientVersion, processorConfig, processed>>

\* Task format versions
V8_OR_LOW == "V8_OR_LOW"
V9_OR_NEW == "V9_OR_NEW"

\* Task record structure: [id: Int, format: String, hasMeta: Boolean, retryCount: Int]

\* Initial state
Init ==
    /\ topic = <<>>
    /\ retryTopic = <<>>
    /\ nextTaskID = 1
    /\ clientVersion = [p \in Clients |-> V8_OR_LOW]  \* All producers start with OLD version
    /\ processorConfig = [p \in Processors |-> [
                            retry_tasks_in_legacy_format |-> TRUE,
                            legacy_parse_fallback_enabled |-> TRUE
                          ]]
    /\ processed = {}

AddTask(p) ==
    /\ nextTaskID <= MaxTaskID
    /\ LET
           format == IF clientVersion[p] = V9_OR_NEW THEN V9_OR_NEW ELSE V8_OR_LOW
           hasMeta == (format = V9_OR_NEW)
           task == [id |-> nextTaskID, format |-> format, hasMeta |-> hasMeta, retryCount |-> 0]
       IN
           /\ topic' = Append(topic, task)
           /\ nextTaskID' = nextTaskID + 1
    /\ UNCHANGED <<retryTopic, clientVersion, processorConfig, processed>>

ProcessTask(p) ==
    /\ topic /= <<>>
    /\ LET
           task == Head(topic)
       IN
           /\ topic' = Tail(topic)
           /\ processed' = processed \union {task.id}
    /\ UNCHANGED <<retryTopic, nextTaskID, clientVersion, processorConfig>>

ProcessRetryTask(p) ==
    /\ retryTopic /= <<>>
    /\ LET
           task == Head(retryTopic)
       IN
           /\ retryTopic' = Tail(retryTopic)
           /\ processed' = processed \union {task.id}
    /\ UNCHANGED <<topic, nextTaskID, clientVersion, processorConfig>>

RetryTask(p) ==
    /\ topic /= <<>>
    /\ LET
           task == Head(topic)
           retryFormat ==
              IF processorConfig[p].retry_tasks_in_legacy_format THEN V8_OR_LOW ELSE V9_OR_NEW
           retryTask == [
               id |-> task.id,
               format |-> retryFormat,
               \* As of v9.1.0: hasMeta |-> task.hasMeta \/ (retryFormat = V9_OR_NEW)
               hasMeta |-> retryFormat = V9_OR_NEW,
               retryCount |-> task.retryCount + 1
           ]
       IN
           /\ task.retryCount < MaxRetries
           /\ topic' = Tail(topic)
           /\ retryTopic' = Append(retryTopic, retryTask)
    /\ UNCHANGED <<nextTaskID, clientVersion, processorConfig, processed>>

UpgradeClient(p) ==
    /\ clientVersion[p] = V8_OR_LOW
    /\ clientVersion' = [clientVersion EXCEPT ![p] = V9_OR_NEW]
    /\ UNCHANGED <<topic, retryTopic, nextTaskID, processorConfig, processed>>

UpdateProcessorConfig(p, newRetryInLegacy, newSupportLegacy) ==
    /\ processorConfig' = [processorConfig EXCEPT ![p] = [
                              retry_tasks_in_legacy_format |-> newRetryInLegacy,
                              legacy_parse_fallback_enabled |-> newSupportLegacy
                           ]]
    /\ UNCHANGED <<topic, retryTopic, nextTaskID, clientVersion, processed>>

\* Upgrade procedures
Step2 ==
    /\ \E p \in Clients: UpgradeClient(p)

Step3 ==
    \E p \in Processors: UpdateProcessorConfig(p, FALSE, processorConfig[p].legacy_parse_fallback_enabled)

Step5 ==
    /\ \A i \in 1..Len(topic): topic[i].format = V9_OR_NEW
    /\ \A i \in 1..Len(retryTopic): retryTopic[i].format = V9_OR_NEW
    /\ \E p \in Processors: UpdateProcessorConfig(p, processorConfig[p].retry_tasks_in_legacy_format, FALSE)

\* Next state
Next ==
    \/ \E p \in Clients: AddTask(p)
    \/ \E p \in Processors: ProcessTask(p)
    \/ \E p \in Processors: RetryTask(p)
    \/ Step2
    \/ Step3
    \/ Step5

\* Spec
Spec == Init /\ [][Next]_vars

\* INVARIANT: "meta exists if and only if task is in new format"
MetaFormatInvariant ==
    /\ \A i \in 1..Len(topic): topic[i].hasMeta <=> topic[i].format = V9_OR_NEW
    /\ \A i \in 1..Len(retryTopic): retryTopic[i].hasMeta <=> retryTopic[i].format = V9_OR_NEW
=============================================================================

Result: Succeeded