Parallel TLC (workers > 1) intermittently reports an incorrect, too low

diameter.

See #45 for the corresponding
issue.

[Documentation]

tlatools/src/tlc2/tool/TLCTrace.java

@@ -121,18 +121,51 @@ public final int getLevelForReporting() throws IOException {
 
 	/**
 	 * @see TLCTrace#getLevel(long)
+	 * @return 1 to the length of the longest behavior found so far.
 	 */
 	public final int getLevel() throws IOException {
-	// This assumption (lastPtr) only holds for the TLC in non-parallel mode.
+	    // This assumption (lastPtr) only holds for the TLC in non-parallel mode.
 		// Generally the last line (logically a state) is not necessarily
-		// on the highest level of the state tree. This is only the case if
-		// states are explored strictly by breadth-first search.
+		// on the highest level of the state tree, which is only true if
+		// states are explored with strict breadth-first search.
+		//
+		// The (execution) trace is a forest of one to n trees, where each path 
+		// in the forest represents the order in which states have been generated
+		// by the workers.
+		// The algorithm, with which the diameter is approximated from the trace,
+		// is pretty simple; too simple. The trace is constantly written to the .st
+		// file where each "record" in the file is a link from a successor state to
+		// its predecessor state. Thus, the link is a position in the trace file
+		// where the predecessor state - actually its fingerprint - is stored. At
+		// the end of the trace file, there are up to m leaf records for which no
+		// successors have been appended (yet, assuming there are any).
+		//
+		// Once the workers have terminated, TLC traverses the trace from a leaf record
+		// back to a root record. This height is what is reported as the diameter. 
+		// The selection, from what leaf record TLC starts the traversal, is based on
+		// the last record inserted into the trace file. If this record is one with a
+		// low height (because its corresponding worker waited most of the time), the
+		// diameter will thus be underreport. If, on the other hand, the last record 
+		// happens to be one with a large height, the diameter will be overreported.
+		// 
+		// The selection of the leaf record is the source of the algorithm's 
+		// non-determinism. With a single worker, the last record in the trace is
+		// always the same which always corresponds to the longest behavior found so 
+		// far (strict BFS). This invariant does not hold with multiple workers.
+        //
+		// Obviously, with multiple workers the approximation of the diameter will
+		// improve with the size of the state graph. Assuming a well-shaped state graph,
+		// we can argue that the approximation is good enough and document, that its 
+		// value can be anything from 1 to the longest behavior found so far.
 		return getLevel(this.lastPtr);
 	}
 
 	/**
-   * @param startLoc The start location (pointer) from where the level (height) of the state tree should be calculated
-	 * @return The level (height) of the state tree.
+	 * @param startLoc
+	 *            The start location (pointer) from where the level (height) of
+	 *            the path in the execution tree should be calculated.
+	 * @return The level (height) of the path in the execution tree (the trace)
+	 *         starting at startLoc.
 	 * @throws IOException
 	 */
 	public synchronized final int getLevel(long startLoc) throws IOException {

tlatools/test/tlc2/tool/DiameterTest.java

@@ -28,8 +28,6 @@
 import static org.junit.Assert.assertFalse;
 import static org.junit.Assert.assertTrue;
 
-import java.util.List;
-
 import org.junit.Test;
 
 import tlc2.output.EC;
@@ -47,12 +45,11 @@ public void testSpec() {
 		// amount of states
 		assertFalse(recorder.recorded(EC.GENERAL));
 		assertTrue(recorder.recorded(EC.TLC_FINISHED));
-		//TODO A fixed number of 97 distinct states looks fishy too.
 		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "97", "16", "0"));
 
-		// The diameter is known to be 8 (as reported by TLC running with a
-		// single worker). With multiple workers, it's possible to get a higher
-		// number. However, TLC should never report a lower value.
+		// The diameter is known to be 8 as reported by TLC running with a
+		// single worker. With multiple workers, it's possible to get a higher
+		// or a lower number.
 		assertTrue(recorder.getRecordAsInt(EC.TLC_SEARCH_DEPTH) >= 8);
 	}