Remove writing state-space statistics after the demise of cimetrics.

Part of "Run TLA+ consensus/consistency from vscode" #6490 #6490 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
microsoft · Oct 2, 2024 · 6cde298 · 6cde298
1 parent 76b2dcf
commit 6cde298
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 13 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -60,9 +60,6 @@ POSTCONDITION
 CONSTRAINTS
     CoverageExpressions
 
-_PERIODIC
-    SerializeCoverage
-
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -1,5 +1,5 @@
 ---------- MODULE MCccfraft ----------
-EXTENDS ccfraft, StatsFile, MCAliases, TLC, IOUtils
+EXTENDS ccfraft, MCAliases, TLC, IOUtils
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree
@@ -168,8 +168,7 @@ AreAllCovered ==
 ----
 
 PostConditions ==
-    /\ WriteStatsFile
-    /\ AreAllCovered
+    AreAllCovered
 
 ----
 \* Refinement

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -39,9 +39,6 @@ CONSTANTS
     NodeFour = n4
     NodeFive = n5
 
-    StatsFilename = "SIMccfraft_stats.json"
-    CoverageFilename = "SIMccraft_coverage.json"
-
     Timeout <- SIMTimeout
     ChangeConfigurationInt <-SIMChangeConfigurationInt
     CheckQuorum <- SIMCheckQuorum
@@ -69,9 +66,6 @@ PROPERTIES
     NeverCommitEntryPrevTermsProp
     RefinementToAbsProp
 
-POSTCONDITION
-    WriteStatsFile
-
 \* ALIAS
 \*     \* DebugAlias
 \*     \* DebugActingServerAlias

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -1,5 +1,5 @@
 ---------- MODULE SIMccfraft ----------
-EXTENDS ccfraft, TLC, Integers, StatsFile, IOUtils, MCAliases
+EXTENDS ccfraft, TLC, Integers, IOUtils, MCAliases
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive