Skip to content
Snippets Groups Projects
Commit cc86c232 authored by dgelessus's avatar dgelessus
Browse files

Improve display of evaluation errors using new position information

parent b938b009
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
CHANGELOG.md
+ 1
− 0
View file @ cc86c232
......@@ -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)
......
notebooks/tests/assert.ipynb
+ 2
− 2
View file @ cc86c232
%% Cell type:code id: tags:
``` prob
:help :assert
```
%% Output
```
:assert PREDICATE
```
Ensure that the predicate is true, and show an error otherwise.
Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.
This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises.
:assert PREDICATE
Ensure that the predicate is true, and show an error otherwise.
Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.
This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises.
%% Cell type:markdown id: tags:
Asserting a true predicate shows $\mathit{TRUE}$.
%% Cell type:code id: tags:
``` prob
:assert 1 = 1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:assert TRUE
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Asserting a predicate doesn't show any solutions.
%% Cell type:code id: tags:
``` prob
:assert x > 1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Asserting a false predicate shows an error.
%% Cell type:code id: tags:
``` prob
:assert 0 = 1
```
%% Output
:assert: Assertion is not true: FALSE
%% Cell type:code id: tags:
``` prob
:assert FALSE
```
%% Output
:assert: Assertion is not true: FALSE
%% Cell type:markdown id: tags:
Asserting something that isn't a predicate/boolean shows an error.
%% Cell type:code id: tags:
``` prob
:assert 123
```
%% Output
:assert: Assertion is not true: 123
%% Cell type:code id: tags:
``` prob
:assert {}
```
%% Output
:assert: Assertion is not true: ∅
%% Cell type:markdown id: tags:
Asserting a formula with errors shows an error.
%% Cell type:code id: tags:
``` prob
:assert 123 + {}
```
%% Output
:assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'
:assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')
%% Cell type:markdown id: tags:
Local variables can be used in assertions.
%% Cell type:code id: tags:
``` prob
:let trü TRUE
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:let flasche FALSE
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
:assert trü
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:assert flasche
```
%% Output
:assert: Assertion is not true: FALSE
......
notebooks/tests/eval.ipynb
+ 13
− 11
View file @ cc86c232
%% Cell type:code id: tags:
``` prob
:help :eval
```
%% Output
```
FORMULA
// or
:eval FORMULA
```
Evaluate a formula and display the result.
Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).
If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.
FORMULA
// or
:eval FORMULA
Evaluate a formula and display the result.
Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).
If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.
%% Cell type:markdown id: tags:
Expressions can be evaluated.
%% Cell type:code id: tags:
``` prob
123
```
%% Output
$123$
123
%% Cell type:code id: tags:
``` prob
123 + 456
```
%% Output
$579$
579
%% Cell type:code id: tags:
``` prob
{1, 2} \/ {5, 6}
```
%% Output
$\{1,2,5,6\}$
{1,2,5,6}
%% Cell type:code id: tags:
``` prob
1..5
```
%% Output
$\{1,2,3,4,5\}$
{1,2,3,4,5}
%% Cell type:code id: tags:
``` prob
MAXINT
```
%% Output
$3$
3
%% Cell type:markdown id: tags:
Solution variables are displayed.
%% Cell type:code id: tags:
``` prob
#xx.(xx : NAT1 & xx mod 3 = 0)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
TRUE
Solution:
xx = 3
%% Cell type:code id: tags:
``` prob
#xx, yy.(xx > 2 & yy < 5 & xx < yy)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:markdown id: tags:
Various kinds of evaluation errors are displayed.
%% Cell type:code id: tags:
``` prob
unknown
```
%% Output
:eval: Computation not completed: Unknown identifier "unknown"
Error from ProB: ERROR
Error: Unknown identifier "unknown" (:1:0 to 1:7)
// Source code not known
%% Cell type:code id: tags:
``` prob
card({x | x > 0 & x mod 2 = 0})
```
%% Output
:eval: UNKNOWN (FALSE with enumeration warning)
Error from ProB: UNKNOWN (enumeration warning)
%% Cell type:code id: tags:
``` prob
2 mod -1
```
%% Output
:eval: NOT-WELL-DEFINED:
mod not defined for negative numbers: 2 mod-1
### Line: 1, Column: 0 until 8
Error from ProB: NOT-WELL-DEFINED
Error: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8)
// Source code not known
%% Cell type:markdown id: tags:
Expressions can be multiline.
%% Cell type:code id: tags:
``` prob
{
1, 2, 3,
4, 5, 6,
7, 8, 9
}
```
%% Output
$\{1,2,3,4,5,6,7,8,9\}$
{1,2,3,4,5,6,7,8,9}
%% Cell type:markdown id: tags:
The `:eval` command is equivalent to entering a bare expression.
%% Cell type:code id: tags:
``` prob
:eval #xx, yy.(xx > 2 & yy < 5 & xx < yy)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:eval {
1, 2, 3,
4, 5, 6,
7, 8, 9
}
```
%% Output
$\{1,2,3,4,5,6,7,8,9\}$
{1,2,3,4,5,6,7,8,9}
......
src/main/java/de/prob2/jupyter/CommandUtils.java
+ 21
− 52
View file @ cc86c232
......@@ -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;
}
}
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);
}
}
......
src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+ 3
− 2
View file @ cc86c232
......@@ -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));
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment