Display status information while :modelcheck is running

src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java

 package de.prob2.jupyter.commands;
 
+import java.util.concurrent.atomic.AtomicLong;
+
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.check.CheckError;
 import de.prob.check.ConsistencyChecker;
+import de.prob.check.IModelCheckListener;
 import de.prob.check.IModelCheckingResult;
 import de.prob.check.ModelCheckErrorUncovered;
+import de.prob.check.ModelCheckingOptions;
 import de.prob.check.NotYetFinished;
+import de.prob.check.StateSpaceStats;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.StateSpace;
+import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
+import io.github.spencerpark.jupyter.kernel.JupyterIO;
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -18,12 +26,16 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class ModelCheckCommand implements Command {
+	private static final AtomicLong idCounter = new AtomicLong();
+	
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private ModelCheckCommand(final @NotNull AnimationSelector animationSelector) {
+	private ModelCheckCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -42,6 +54,25 @@ public final class ModelCheckCommand implements Command {
 		return "If an error state is found, it is made the current state, so that it can be inspected using `:trace`, `:check`, etc.";
 	}
 	
+	private static @NotNull String formatMillisecondsAsSeconds(final long milliseconds) {
+		return String.format("%d.%03d", milliseconds / 1000, milliseconds % 1000);
+	}
+	
+	private static @NotNull String formatModelCheckStats(final long timeElapsed, final @Nullable StateSpaceStats stats) {
+		final StringBuilder sb = new StringBuilder(formatMillisecondsAsSeconds(timeElapsed));
+		sb.append(" sec");
+		if (stats != null) {
+			sb.append(", ");
+			sb.append(stats.getNrProcessedNodes());
+			sb.append(" of ");
+			sb.append(stats.getNrTotalNodes());
+			sb.append(" states processed, ");
+			sb.append(stats.getNrTotalTransitions());
+			sb.append(" transitions");
+		}
+		return sb.toString();
+	}
+	
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		if (!argString.isEmpty()) {
@@ -49,7 +80,28 @@ public final class ModelCheckCommand implements Command {
 		}
 		
 		final StateSpace stateSpace = this.animationSelector.getCurrentTrace().getStateSpace();
-		final ConsistencyChecker job = new ConsistencyChecker(stateSpace);
+		
+		final JupyterIO io = this.kernelProvider.get().getIO();
+		
+		// Create the DisplayData that will be used to display status updates.
+		final String statusDataId = ModelCheckCommand.class.getName() + " status " + idCounter.getAndIncrement();
+		final DisplayData data = new DisplayData("");
+		data.setDisplayId(statusDataId);
+		io.display.display(data);
+		
+		final ConsistencyChecker job = new ConsistencyChecker(stateSpace, ModelCheckingOptions.DEFAULT, null, new IModelCheckListener() {
+			@Override
+			public void updateStats(final @NotNull String jobId, final long timeElapsed, final @NotNull IModelCheckingResult result, final @Nullable StateSpaceStats stats) {
+				io.display.updateDisplay(statusDataId, new DisplayData(formatModelCheckStats(timeElapsed, stats) + "\n" + result.getMessage()));
+			}
+			
+			@Override
+			public void isFinished(final @NotNull String jobId, final long timeElapsed, final @NotNull IModelCheckingResult result, final @Nullable StateSpaceStats stats) {
+				// Same as updateStats, except that the result is not included, because the final result will be displayed as the main command result instead of in the status.
+				io.display.updateDisplay(statusDataId, new DisplayData(formatModelCheckStats(timeElapsed, stats)));
+			}
+		});
+		
 		final IModelCheckingResult result = job.call();
 		
 		final StringBuilder sbPlain = new StringBuilder();