From 428f34854a0ecf29634ca77e1a2f164f46e2b4f3 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 1 May 2023 09:30:44 -0700 Subject: [PATCH] Assert a node's currentTerm at every step. (Reveals inconsistencies in raft.h logging). --- tla/Traceccfraft.tla | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tla/Traceccfraft.tla b/tla/Traceccfraft.tla index 610ef8bd6..03f916277 100644 --- a/tla/Traceccfraft.tla +++ b/tla/Traceccfraft.tla @@ -347,6 +347,10 @@ TraceNextConstraint == \* BP:: line below is the first step towards diagnosing a divergence. Once \* hit, advance evaluation with step over (F10) and step into (F11). BP:: + \* json state logging in raft.h is inconsistent; sometimes it logs the state before + \* and othertimes after the state change. Therefore, we must check both. + /\ \/ currentTerm[logline.msg.state.node_id] = logline.msg.state.current_view + \/ currentTerm'[logline.msg.state.node_id] = logline.msg.state.current_view /\ \/ IsTimeout(logline) \/ IsBecomeLeader(logline) \/ IsBecomeFollower(logline)