TLC will report a bogus violation of the property TraceMatched if TLC…

… runs with more than a single worker.
microsoft · Aug 17, 2023 · 5ee128f · 5ee128f
1 parent d8bdc3c
commit 5ee128f
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/tla/Traceccfraft.tla b/tla/Traceccfraft.tla
@@ -363,6 +363,9 @@ TraceView ==
 
 -------------------------------------------------------------------------------------
 
+\* The property TraceMatched below will be violated if TLC runs with more than a single worker.
+ASSUME TLCGet("config").worker = 1
+
 TraceMatched ==
     \* We force TLC to check TraceMatched as a temporal property because TLC checks temporal
     \* properties after generating all successor states of the current state, unlike