TLC does *not* randomize the enumeration of e.g. IntervalValue instances

with `.probabilistic=true`.

[Bug][TLC]

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

@@ -83,7 +83,7 @@ public ValueEnumeration elements(final Ordering ordering) {
 				return ((Enumerable) enumerated.normalize()).elements();
 			}
 		} else if (ordering == Ordering.RANDOMIZED) {
-			elements(size());
+			return elements(size());
 		}
 		return elements();
 	}