SERVER-59026 Move TLA+ dir from repl/ to mongo/

18 files changed, 10 insertions, 10 deletions

diff --git a/buildscripts/resmokeconfig/suites/tla_plus.yml b/buildscripts/resmokeconfig/suites/tla_plus.yml
index 6ce813f6c84..0e82c6fb3a4 100644
--- a/buildscripts/resmokeconfig/suites/tla_plus.yml
+++ b/buildscripts/resmokeconfig/suites/tla_plus.yml
@@ -2,7 +2,7 @@ test_kind: tla_plus_test
 
 selector:
   roots:
-  - src/mongo/db/repl/tla_plus/**/*.cfg
+  - src/mongo/tla_plus/**/*.cfg
 
 executor:
   config:
diff --git a/buildscripts/resmokelib/testing/testcases/tla_plus_test.py b/buildscripts/resmokelib/testing/testcases/tla_plus_test.py
index de1fd2349f5..efc4b27accd 100644
--- a/buildscripts/resmokelib/testing/testcases/tla_plus_test.py
+++ b/buildscripts/resmokelib/testing/testcases/tla_plus_test.py
@@ -15,19 +15,19 @@ class TLAPlusTestCase(interface.ProcessTestCase):
         """Initialize the TLAPlusTestCase with a TLA+ model config file.
 
         model_config_file is the full path to a file like
-        src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg.
+        src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg.
 
         java_binary is the full path to the "java" program, or None.
         """
         message = f"Path '{model_config_file}' doesn't" \
                   f" match **/<SpecName>/MC<SpecName>.cfg"
 
-        # spec_dir should be like src/mongo/db/repl/tla_plus/MongoReplReconfig.
+        # spec_dir should be like src/mongo/tla_plus/MongoReplReconfig.
         spec_dir, filename = os.path.split(model_config_file)
         if not (spec_dir and filename):
             raise ValueError(message)
 
-        # working_dir is like src/mongo/db/repl/tla_plus.
+        # working_dir is like src/mongo/tla_plus.
         self.working_dir, specname = os.path.split(spec_dir)
         if not specname or filename != f'MC{specname}.cfg':
             raise ValueError(message)
diff --git a/evergreen/download_tlc.sh b/evergreen/download_tlc.sh
index 2f4079680bb..7c4f1b11ed6 100755
--- a/evergreen/download_tlc.sh
+++ b/evergreen/download_tlc.sh
@@ -1,5 +1,5 @@
 set -o errexit
 set -o verbose
 
-cd src/src/mongo/db/repl/tla_plus
+cd src/src/mongo/tla_plus
 ./download-tlc.sh
diff --git a/src/mongo/db/repl/README.md b/src/mongo/db/repl/README.md
index 4e1edfdf648..ed58ab00185 100644
--- a/src/mongo/db/repl/README.md
+++ b/src/mongo/db/repl/README.md
@@ -1809,11 +1809,11 @@ description of the complete voting behavior, see the [Elections](#Elections) sec
 ### Formal Specification
 
 For more details on the safe reconfig protocol and its behaviors, refer to the [TLA+
-specification](https://github.com/mongodb/mongo/tree/r4.4.0-rc6/src/mongo/db/repl/tla_plus/MongoReplReconfig).
+specification](https://github.com/mongodb/mongo/tree/r4.4.0-rc6/src/mongo/tla_plus/MongoReplReconfig).
 It defines two main invariants of the protocol,
-[ElectionSafety](https://github.com/mongodb/mongo/blob/r4.4.0-rc6/src/mongo/db/repl/tla_plus/MongoReplReconfig/MongoReplReconfig.tla#L403-L404)
+[ElectionSafety](https://github.com/mongodb/mongo/blob/r4.4.0-rc6/src/mongo/tla_plus/MongoReplReconfig/MongoReplReconfig.tla#L403-L404)
 and
-[NeverRollbackCommitted](https://github.com/mongodb/mongo/blob/r4.4.0-rc6/src/mongo/db/repl/tla_plus/MongoReplReconfig/MongoReplReconfig.tla#L413-L420),
+[NeverRollbackCommitted](https://github.com/mongodb/mongo/blob/r4.4.0-rc6/src/mongo/tla_plus/MongoReplReconfig/MongoReplReconfig.tla#L413-L420),
 which assert, respectively, that no two leaders are elected in the same term and that majority
 committed writes are never rolled back.
 
diff --git a/src/mongo/db/repl/tla_plus/.gitignore b/src/mongo/tla_plus/.gitignore
index a9dcc645fd5..a9dcc645fd5 100644
--- a/src/mongo/db/repl/tla_plus/.gitignore
+++ b/src/mongo/tla_plus/.gitignore
diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg
index beb09332519..beb09332519 100644
--- a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg
+++ b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg
diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla
index 5ebe4859678..5ebe4859678 100644
--- a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla
+++ b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla
diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MongoReplReconfig.tla b/src/mongo/tla_plus/MongoReplReconfig/MongoReplReconfig.tla
index fe3061827be..fe3061827be 100644
--- a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MongoReplReconfig.tla
+++ b/src/mongo/tla_plus/MongoReplReconfig/MongoReplReconfig.tla
diff --git a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.cfg b/src/mongo/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.cfg
index bdf6a17c98f..bdf6a17c98f 100644
--- a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.cfg
+++ b/src/mongo/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.cfg
diff --git a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.tla b/src/mongo/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.tla
index 08ac48de0b2..08ac48de0b2 100644
--- a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.tla
+++ b/src/mongo/tla_plus/MultiTenantMigrations/MCMultiTenantMigrations.tla
diff --git a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MultiTenantMigrations.tla b/src/mongo/tla_plus/MultiTenantMigrations/MultiTenantMigrations.tla
index 159188481f1..fda343da0a7 100644
--- a/src/mongo/db/repl/tla_plus/MultiTenantMigrations/MultiTenantMigrations.tla
+++ b/src/mongo/tla_plus/MultiTenantMigrations/MultiTenantMigrations.tla
@@ -10,7 +10,7 @@
 \*
 \* To run the model-checker, first edit the constants in MCMultiTenantMigrations.cfg if desired,
 \* then:
-\*     cd src/mongo/db/repl/tla_plus
+\*     cd src/mongo/tla_plus
 \*     ./model-check.sh MultiTenantMigrations
 \*
 
diff --git a/src/mongo/db/repl/tla_plus/README.md b/src/mongo/tla_plus/README.md
index 04b22f406d3..04b22f406d3 100644
--- a/src/mongo/db/repl/tla_plus/README.md
+++ b/src/mongo/tla_plus/README.md
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.cfg
index 3724efb7f0b..3724efb7f0b 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg
+++ b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.cfg
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.tla b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla
index 057e3dd7a91..057e3dd7a91 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.tla
+++ b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla b/src/mongo/tla_plus/RaftMongo/RaftMongo.tla
index 06bc84baeea..bb1ce3f6684 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla
+++ b/src/mongo/tla_plus/RaftMongo/RaftMongo.tla
@@ -8,7 +8,7 @@
 \* This is the formal specification for the Raft consensus algorithm in MongoDB.
 \*
 \* To run the model-checker, first edit the constants in MCRaftMongo.cfg if desired, then:
-\*     cd src/mongo/db/repl/tla_plus
+\*     cd src/mongo/tla_plus
 \*     ./model-check.sh RaftMongo
 
 EXTENDS Integers, FiniteSets, Sequences
diff --git a/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla b/src/mongo/tla_plus/RaftMongoWithRaftReconfig.tla
index aacb2903a1b..aacb2903a1b 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongoWithRaftReconfig.tla
+++ b/src/mongo/tla_plus/RaftMongoWithRaftReconfig.tla
diff --git a/src/mongo/db/repl/tla_plus/download-tlc.sh b/src/mongo/tla_plus/download-tlc.sh
index b63944a7231..b63944a7231 100755
--- a/src/mongo/db/repl/tla_plus/download-tlc.sh
+++ b/src/mongo/tla_plus/download-tlc.sh
diff --git a/src/mongo/db/repl/tla_plus/model-check.sh b/src/mongo/tla_plus/model-check.sh
index cc53169ca28..cc53169ca28 100755
--- a/src/mongo/db/repl/tla_plus/model-check.sh
+++ b/src/mongo/tla_plus/model-check.sh