From eef132ef82a8c131cbd44ffcae1299d81532308c Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Wed, 1 Nov 2023 19:53:41 +0000
Subject: [PATCH] tidying up

---
 tla/consensus/MCccfraft.cfg               |  8 +++++---
 tla/consensus/MCccfraft.tla               | 11 +++++++----
 tla/consensus/MCccfraftAtomicReconfig.cfg |  6 +++++-
 tla/consensus/MCccfraftWithReconfig.cfg   |  6 +++++-
 4 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index f8cb16fffbd4..5602cd0ed89d 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -6,8 +6,9 @@ CONSTANTS
 
     MaxTermLimit = 1
     MaxCommitsNotified = 0
-    StatsFilename = "MCccfraft_stats.json"
     RequestLimit = 3
+
+    StatsFilename = "MCccfraft_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -51,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp
@@ -78,5 +82,3 @@ INVARIANTS
     MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
-
-POSTCONDITION StatsFile
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index bd9fc1c70897..97f250a8fcf4 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -17,13 +17,14 @@ ASSUME MaxTermLimit \in Nat
 CONSTANT MaxCommitsNotified
 ASSUME MaxCommitsNotified \in Nat
 
-CONSTANT StatsFilename
-ASSUME StatsFilename \in STRING
-
 \* Limit on client requests
 CONSTANT RequestLimit
 ASSUME RequestLimit \in Nat
 
+\* Filename to write TLC stats to
+CONSTANT StatsFilename
+ASSUME StatsFilename \in STRING
+
 
 ToServers ==
     UNION Range(Configurations)
@@ -141,7 +142,9 @@ AllReconfigurationsCommitted ==
 DebugAllReconfigurationsReachableInv ==
     ~AllReconfigurationsCommitted
 
-StatsFile == 
+\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format
+\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking
+WriteStatsFile == 
     ndJsonSerialize(StatsFilename, <<TLCGet("stats")>>)
 
 ===================================
\ No newline at end of file
diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
index 73f1df795e52..914b0e160935 100644
--- a/tla/consensus/MCccfraftAtomicReconfig.cfg
+++ b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -6,8 +6,9 @@ CONSTANTS
 
     MaxTermLimit = 4
     MaxCommitsNotified = 2
-    StatsFilename = "MCccfraftAtomicReconfig_stats.json"
     RequestLimit = 3
+
+    StatsFilename = "MCccfraftAtomicReconfig_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -51,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
index 8df96ff1f760..db2f1b600bf0 100644
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -6,8 +6,9 @@ CONSTANTS
 
     MaxTermLimit = 3
     MaxCommitsNotified = 2
-    StatsFilename = "MCccfraftWithReconfig_stats.json"
     RequestLimit = 3
+
+    StatsFilename = "MCccfraftWithReconfig_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -51,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp