In replsettest.js, ReplSetTest starts up a single node replica set then reconfigures to the correct size (if the config contains more than 1 node), so the primary is elected more quickly.

This presents a problem for TLA+ trace checking. RaftMongo.tla specifies that a server's commit point is an optime included in the server's oplog. I.e., for server s, if commitPoint[s] is [term -> t, index-> i], then Len(log[s]) >= i and log[s][i] == t.

When TLA+ trace logging is enabled, the server logs its commit point and the visible contents of the oplog whenever it executes a TLA+ action. The member of a one-node set can advance the commit point beyond the visible timestamp, leading to a weird log line: the commit point is beyond all optimes in the oplog.

For now, let's not support one-node sets with TLA+ trace checking. Let's add an JSTest TestData option that disables the two-stage initialization so that we don't pass through the one-node config when we initialize a set for trace checking.

This is not a hard requirement for the trace checking project. We could choose to trace check only replica sets started for fuzz testing by replicaset.py instead of ReplSetTest.js. However, it would be broadly useful to check execution traces from our existing JSTests.