Adding a new configuration to the model checking CI (#5802)

.github/workflows/tlaplus.yml

@@ -28,6 +28,11 @@ jobs:
           cd tla/
           ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
 
+      - name: MCccfraftAtomicReconfig.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json
+
       - name: MCccfraftWithReconfig.cfg
         run: |
           cd tla/

tla/consensus/MCccfraft.tla

@@ -5,6 +5,7 @@ CONSTANTS
     NodeOne, NodeTwo, NodeThree
 
 1Configuration == <<{NodeOne, NodeTwo, NodeThree}>>
+2Configurations == <<{NodeOne}, {NodeTwo}>>
 3Configurations == <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>>
 
 CONSTANT Configurations
@@ -24,10 +25,13 @@ CCF == INSTANCE ccfraft
 \* This file controls the constants as seen below.
 \* In addition to basic settings of how many nodes are to be model checked,
 \* the model allows to place additional limitations on the state space of the program.
+
+\* Limit the reconfigurations to the next configuration in Configurations
 MCChangeConfigurationInt(i, newConfiguration) ==
-    /\ reconfigurationCount < Len(Configurations)
+    /\ reconfigurationCount < Len(Configurations)-1
     \* +1 because TLA+ sequences are 1-index
-    /\ newConfiguration = Configurations[reconfigurationCount+1]
+    \* +1 to get the next configuration
+    /\ newConfiguration = Configurations[reconfigurationCount+2]
     /\ CCF!ChangeConfigurationInt(i, newConfiguration)
 
 \* Limit the terms that can be reached. Needs to be set to at least 3 to
@@ -49,7 +53,7 @@ MCTimeout(i) ==
     /\ CCF!Timeout(i)
 
 \* Limit on client requests
-RequestLimit == 2
+RequestLimit == 3
 
 \* Limit number of requests (new entries) that can be made
 MCClientRequest(i) ==
@@ -93,7 +97,25 @@ MCNotifyCommit(i,j) ==
 MCInMaxSimultaneousCandidates(i) ==
     Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1
 
-mc_spec == Spec
+\* Alternative to CCF!InitReconfigurationVars that sets the initial configuration to the first config defined in Configurations
+MCInitReconfigurationVars ==
+    /\ reconfigurationCount = 0
+    /\ removedFromConfiguration = {}
+    /\ configurations = [i \in Servers |-> 0 :> Configurations[1]]
+
+\* Alternative to CCF!Init that uses the above MCInitReconfigurationVars
+MCInit ==
+    /\ MCInitReconfigurationVars
+    /\ CCF!InitMessagesVars
+    /\ CCF!InitServerVars
+    /\ CCF!InitCandidateVars
+    /\ CCF!InitLeaderVars
+    /\ CCF!InitLogVars
+
+\* 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.
@@ -106,7 +128,7 @@ View == << reconfigurationVars, <<messages, commitsNotified>>, serverVars, candi
 
 AllReconfigurationsCommitted == 
     \E s \in ToServers:
-        \A c \in ToSet(Configurations):
+        \A c \in ToSet(Tail(Configurations)):
             \E i \in DOMAIN Committed(s):
                 /\ HasTypeReconfiguration(Committed(s)[i])
                 /\ Committed(s)[i].configuration = c

tla/consensus/MCccfraftAtomicReconfig.cfg

@@ -0,0 +1,78 @@
+SPECIFICATION mc_spec
+
+CONSTANTS
+    Configurations <- 2Configurations
+    Servers <- ToServers
+
+    MaxTermLimit = 4
+    MaxCommitsNotified = 2
+
+    Timeout <- MCTimeout
+    Send <- MCSend
+    ClientRequest <- MCClientRequest
+    SignCommittableMessages <- MCSignCommittableMessages
+    ChangeConfigurationInt <- MCChangeConfigurationInt
+    NotifyCommit <- MCNotifyCommit
+
+    Nil = Nil
+
+    Follower = Follower
+    Candidate = Candidate
+    Leader = Leader
+    RetiredLeader = RetiredLeader
+    Pending = Pending
+
+    RequestVoteRequest = RequestVoteRequest
+    RequestVoteResponse = RequestVoteResponse
+    AppendEntriesRequest = AppendEntriesRequest
+    AppendEntriesResponse = AppendEntriesResponse
+    NotifyCommitMessage = NotifyCommitMessage
+    ProposeVoteRequest = ProposeVoteRequest
+
+    OrderedNoDup = OrderedNoDup
+    Ordered = Ordered
+    ReorderedNoDup = ReorderedNoDup
+    Reordered = Reordered
+    Guarantee = OrderedNoDup
+
+    TypeEntry = Entry
+    TypeSignature = Signature
+    TypeReconfiguration = Reconfiguration
+
+    NodeOne = n1
+    NodeTwo = n2
+    NodeThree = n3
+
+SYMMETRY Symmetry
+VIEW View
+
+CHECK_DEADLOCK 
+    FALSE
+
+PROPERTIES
+    CommittedLogAppendOnlyProp
+    MonotonicTermProp
+    MonotonicMatchIndexProp
+    PermittedLogChangesProp
+    StateTransitionsProp
+    PendingBecomesFollowerProp
+    NeverCommitEntryPrevTermsProp
+
+INVARIANTS
+    LogInv
+    MoreThanOneLeaderInv
+    CandidateTermNotInLogInv
+    ElectionSafetyInv
+    LogMatchingInv
+    QuorumLogInv
+    MoreUpToDateCorrectInv
+    LeaderCompletenessInv
+    SignatureInv
+    TypeInv
+    MonoTermInv
+    MonoLogInv
+    LogConfigurationConsistentInv
+    NoLeaderInTermZeroInv
+    MatchIndexLowerBoundNextIndexInv
+    CommitCommittableIndices
+    CommittableIndicesAreKnownSignaturesInv