Redefine the fairness constraint in simulation mode to exclude Random…

…Element conjuncts that interfere with enablement. See tlaplus/tlaplus#1039 (comment) for details. Signed-off-by: Markus Alexander Kuppe <[email protected]>
microsoft · Oct 9, 2024 · 47eb0d9 · 47eb0d9
1 parent 1533530
commit 47eb0d9
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 5 deletions.
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -43,6 +43,8 @@ CONSTANTS
     ChangeConfigurationInt <-SIMChangeConfigurationInt
     CheckQuorum <- SIMCheckQuorum
 
+    Fairness <- SIMFairness
+
     InitReconfigurationVars <- SIMInitReconfigurationVars
 
     Extend <- [abs]ABSExtend
@@ -65,6 +67,9 @@ PROPERTIES
     NeverCommitEntryPrevTermsProp
     RefinementToAbsProp
 
+    LeaderProp
+    LogMatchingProp
+
 \* ALIAS
 \*     \* DebugAlias
 \*     \* DebugActingServerAlias

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -33,6 +33,31 @@ SIMTimeout(i) ==
           /\ Network!Messages = {}
     /\ CCF!Timeout(i)
 
+\* See https://github.com/tlaplus/tlaplus/issues/1039#issue-2574569206
+\* for why we need to redefine the fairness constraint.
+SIMFairness ==
+    \* 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(RcvProposeVoteRequest(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(AppendRetiredCommitted(s))
+    /\ \A s \in Servers : WF_vars(BecomeLeader(s))
+    \* The following fairness conditions reference the original CCF actions
+    \* and, thus, do not include the RandomElement conjunct.
+    /\ \A s \in Servers : WF_vars(CCF!Timeout(s))
+    /\ \A s \in Servers : 
+        \E newConfiguration \in SUBSET(Servers) \ {{}}:
+            WF_vars(CCF!ChangeConfigurationInt(s, newConfiguration))
+
 \* The state constraint  StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounters an error first.
 StopAfter ==

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -1278,11 +1278,7 @@ NextInt(i) ==
 Next ==
     \E i \in Servers: NextInt(i)
 
-\* The specification must start with the initial state and transition according
-\* to Next.
-Spec == 
-    /\ Init
-    /\ [][Next]_vars
+Fairness ==
     \* Network actions
     /\ \A i, j \in Servers : WF_vars(RcvDropIgnoredMessage(i, j))
     /\ \A i, j \in Servers : WF_vars(RcvUpdateTerm(i, j))
@@ -1301,6 +1297,13 @@ Spec ==
     /\ \A s \in Servers : WF_vars(Timeout(s))
     /\ \A s \in Servers : WF_vars(ChangeConfiguration(s))
 
+\* The specification must start with the initial state and transition according
+\* to Next.
+Spec == 
+    /\ Init
+    /\ [][Next]_vars
+    /\ Fairness
+
 ------------------------------------------------------------------------------
 \* Correctness invariants
 \* These invariants should be true for all possible states