diff --git a/tla/consensus/SIMCoverageccfraft.R b/tla/consensus/SIMCoverageccfraft.R
deleted file mode 100644
index f7822ce015e9..000000000000
--- a/tla/consensus/SIMCoverageccfraft.R
+++ /dev/null
@@ -1,18 +0,0 @@
-require(ggplot2)
-require(dplyr)
-
-df <- unique(read.csv(header = TRUE, sep = "#", file = "./SIMCoverageccfraft_S5.csv"))
-
-# Add a column to df that combines the three columns Spec, P, and C.
-df$SpecP <- paste(df$Spec, df$P, df$Q, df$R, sep = "_")
-
-# Eyeball if all configurations are roughly equally represented.
-df %>% group_by(SpecP) %>% summarize(count = n())
-# Count the occurrences of each character sequence in column state
-# grouped by column SpecP.
-df %>%
-  group_by(SpecP, state) %>%
-  summarize(count = n()) %>%
-  ggplot(aes(x=SpecP, fill=state, y=count)) +
-    geom_bar(stat="identity") +
-    theme(axis.text.x = element_text(angle = 90, vjust = 0.5, hjust=1))
diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg
deleted file mode 100644
index 60ad478208d7..000000000000
--- a/tla/consensus/SIMCoverageccfraft.cfg
+++ /dev/null
@@ -1,49 +0,0 @@
-SPECIFICATION SIMCoverageSpec
-
-CONSTANTS
-    Servers <- Servers_mc
-
-    Nil = Nil
-
-    Follower = L_Follower
-    Candidate = L_Candidate
-    Leader = L_Leader
-    None = L_None
-
-    Active = R_Active
-    RetirementOrdered = R_RetirementOrdered
-    RetirementSigned = R_RetirementSigned
-    RetirementCompleted = R_RetirementCompleted
-    RetiredCommitted = R_RetiredCommitted
-
-    RequestVoteRequest = M_RequestVoteRequest
-    RequestVoteResponse = M_RequestVoteResponse
-    AppendEntriesRequest = M_AppendEntriesRequest
-    AppendEntriesResponse = M_AppendEntriesResponse
-    ProposeVoteRequest = M_ProposeVoteRequest
-
-    OrderedNoDup = N_OrderedNoDup
-    Ordered = N_Ordered
-    ReorderedNoDup = N_ReorderedNoDup
-    Reordered = N_Reordered
-    Guarantee = N_OrderedNoDup
-
-    TypeEntry = T_Entry
-    TypeSignature = T_Signature
-    TypeReconfiguration = T_Reconfiguration
-    TypeRetired = T_Retired
-
-    NodeOne = n1
-    NodeTwo = n2
-    NodeThree = n3
-    NodeFour = n4
-    NodeFive = n5
-
-    Timeout <- SIMTimeout
-    ChangeConfigurationInt <-SIMChangeConfigurationInt
-    CheckQuorum <- SIMCheckQuorum
-
-    InitReconfigurationVars <- SIMInitReconfigurationVars
-
-CONSTRAINT
-    StatisticsStateConstraint
diff --git a/tla/consensus/SIMCoverageccfraft.tla b/tla/consensus/SIMCoverageccfraft.tla
index 69f2d0c4c277..83f3d02bd82b 100644
--- a/tla/consensus/SIMCoverageccfraft.tla
+++ b/tla/consensus/SIMCoverageccfraft.tla
@@ -1,65 +1,40 @@
----------- MODULE SIMCoverageccfraft ----------
-EXTENDS ccfraft, TLC, Integers, CSV, TLCExt
 
-CONSTANTS
-    NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
+  $ wget https://nightly.tlapl.us/dist/tla2tools.jar
+  $ wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
+  ## Run with as many workers as you like to parallelize the nested simulation runs (auto uses all your cores).
+  $ java -jar tla2tools.jar -config SIMCoverageccfraft.tla SIMCoverageccfraft.tla -workers auto
 
-Servers_mc == {NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive}
+----------------------------- MODULE SIMCoverageccfraft -----------------------------
+EXTENDS TLC, Naturals, Sequences, IOUtils
 
-Baseline ==
-    {<<"Next", 0..0, 0..0, 0..0>>}
+CmdLine ==
+    <<"sh", "-c",
+    "java " \o
+    "-XX:+UseParallelGC " \o
+    "-Dtlc2.tool.impl.Tool.cdot=true " \o
+    "-Dtlc2.tool.Simulator.extendedStatistics=true " \o
+    "-jar tla2tools.jar " \o
+    "-depth 1000 " \o
+    "-simulate SIMccfraft.tla >> SIMCoverageccfraft.txt 2>&1">>
 
-Confs == 
-    Baseline \cup
-        ({"SIMNext"} \X {1..1, 1..10, 1..100} \X {201..201, 201..210, 201..300} \X {401..401, 401..410, 401..500})
+-----------------------------------------------------------------------------
 
-VARIABLE conf
+VARIABLE c, d
 
-CCF == INSTANCE ccfraft
+Init ==
+    /\ c \in [ R: {10, 1000}, C: {10, 1000}, Q: {10, 1000}, T: {10, 1000} ]
+    /\ d = FALSE
 
-SIMInitReconfigurationVars == 
-    \/ CCF!InitLogConfigServerVars(Servers, JoinedLog)
-    \/ CCF!InitReconfigurationVars
+Next ==
+    /\ ~d
+    /\ d' = TRUE
+    /\ PrintT(<<"conf", c>>)
+    /\ IOEnvExec(c, CmdLine).exitValue = 0
+    /\ UNCHANGED c
 
-SIMCheckQuorum(i) ==
-    /\ conf[1] # "Next" => RandomElement(1..1000) \in conf[3]
-    /\ CCF!CheckQuorum(i)
-
-SIMChangeConfigurationInt(i, newConfiguration) ==
-    /\ conf[1] # "Next" => RandomElement(1..1000) \in conf[4]
-    /\ CCF!ChangeConfigurationInt(i, newConfiguration)
-
-SIMTimeout(i) ==
-    /\ \/ RandomElement(1..1000) \in conf[2]
-       \/ conf[1] # "Next"
-       \* Always allow Timeout if no messages are in the network
-       \* and no node is a candidate or leader.  Otherwise, the system
-       \* will deadlock if 1 # RandomElement(...).
-       \/ /\ \A s \in Servers: leadershipState[s] \notin {Leader, Candidate}
-          /\ Network!Messages = {}
-    /\ CCF!Timeout(i)
-
-SIMCoverageSpec ==
-    /\ Init
-    /\ conf \in Confs
-    /\ [][UNCHANGED conf /\ Next]_<<vars, conf>>
-
-------------------------------------------------------------------------------
-
-CSVFile == "SIMCoverageccfraft_S" \o ToString(Cardinality(Servers)) \o ".csv"
-
-CSVColumnHeaders ==
-    "Spec#P#Q#R#currentTerm#state#commitIndex#log#node"
-
-ASSUME
-    CSVRecords(CSVFile) = 0 => 
-        CSVWrite(CSVColumnHeaders, <<>>, CSVFile)
-
-StatisticsStateConstraint ==
-    (TLCGet("level") > TLCGet("config").depth) =>
-        TLCDefer(\A s \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s",
-                << conf[1], Cardinality(conf[2]), Cardinality(conf[3]), Cardinality(conf[4]), 
-                   currentTerm[s], leadershipState[s], commitIndex[s], Len(log[s]), s
-                   >>,
-                CSVFile))
 =============================================================================
+---- CONFIG SIMCoverageccfraft ----
+INIT Init
+NEXT Next
+CHECK_DEADLOCK FALSE
+====
\ No newline at end of file
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index 0e2dac7a5aac..26d2b1f51e06 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -42,6 +42,7 @@ CONSTANTS
     Timeout <- SIMTimeout
     ChangeConfigurationInt <-SIMChangeConfigurationInt
     CheckQuorum <- SIMCheckQuorum
+    ClientRequest <- SIMClientRequest
 
     Fairness <- SIMFairness
 
@@ -50,8 +51,8 @@ CONSTANTS
     Extend <- [abs]ABSExtend
     CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
-CONSTRAINT
-    StopAfter
+_PERIODIC
+    Periodically
 
 CHECK_DEADLOCK
     FALSE
diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
index 269db4c61009..d9c234e89cf6 100644
--- a/tla/consensus/SIMccfraft.tla
+++ b/tla/consensus/SIMccfraft.tla
@@ -1,5 +1,5 @@
 ---------- MODULE SIMccfraft ----------
-EXTENDS ccfraft, TLC, Integers, IOUtils, MCAliases
+EXTENDS ccfraft, TLC, Integers, IOUtils
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
@@ -16,16 +16,32 @@ SIMInitReconfigurationVars ==
     \* Start with any subset of servers in the active configuration.
     \/ CCF!InitReconfigurationVars
 
+LOCAL R ==
+    1..IF "R" \in DOMAIN IOEnv THEN atoi(IOEnv.R) ELSE 10
+
+SIMClientRequest(i) ==
+    /\ 1 = RandomElement(R)
+    /\ CCF!ClientRequest(i)
+
+LOCAL Q ==
+    1..IF "Q" \in DOMAIN IOEnv THEN atoi(IOEnv.Q) ELSE 10
+
 SIMCheckQuorum(i) ==
-    /\ 1 = RandomElement(1..10)
+    /\ 1 = RandomElement(Q)
     /\ CCF!CheckQuorum(i)
 
+LOCAL C ==
+    1..IF "C" \in DOMAIN IOEnv THEN atoi(IOEnv.C) ELSE 10
+
 SIMChangeConfigurationInt(i, newConfiguration) ==
-    /\ 1 = RandomElement(1..100)
+    /\ 1 = RandomElement(C)
     /\ CCF!ChangeConfigurationInt(i, newConfiguration)
 
+LOCAL T ==
+    1..IF "T" \in DOMAIN IOEnv THEN atoi(IOEnv.T) ELSE 1000
+
 SIMTimeout(i) ==
-    /\ \/ 1 = RandomElement(1..100)
+    /\ \/ 1 = RandomElement(T)
        \* Always allow Timeout if no messages are in the network
        \* and no node is a candidate or leader.  Otherwise, the system
        \* will deadlock if 1 # RandomElement(...).
@@ -58,13 +74,26 @@ SIMFairness ==
         \E newConfiguration \in SUBSET(Servers) \ {{}}:
             WF_vars(CCF!ChangeConfigurationInt(s, newConfiguration))
 
-\* The state constraint  StopAfter  stops TLC after the alloted
+----
+
+\* StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounters an error first.
 StopAfter ==
     LET timeout == IF ("SIM_TIMEOUT" \in DOMAIN IOEnv) /\ IOEnv.SIM_TIMEOUT # "" THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
-    (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)
 
+SerializeFilename ==
+    "SIMccfraft_" \o "R-" \o ToString(R) \o "_T-" \o ToString(T) \o "_Q-" \o ToString(Q) \o "_C-" \o ToString(C) \o "_ts-" \o ToString(JavaTime) \o ".ndjson"
+
+SerializeTLCStats ==
+    Serialize(<<TLCGet("stats")>>, SerializeFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+
+Periodically ==
+    /\ StopAfter
+    /\ SerializeTLCStats
+
+----
+
 DebugInvUpToDepth ==
     \* The following invariant causes TLC to terminate with a counterexample of length
     \* -depth after generating the first trace.