Change visibility of getTrace(TLCState) method to public.

tlatools/src/tlc2/tool/ConcurrentTLCTrace.java

@@ -73,7 +73,10 @@ public class ConcurrentTLCTrace extends TLCTrace {
 		return maxLevel;
 	}
 
-	private TLCStateInfo[] getTrace(final TLCState state) throws IOException {
+	/**
+	 * @see TLCTrace#getTrace(LongVec)
+	 */
+	public TLCStateInfo[] getTrace(final TLCState state) throws IOException {
 		final LongVec fps = new LongVec();
 
 		// Starting at the given start fingerprint (which is the end of the

tlatools/src/tlc2/tool/TLCTrace.java

@@ -260,6 +260,17 @@ public class TLCTrace {
 		return getTrace(fps);
 	}
 
+	/**
+	 * This method is *not* safe to call multiple times iff the spec being checked
+	 * consumed randomness, ie. TLC!RandomElement or through the Randomization
+	 * module. In other words, such specs are incompatible with TLC's -continue
+	 * mode.
+	 * <p>
+	 * To implement this correctly, state space exploration would either have to
+	 * halt while the fingerprints are resolved to TLCStates below or ITool has
+	 * to offer additional API s.t. the seed of RandomEnumerableValues gets
+	 * passed as part of the method call.
+	 */
 	protected final TLCStateInfo[] getTrace(LongVec fps) {
 		// Re-Initialize the rng with the seed value recorded and used during the model
 		// checking phase. Otherwise, we won't be able to reconstruct the error trace

tlatools/src/tlc2/value/impl/EnumerableValue.java

@@ -121,7 +121,7 @@ public abstract class EnumerableValue extends Value implements Enumerable {
 			//
 			// x has to be co-prime to n. Since n might or might not be a prime number
 			// - it depends on the actual size of the set - we simply set x to
-			// be a prime number. The prime x has to be larger than n tough, since n is
+			// be a prime number. The prime x has to be larger than n though, since n is
 			// bound by Integer.MAX_VALUE, we simply choose the Mersenne prime
 			// Integer.MAX_VALUE
 			// for x and accept that we fail if n = Integer.MAX_VALUE. To minimize