From 0b3d80b052bf68cad3f71ba2322d3a9e5d7bc0b8 Mon Sep 17 00:00:00 2001
From: Federico Ponzi <me@fponzi.me>
Date: Wed, 12 Jun 2024 09:15:25 +0100
Subject: [PATCH] Diameter is nondeterministic with multiple workers

Persist the learning from issue #883. Diameter is
non-deterministic when the BFS is run with multiple workers.

Signed-off-by: Federico Ponzi <me@fponzi.me>
---
 general/docs/current-tools.md                              | 4 ++++
 tlatools/org.lamport.tlatools/src/tlc2/TLC.java            | 2 ++
 .../html/model/tlc-options-page.html                       | 7 +++++++
 3 files changed, 13 insertions(+)

diff --git a/general/docs/current-tools.md b/general/docs/current-tools.md
index 0347684408..9cb30473f6 100644
--- a/general/docs/current-tools.md
+++ b/general/docs/current-tools.md
@@ -30,6 +30,10 @@ ISpec == IM!Spec
 
 TLC cannot handle natural numbers greater than 2<sup>31</sup> - 1.
 
+When running the model checking in BFS mode with multiple workers on a medium-small model, the reported diameter might differ across runs.
+This is a limitation we accept to avoid putting additional synchronization that would limit the scalability of the visit. 
+For small models, use a single worker. For large models, the diameter will almost always appear deterministic.
+
 ### Additional Features
 
 #### Enhanced Replacement
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
index cab68b805d..a714d2f701 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
@@ -1687,6 +1687,8 @@ private void printUsage()
 					+ "duplicate operator definitions, this is likely due to the 'monolith' specification\n"
 					+ "creation. Try re-running TLC adding the 'nomonolith' option to the '-generateSpecTE'\n"
 					+ "parameter.");
+        tips.add("When using more than one worker, the reported depth might differ. For small models, use a single " +
+                "worker. For large models, the diameter will almost always appear deterministic.");
     	
     	UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC,
     								"provides model checking and simulation of TLA+ specifications",
diff --git a/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html b/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html
index 7db4dc7f0c..231bc61ab4 100644
--- a/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html
+++ b/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html
@@ -38,6 +38,11 @@ <h3>Number of worker threads</h3>
 This parameter specifies the number of separate threads that TLC will spawn to
 perform that computation.&nbsp;  You should not set it to be greater than the number of
 separate processors (cores) on your computer; the Toolbox will warn you if you do.
+When using multiple workers on a medium-small model, the reported <i>Diameter</i> might
+differ across runs.
+This is a limitation we accept to avoid putting additional synchronization that would limit
+the scalability of the visit. For small models, use a single worker. For large models,
+the diameter will almost always appear deterministic.
 
 <h3>Fraction of physical memory allocated to TLC</h3>
 
@@ -96,6 +101,8 @@ <h3><a  name="model-mode">Model-checking mode</a></h3>
 queue, so it does not produce any
  <i>Diameter</i> or <i>Queue size</i>
  statistics.
+Additionally, <em>Depth-first</em> option doesn't currently
+support running with multiple workers.
 </p>
 <p>
 <b>Warning:</b> Depth-first search is an experimental TLC