Diameter is nondeterministic with multiple workers

Persist the learning from issue tlaplus#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

@@ -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

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",

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