Add :modelcheck command (#14)

CHANGELOG.md

@@ -5,6 +5,7 @@
 * Added a `--user` flag to the installer to allow installing the kernel into the user home directory. This allows installing the kernel without `sudo` when not using a virtual environment.
 * Added `:let` and `:unlet` commands to (un)define local variables.
 	* **Note:** Local variables are currently stored and expanded in text form. Values whose text form is not parsable cannot be stored in local variables, and storing large values may cause performance issues.
+* Added a `:modelcheck` command to run the ProB model checker.
 * Added support for additional languages and file extensions. The `:load` command now recognizes all languages and file extensions supported by ProB 2.
 	* **Note:** Some languages are not fully working yet (for example XTL).
 * Added support for Java 11.

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -39,6 +39,7 @@ import de.prob2.jupyter.commands.InitialiseCommand;
 import de.prob2.jupyter.commands.LetCommand;
 import de.prob2.jupyter.commands.LoadCellCommand;
 import de.prob2.jupyter.commands.LoadFileCommand;
+import de.prob2.jupyter.commands.ModelCheckCommand;
 import de.prob2.jupyter.commands.NoSuchCommandException;
 import de.prob2.jupyter.commands.PrefCommand;
 import de.prob2.jupyter.commands.PrettyPrintCommand;
@@ -178,6 +179,7 @@ public final class ProBKernel extends BaseKernel {
 		this.commands.put(":groovy", injector.getInstance(GroovyCommand.class));
 		this.commands.put("::render", injector.getInstance(RenderCommand.class));
 		this.commands.put(":prettyprint", injector.getInstance(PrettyPrintCommand.class));
+		this.commands.put(":modelcheck", injector.getInstance(ModelCheckCommand.class));
 		
 		this.variables = new HashMap<>();
 		

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

+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.check.CheckError;
+import de.prob.check.ConsistencyChecker;
+import de.prob.check.IModelCheckingResult;
+import de.prob.check.ModelCheckErrorUncovered;
+import de.prob.check.NotYetFinished;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.StateSpace;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class ModelCheckCommand implements Command {
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private ModelCheckCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":modelcheck";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Run the ProB model checker on the current model.";
+	}
+	
+	@Override
+	public @NotNull String getHelpBody() {
+		return "If an error state is found, it is made the current state, so that it can be inspected using `:trace`, `:check`, etc.";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		if (!argString.isEmpty()) {
+			throw new UserErrorException("Unexpected argument: " + argString);
+		}
+		
+		final StateSpace stateSpace = this.animationSelector.getCurrentTrace().getStateSpace();
+		final ConsistencyChecker job = new ConsistencyChecker(stateSpace);
+		final IModelCheckingResult result = job.call();
+		
+		final StringBuilder sbPlain = new StringBuilder();
+		if (result instanceof NotYetFinished || result instanceof CheckError) {
+			throw new UserErrorException("Model check could not finish properly: " + result);
+		} else if (result instanceof ModelCheckErrorUncovered) {
+			sbPlain.append("Model check uncovered an error: ");
+			sbPlain.append(result.getMessage());
+			sbPlain.append("\nUse :trace to view the trace to the error state.");
+			this.animationSelector.changeCurrentAnimation(((ModelCheckErrorUncovered)result).getTrace(stateSpace));
+		} else {
+			sbPlain.append(result.getMessage());
+		}
+		return new DisplayData(sbPlain.toString());
+	}
+	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return null;
+	}
+	
+	@Override
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+		return null;
+	}
+}