Models failing smoke testing #65

Addresses Github issue #65 #65 [Bug]
tlaplus · Feb 2, 2023 · fca6a17 · fca6a17
1 parent dd4bb5b
commit fca6a17
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/specifications/ewd426/SimTokenRing.tla b/specifications/ewd426/SimTokenRing.tla
@@ -3,6 +3,10 @@ EXTENDS TokenRing, TLC, CSV, IOUtils
 
 (* Statistics collection *)
 
+\* TCLGet("stats").traces is only defined when TLC runs in simulation or generation mode.
+\* For this spec, users have to run TLC in generate mode to collect meaningful statistics.
+ASSUME TLCGet("config").mode = "generate"
+
 CSVFile ==
     "SimTokenRing.csv"
 
@@ -24,4 +28,4 @@ $ rm -rf states/ ; rm *.csv ; tlc SimTokenRing -note -generate -depth -1
 
 
 $ alias tlc
-tlc='java -cp /path/to/tla2tools.jar tlc2.TLC'
+tlc='java -cp /path/to/tla2tools.jar tlc2.TLC'