Larger Context

test/model provides deterministic model-based verification for disaggregated workloads, but it does not generate single-node role transitions.

Motivation

Switch-mode coverage will exercise repeated changes between leader and follower roles together. It complements Python and test/format coverage with an independent correctness model, deterministic replay, and reduced counterexamples.

Scope

This Epic delivers follower-mode workload support as the first stepping stone, followed by the synchronous switch_role operation, transition-requirement validation, randomised switch_role generation, and one model-test-switch Evergreen task. It also includes design and proof-of-concept work for asynchronous switch_role.

Full asynchronous implementation will be planned after the design and proof of concept are complete.

Acceptance Criteria

• Fixed and randomised workloads perform valid repeated transitions in both directions.
• Transactions, timestamps, checkpoints, crashes, and restarts behave correctly around role transitions.
• Counterexample reduction and deterministic replay work for switch-mode workloads.
• Model and WiredTiger operation results and recovered data match.
• model-test-switch runs the randomised workload in Evergreen.
• The asynchronous design work produces an implementation-ready recommendation or identifies remaining blockers.

Outcome

test/model provides reusable single-node role-transition infrastructure and a clear path for asynchronous step-down and future multi-node role-transition testing.