Diameter is nondeterministic with multiple workers

Persist the learnings 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>
 
@@ -101,7 +106,7 @@ <h3><a  name="model-mode">Model-checking mode</a></h3>
 <b>Warning:</b> Depth-first search is an experimental TLC
 option that has not been used much. We don't know
 if it offers any advantages.
-If you do try it and find it useful, please tell us what you did.
+If you do try it and find it useful, please tell us what you did. It only support running with a single worker.
 </p>
 
 <p>