summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTess Avitabile <tess.avitabile@mongodb.com>2019-12-18 16:09:44 +0000
committerevergreen <evergreen@mongodb.com>2019-12-18 16:09:44 +0000
commit527ad1d4b805b2901a058219693c8706711bf4c1 (patch)
tree6144da92cbbfc873c1bb424d35b675340ea4c37f /src
parentb14cfb55e25db5a7f05355054f687bcc73779ee2 (diff)
downloadmongo-527ad1d4b805b2901a058219693c8706711bf4c1.tar.gz
SERVER-44340 Clarify that spec was for exploratory purposes only
Diffstat (limited to 'src')
-rw-r--r--src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla b/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla
index 4ac6b3d473b..377f928d939 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla
+++ b/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla
@@ -7,6 +7,8 @@
--------------------------------- MODULE RaftMongoWithRaftReconfig --------------------------------
\* This is the formal specification for the Raft consensus algorithm in MongoDB.
\* It allows reconfig using the protocol for single server membership changes described in Raft.
+\* Note that we did not choose to implement the protocol for single server membership changes
+\* described in Raft. This specification was for exploratory purposes only.
EXTENDS Naturals, FiniteSets, Sequences, TLC