Check high-level liveness properties in simulation mode (#6545)

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>

tla/consensus/MCccfraft.cfg

@@ -1,8 +1,9 @@
-SPECIFICATION mc_spec
+SPECIFICATION Spec
 
 CONSTANTS
     Servers <- ToServers
     
+    Init <- MCInit
     Timeout <- MCTimeout
     RcvProposeVoteRequest <- MCRcvProposeVoteRequest
     Send <- MCSend

tla/consensus/MCccfraft.tla

@@ -12,6 +12,7 @@ Configurations ==
             [] IOEnv.RAFT_CONFIGS = "1C2N" -> default
             [] IOEnv.RAFT_CONFIGS = "1C3N" -> <<{NodeOne, NodeTwo, NodeThree}>>
             [] IOEnv.RAFT_CONFIGS = "2C2N" -> <<{NodeOne}, {NodeTwo}>>
+            [] IOEnv.RAFT_CONFIGS = "2C3N" -> <<{NodeOne, NodeTwo}, {NodeTwo, NodeThree}>>
             [] IOEnv.RAFT_CONFIGS = "3C2N" -> <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>>
             [] OTHER -> Print("Unsupported value for RAFT_CONFIGS, defaulting to 1C2N: <<{NodeOne, NodeTwo}>>.", default)
     ELSE Print("RAFT_CONFIGS is not set, defaulting to 1C2N: <<{NodeOne, NodeTwo}>>.", default)
@@ -115,11 +116,6 @@ MCInit ==
        \* If we want to start with multiple nodes, we can start with a four-tx log with a reconfiguration already appended.
        ELSE InitLogConfigServerVars(Configurations[1], JoinedLog)
 
-\* Alternative to CCF!Spec that uses the above MCInit
-mc_spec ==   
-    /\ MCInit
-    /\ [][Next]_vars
-
 \* Symmetry set over possible servers. May dangerous and is only enabled
 \* via the Symmetry option in cfg file.
 Symmetry == Permutations(Servers)

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

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 ==

tla/consensus/ccfraft.tla

@@ -1273,11 +1273,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))
@@ -1291,8 +1287,17 @@ Spec ==
     /\ \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))
     /\ \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
@@ -1613,7 +1618,8 @@ LogMatchingProp ==
     \A i, j \in Servers : []<>(log[i] = log[j])
 
 LeaderProp ==
-    []<><<\E i \in Servers : leadershipState[i] = Leader>>_vars
+    \* There is repeatedly a non-retired leader.
+    []<><<\E i \in Servers : leadershipState[i] = Leader /\ membershipState[i] # RetiredCommitted>>_vars
 
 ------------------------------------------------------------------------------
 \* Refinement of the more high-level specification abs.tla that abstracts the