15 files changed, 5 insertions, 5 deletions
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