From 09a64c2b7db450f5b8be7b4a6a89261e93fb4ea7 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 16 Jul 2018 12:49:22 +0200 Subject: [PATCH] Add :check command to show and check properties/invariant/assertions --- .../java/de/prob2/jupyter/ProBKernel.java | 2 + .../prob2/jupyter/commands/CheckCommand.java | 106 ++++++++++++++++++ .../prob2/jupyter/commands/CommandUtils.java | 40 ++++++- 3 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 src/main/java/de/prob2/jupyter/commands/CheckCommand.java diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java index 0c02692..46846d6 100644 --- a/src/main/java/de/prob2/jupyter/ProBKernel.java +++ b/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)); diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java new file mode 100644 index 0000000..c8ca685 --- /dev/null +++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java @@ -0,0 +1,106 @@ +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()); + } +} diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java index 557c4e7..8d1517e 100644 --- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java +++ b/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(), -- GitLab