Notify TLC users about the performance overhead related to

coverage collection after N minutes of model checking.

The assumption is that a user has little interest in coverage for a
large (long-running) model anyway. Subsequent commit will raise a
notification in the Toolbox too.

[Feature][TLC]

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java

@@ -480,6 +480,7 @@ public void onOutput(ITypedRegion region, String text)
                     }
                     informPresenter(ITLCModelLaunchDataPresenter.COVERAGE);
                     break;
+                case EC.TLC_COVERAGE_END_OVERHEAD:
                 case EC.TLC_COVERAGE_END:
                     informPresenter(ITLCModelLaunchDataPresenter.COVERAGE_END);
                     break;

tlatools/src/tlc2/output/EC.java

@@ -234,6 +234,7 @@ public interface EC
     public static final int TLC_COVERAGE_NEXT = 2772;
     public static final int TLC_COVERAGE_INIT = 2773;
     public static final int TLC_COVERAGE_PROPERTY = 2774;
+    public static final int TLC_COVERAGE_END_OVERHEAD = 2777;
 
     // config file errors
     public static final int TLC_CONFIG_VALUE_NOT_ASSIGNED_TO_CONSTANT_PARAM = 2222;

tlatools/src/tlc2/output/MP.java

@@ -972,6 +972,10 @@ else if (parameters.length == 2) {
         case EC.TLC_COVERAGE_END:
             b.append("End of statistics.");
             break;
+		case EC.TLC_COVERAGE_END_OVERHEAD:
+			b.append("End of statistics (please note that for performance reasons large models\n"
+					+ "are best checked with coverage and cost statistics disabled).");
+            break;
 
         /* ************************************************************************ */
         // errors evaluating the config file and the MC file

tlatools/src/tlc2/tool/AbstractChecker.java

@@ -145,7 +145,7 @@ protected void reportCoverage(IWorker[] workers)
 		// Without actions (empty spec) there won't be any statistics anyway.
 		if (TLCGlobals.isCoverageEnabled() && this.tool.getActions().length > 0)
 		{
-            CostModelCreator.report(this.tool);
+            CostModelCreator.report(this.tool, this.startTime);
         }
     }
 

tlatools/src/tlc2/tool/Simulator.java

@@ -125,6 +125,11 @@ public Simulator(String specFile, String configFile, String traceFile, boolean d
 
 	// Each simulation worker pushes their results onto this shared queue.
 	private BlockingQueue<SimulationWorkerResult> workerResultQueue = new LinkedBlockingQueue<>();
+
+    /**
+     * Timestamp of when simulation started.
+     */
+	private final long startTime = System.currentTimeMillis();
 
 	 /**
 	 * Returns whether a given error code is considered "continuable". That is, if
@@ -359,7 +364,7 @@ public final void printSummary() {
 	 */
 	public final void reportCoverage() {
 		if (TLCGlobals.isCoverageEnabled()) {
-            CostModelCreator.report(this.tool);
+            CostModelCreator.report(this.tool, this.startTime );
 		}
 	}
 

tlatools/src/tlc2/tool/coverage/CostModelCreator.java

@@ -327,7 +327,7 @@ public static final void create(final ITool tool) {
 		}
 	}
 
-	public static void report(final ITool tool) {
+	public static void report(final ITool tool, final long startTime) {
         MP.printMessage(EC.TLC_COVERAGE_START);
     	final Vect<Action> init = tool.getInitStateSpec();
     	for (int i = 0; i < init.size(); i++) {
@@ -355,6 +355,17 @@ public int compare(Action o1, Action o2) {
         	//TODO Might have to be ordered similar to next-state actions above.
         	invariant.cm.report();
 		}
-        MP.printMessage(EC.TLC_COVERAGE_END);
+
+		// Notify users about the performance overhead related to coverage collection
+		// after N minutes of model checking. The assumption is that a user has little
+		// interest in coverage for a large (long-running) model anyway.  In the future
+        // it is hopefully possible to switch from profiling to sampling to relax the
+        // performance overhead of coverage and cost statistics.
+		final long l = System.currentTimeMillis() - startTime;
+		if (l > (5L * 60L * 1000L)) {
+			MP.printMessage(EC.TLC_COVERAGE_END_OVERHEAD);
+		} else {
+			MP.printMessage(EC.TLC_COVERAGE_END);
+		}
 	}
 }