From f0d65012498b48e602622ccb2c7451357c6f6328 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Thu, 2 Nov 2023 10:00:20 +0000 Subject: [PATCH] Startup --- .../trace_validation.yml | 25 ++++++++++--------- tla/consensus/ccfraft.tla | 4 ++- 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/.azure-pipelines-templates/trace_validation.yml b/.azure-pipelines-templates/trace_validation.yml index 09d0a4b58627..22679c2e62e1 100644 --- 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 index a70f8a5661e1..9f0b9edd2b10 100644 --- 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 <>