From cc86c2326ff08c931ae79fccdaf984d34722189d Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 23 May 2022 15:54:39 +0200
Subject: [PATCH] Improve display of evaluation errors using new position
information
---
CHANGELOG.md | 1 +
notebooks/tests/assert.ipynb | 4 +-
notebooks/tests/eval.ipynb | 24 +++---
.../java/de/prob2/jupyter/CommandUtils.java | 73 ++++++-------------
.../prob2/jupyter/commands/AssertCommand.java | 5 +-
5 files changed, 40 insertions(+), 67 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b8922b2..f7ce336 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,7 @@
## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test)
* Updated ProB 2 to version 4.0.0-SNAPSHOT.
+* Added position information to formula evaluation errors (e. g. type or well-definedness errors).
* Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index 8d6f514..a6b39cf 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -223,10 +223,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'",
+ "evalue": ":assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'\u001b[0m"
+ "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')\u001b[0m"
]
}
],
diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
index 6cdfedf..a3ca672 100644
--- a/notebooks/tests/eval.ipynb
+++ b/notebooks/tests/eval.ipynb
@@ -242,11 +242,13 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: Computation not completed: Unknown identifier \"unknown\"",
+ "ename": "ProBError",
+ "evalue": "ERROR\nProB returned error messages:\nError: Unknown identifier \"unknown\" (:1:0 to 1:7)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"unknown\"\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mERROR\u001b[0m",
+ "\u001b[1m\u001b[31mError: Unknown identifier \"unknown\" (:1:0 to 1:7)\u001b[0m",
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
@@ -260,11 +262,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
+ "ename": "ProBError",
+ "evalue": "UNKNOWN (enumeration warning)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUNKNOWN (enumeration warning)\u001b[0m"
]
}
],
@@ -278,13 +280,13 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-WELL-DEFINED: \nmod not defined for negative numbers: 2 mod-1\n ### Line: 1, Column: 0 until 8\n\n",
+ "ename": "ProBError",
+ "evalue": "NOT-WELL-DEFINED\nProB returned error messages:\nError: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
- "\u001b[1m\u001b[31mmod not defined for negative numbers: 2 mod-1\u001b[0m",
- "\u001b[1m\u001b[31m ### Line: 1, Column: 0 until 8\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-WELL-DEFINED\u001b[0m",
+ "\u001b[1m\u001b[31mError: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8)\u001b[0m",
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index 1951b38..692931f 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -18,16 +18,14 @@ import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.command.GetDefaultPreferencesCommand;
import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.domainobjects.AbstractEvalResult;
-import de.prob.animator.domainobjects.ComputationNotCompletedResult;
import de.prob.animator.domainobjects.EnumerationWarning;
+import de.prob.animator.domainobjects.ErrorItem;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.EvaluationErrorResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.animator.domainobjects.IdentifierNotInitialised;
import de.prob.animator.domainobjects.ProBPreference;
import de.prob.animator.domainobjects.TypeCheckResult;
-import de.prob.animator.domainobjects.WDError;
import de.prob.exception.ProBError;
import de.prob.formula.PredicateBuilder;
import de.prob.statespace.Trace;
@@ -258,7 +256,6 @@ public final class CommandUtils {
public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) {
final StringBuilder sb = new StringBuilder();
final StringBuilder sbMarkdown = new StringBuilder();
- final boolean error;
if (aer instanceof EvalResult) {
final EvalResult result = (EvalResult)aer;
sb.append(UnicodeTranslator.toUnicode(result.getValue()));
@@ -280,75 +277,47 @@ public final class CommandUtils {
sbMarkdown.append('$');
});
}
- error = false;
- } else if (aer instanceof ComputationNotCompletedResult) {
- final ComputationNotCompletedResult result = (ComputationNotCompletedResult)aer;
- sb.append("Computation not completed: ");
- sb.append(result.getReason());
- error = true;
} else if (aer instanceof EnumerationWarning) {
- sb.append("UNKNOWN (FALSE with enumeration warning)");
- error = true;
+ throw new ProBError(aer.toString());
} else if (aer instanceof EvaluationErrorResult) {
final EvaluationErrorResult result = (EvaluationErrorResult)aer;
- sb.append(result.getResult());
- if (!result.getErrors().isEmpty()) {
- sb.append(": ");
- result.getErrors().forEach(s -> {
- sb.append('\n');
- sb.append(s);
- });
- }
- error = true;
+ throw new ProBError(result.getResult(), result.getErrorItems());
} else {
- LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
sb.append(aer);
sbMarkdown.append(aer);
- error = false;
}
- if (error) {
- throw new UserErrorException(sb.toString());
- } else {
- final DisplayData result = new DisplayData(sb.toString());
- result.putMarkdown(sbMarkdown.toString());
- return result;
- }
+ final DisplayData result = new DisplayData(sb.toString());
+ result.putMarkdown(sbMarkdown.toString());
+ return result;
}
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() + ')';
+ final EvaluationErrorResult result = (EvaluationErrorResult)aer;
+ final StringBuilder sb = new StringBuilder("(");
+ sb.append(result.getResult());
+ if (!result.getErrorItems().isEmpty()) {
+ sb.append(": ");
+ sb.append(result.getErrorItems().stream()
+ .map(ErrorItem::getMessage)
+ .collect(Collectors.joining(", ")));
+ }
+ sb.append(")");
+ return sb.toString();
} 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.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() + ")*";
+ if (aer instanceof EvaluationErrorResult) {
+ // Display errors in italics
+ return "*" + inlinePlainTextForEvalResult(aer) + "*";
} else {
- LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
- return aer.toString();
+ return inlinePlainTextForEvalResult(aer);
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 31a2f55..9c974c0 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -9,6 +9,7 @@ import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
+import de.prob.exception.ProBError;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
@@ -81,8 +82,8 @@ public final class AssertCommand implements Command {
final DisplayData displayData;
try {
displayData = CommandUtils.displayDataForEvalResult(result);
- } catch (final UserErrorException e) {
- throw new UserErrorException("Error while evaluating assertion: " + e.getMessage());
+ } catch (final ProBError e) {
+ throw new UserErrorException("Error while evaluating assertion: " + CommandUtils.inlinePlainTextForEvalResult(result), e);
}
throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN));
}
--
GitLab