Add :check command to show and check properties/invariant/assertions

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

@@ -22,6 +22,7 @@ import de.prob.statespace.Trace;
 
 import de.prob2.jupyter.commands.AssertCommand;
 import de.prob2.jupyter.commands.BrowseCommand;
+import de.prob2.jupyter.commands.CheckCommand;
 import de.prob2.jupyter.commands.Command;
 import de.prob2.jupyter.commands.CommandExecutionException;
 import de.prob2.jupyter.commands.CommandUtils;
@@ -165,6 +166,7 @@ public final class ProBKernel extends BaseKernel {
 		this.commands.put(":show", injector.getInstance(ShowCommand.class));
 		this.commands.put(":dot", injector.getInstance(DotCommand.class));
 		this.commands.put(":assert", injector.getInstance(AssertCommand.class));
+		this.commands.put(":check", injector.getInstance(CheckCommand.class));
 		this.commands.put(":time", injector.getInstance(TimeCommand.class));
 		this.commands.put(":groovy", injector.getInstance(GroovyCommand.class));
 		this.commands.put("::render", injector.getInstance(RenderCommand.class));

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

+package de.prob2.jupyter.commands;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
+import java.util.StringJoiner;
+import java.util.stream.Collectors;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.command.GetMachineStructureCommand;
+import de.prob.animator.domainobjects.AbstractEvalResult;
+import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.prologast.ASTCategory;
+import de.prob.animator.prologast.ASTFormula;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+import de.prob.unicode.UnicodeTranslator;
+
+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;
+
+public final class CheckCommand implements Command {
+	private static final @NotNull Map<@NotNull String, @NotNull String> SECTION_NAME_MAP;
+	static {
+		final Map<String, String> sectionNameMap = new HashMap<>();
+		sectionNameMap.put("properties", "PROPERTIES");
+		sectionNameMap.put("invariant", "INVARIANTS");
+		sectionNameMap.put("assertions", "ASSERTIONS");
+		SECTION_NAME_MAP = Collections.unmodifiableMap(sectionNameMap);
+	}
+	
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private CheckCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":check WHAT";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Check the machine's properties, invariant, or assertions in the current state.";
+	}
+	
+	@Override
+	public @NotNull String getHelpBody() {
+		return "The properties/invariant/assertions are checked and displayed in table form. Each row corresponds to a part of the properties/invariant conjunction, or to an assertion.";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		if (!SECTION_NAME_MAP.containsKey(argString)) {
+			throw new UserErrorException("Don't know how to check " + argString);
+		}
+		final String categoryName = SECTION_NAME_MAP.get(argString);
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		final GetMachineStructureCommand cmd = new GetMachineStructureCommand();
+		trace.getStateSpace().execute(cmd);
+		final Optional<ASTCategory> category = cmd.getPrologASTList().stream()
+			.filter(ASTCategory.class::isInstance)
+			.map(ASTCategory.class::cast)
+			.filter(c -> categoryName.equals(c.getName()))
+			.findAny();
+		
+		if (category.isPresent()) {
+			final StringJoiner sjPlain = new StringJoiner("\n");
+			final StringJoiner sjMarkdown = new StringJoiner("\n", "|Predicate|Value|\n|---|---|\n", "");
+			category.get()
+				.getSubnodes()
+				.stream()
+				.filter(ASTFormula.class::isInstance)
+				.map(ASTFormula.class::cast)
+				.forEach(f -> {
+					final AbstractEvalResult result = trace.evalCurrent(f.getFormula(FormulaExpand.TRUNCATE));
+					sjPlain.add(f.getPrettyPrint() + " = " + CommandUtils.inlinePlainTextForEvalResult(result));
+					sjMarkdown.add("|$" + UnicodeTranslator.toLatex(f.getPrettyPrint()) + "$|" + CommandUtils.inlineMarkdownForEvalResult(result) + '|');
+				});
+			final DisplayData result = new DisplayData(sjPlain.toString());
+			result.putMarkdown(sjMarkdown.toString());
+			return result;
+		} else {
+			return new DisplayData("Machine has no " + argString);
+		}
+	}
+	
+	@Override
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
+		final String prefix = argString.substring(0, at);
+		return new ReplacementOptions(SECTION_NAME_MAP.keySet()
+			.stream()
+			.filter(s -> s.startsWith(prefix))
+			.collect(Collectors.toList()), 0, argString.length());
+	}
+}

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

@@ -20,6 +20,8 @@ import de.prob.animator.domainobjects.ComputationNotCompletedResult;
 import de.prob.animator.domainobjects.EnumerationWarning;
 import de.prob.animator.domainobjects.EvalResult;
 import de.prob.animator.domainobjects.EvaluationErrorResult;
+import de.prob.animator.domainobjects.IdentifierNotInitialised;
+import de.prob.animator.domainobjects.WDError;
 import de.prob.exception.ProBError;
 import de.prob.statespace.Trace;
 import de.prob.unicode.UnicodeTranslator;
@@ -159,7 +161,7 @@ public final class CommandUtils {
 			}
 			error = true;
 		} else {
-			LOGGER.info("Unhandled eval result type, falling back to toString(): {}", aer.getClass());
+			LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
 			sb.append(aer);
 			sbMarkdown.append(aer);
 			error = false;
@@ -174,6 +176,42 @@ public final class CommandUtils {
 		}
 	}
 	
+	public static @NotNull String inlinePlainTextForEvalResult(final @NotNull AbstractEvalResult aer) {
+		if (aer instanceof EvalResult) {
+			return UnicodeTranslator.toUnicode(((EvalResult)aer).getValue());
+		} else if (aer instanceof ComputationNotCompletedResult) {
+			return "(computation not completed: " + ((ComputationNotCompletedResult)aer).getReason() + ')';
+		} else if (aer instanceof IdentifierNotInitialised) {
+			return "(not initialised)";
+		} else if (aer instanceof WDError) {
+			return "(not well-defined)";
+		} else if (aer instanceof EvaluationErrorResult) {
+			LOGGER.warn("Unknown evaluation error of type {}: {}", aer.getClass(), aer);
+			return "(evaluation error: " + ((EvaluationErrorResult)aer).getErrors() + ')';
+		} else {
+			LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
+			return aer.toString();
+		}
+	}
+	
+	public static @NotNull String inlineMarkdownForEvalResult(final @NotNull AbstractEvalResult aer) {
+		if (aer instanceof EvalResult) {
+			return '$' + UnicodeTranslator.toLatex(((EvalResult)aer).getValue()) + '$';
+		} else if (aer instanceof ComputationNotCompletedResult) {
+			return "*(computation not completed: " + ((ComputationNotCompletedResult)aer).getReason() + ")*";
+		} else if (aer instanceof IdentifierNotInitialised) {
+			return "*(not initialised)*";
+		} else if (aer instanceof WDError) {
+			return "*(not well-defined)*";
+		} else if (aer instanceof EvaluationErrorResult) {
+			LOGGER.warn("Unknown evaluation error of type {}: {}", aer.getClass(), aer);
+			return "*(evaluation error: " + ((EvaluationErrorResult)aer).getErrors() + ")*";
+		} else {
+			LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
+			return aer.toString();
+		}
+	}
+	
 	public static @NotNull ReplacementOptions offsetReplacementOptions(final @NotNull ReplacementOptions replacements, final int offset) {
 		return new ReplacementOptions(
 			replacements.getReplacements(),