Complete HandleAppendEntriesRequest (raft.tla:327) + UpdateTerm (raft.tla:406), implemented as one function to avoid a misleading partial handler. Fixed step order: UpdateTerm FIRST on every RPC incl. heartbeat (G5, strictly-greater, clears voted_for, persists, leader step-down fires on_become_follower) -> stale reject -> candidate step-down -> logOk (G2) -> reject if !logOk -> accept (already-have / conflict-truncate-then-repersist (G3) / append). Never advances commit, never does transport I/O. Review-applied: logOk now includes the explicit prev_log_index <= log_len bound (raft.tla:330 / Req 4.1) instead of relying solely on the 0-absent sentinel; added a candidate-equal-term-logOk-fails step-ordering test. 15 tests, ASAN green. |
||
|---|---|---|
| .. | ||
| settings | ||
| specs | ||
| steering | ||