tidying up

microsoft · Nov 1, 2023 · eef132e · eef132e
1 parent 27e2fbf
commit eef132e
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 9 deletions.
diff --git 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
@@ -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")>>)
 
 ===================================
diff --git 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
@@ -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