From de2713baaf2728059427619d6ad852845d4f7218 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 7 Sep 2023 11:06:12 -0700 Subject: [PATCH] Add two high-level liveness properties and a suitable fairness constraint. Have to be manually added to TLC's config files for now. --- tla/ccfraft.tla | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla index 0abf3a1e7176..fc74623056a5 100644 --- a/tla/ccfraft.tla +++ b/tla/ccfraft.tla @@ -1100,7 +1100,24 @@ Next == \* The specification must start with the initial state and transition according \* to Next. -Spec == Init /\ [][Next]_vars +Spec == + /\ Init + /\ [][Next]_vars + \* Network actions + /\ \A i, j \in Servers : WF_vars(RcvDropIgnoredMessage(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvUpdateTerm(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvRequestVoteRequest(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvRequestVoteResponse(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvAppendEntriesRequest(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvAppendEntriesResponse(i, j)) + /\ \A i, j \in Servers : WF_vars(RcvUpdateCommitIndex(i, j)) + \* Node actions + /\ \A s, t \in Servers : WF_vars(AppendEntries(s, t)) + /\ \A s, t \in Servers : WF_vars(RequestVote(s, t)) + /\ \A s \in Servers : WF_vars(SignCommittableMessages(s)) + /\ \A s \in Servers : WF_vars(AdvanceCommitIndex(s)) + /\ \A s \in Servers : WF_vars(BecomeLeader(s)) + /\ \A s \in Servers : WF_vars(Timeout(s)) ------------------------------------------------------------------------------ \* Correctness invariants @@ -1315,6 +1332,12 @@ PendingBecomesFollowerProp == s \in GetServerSet(s)' => state[s]' = Follower]_vars +LogMatchingProp == + \A i, j \in Servers : []<>(log[i] = log[j]) + +LeaderProp == + []<><<\E i \in Servers : state[i] = Leader>>_vars + ------------------------------------------------------------------------------ \* Debugging invariants \* These invariants should give error traces and are useful for debugging to see if important situations are possible