Startup

achamayou · Nov 2, 2023 · f0d6501 · f0d6501
1 parent 0866229
commit f0d6501
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 13 deletions.
diff --git a/.azure-pipelines-templates/trace_validation.yml b/.azure-pipelines-templates/trace_validation.yml
@@ -10,16 +10,17 @@ steps:
       set -ex
       cd tla/
       parallel 'JSON={} ./tlc.sh consensus/Traceccfraft.tla' ::: \
-      ../build/replicate.ndjson \
-      ../build/election.ndjson \
-      ../build/multi_election.ndjson \
-      ../build/check_quorum.ndjson \
-      ../build/reconnect.ndjson \
-      ../build/reconnect_node.ndjson \
-      ../build/bad_network.ndjson \
-      ../build/fancy_election.1.ndjson \
-      ../build/fancy_election.2.ndjson \
-      ../build/suffix_collision.1.ndjson \
-      ../build/suffix_collision.2.ndjson \
-      ../build/suffix_collision.3.ndjson
+      ../build/startup.ndjson
+      # ../build/replicate.ndjson \
+      # ../build/election.ndjson \
+      # ../build/multi_election.ndjson \
+      # ../build/check_quorum.ndjson \
+      # ../build/reconnect.ndjson \
+      # ../build/reconnect_node.ndjson \
+      # ../build/bad_network.ndjson \
+      # ../build/fancy_election.1.ndjson \
+      # ../build/fancy_election.2.ndjson \
+      # ../build/suffix_collision.1.ndjson \
+      # ../build/suffix_collision.2.ndjson \
+      # ../build/suffix_collision.3.ndjson
     displayName: "Run trace validation"
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -667,9 +667,11 @@ ChangeConfigurationInt(i, newConfiguration) ==
             configuration |-> newConfiguration,
             contentType |-> TypeReconfiguration]
         newLog == [log[i] EXCEPT ![Len(log[i])] = entry]
+        \* Remove the ghost configuration at index 0, there's no index 0 in the log
+        validConfigurationPrefix == [ci \in DOMAIN configurations[i] \ {0} |-> configurations[i]]
         IN
         /\ log' = [log EXCEPT ![i] = newLog]
-        /\ configurations' = [configurations EXCEPT ![i] = @ @@ Len(log[i]) :> newConfiguration]
+        /\ configurations' = [configurations EXCEPT ![i] = validConfigurationPrefix @@ Len(log[i]) :> newConfiguration]
     /\ UNCHANGED <<messageVars, serverVars, candidateVars,
                     leaderVars, commitIndex, committableIndices>>