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

Add :assert command

parent 1cc75071
No related branches found
No related tags found
No related merge requests found
%% Cell type:code id: tags:
``` prob
:help :assert
```
%% Output
```
:assert PREDICATE
```
Ensure that the predicate is true, and show an error otherwise.
:assert PREDICATE
Ensure that the predicate is true, and show an error otherwise.
%% Cell type:markdown id: tags:
Asserting a true predicate doesn't show anything.
%% Cell type:code id: tags:
``` prob
:assert 1 = 1
```
%% Cell type:code id: tags:
``` prob
:assert 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 '{}'
......@@ -18,6 +18,7 @@ import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.commands.AssertCommand;
import de.prob2.jupyter.commands.BrowseCommand;
import de.prob2.jupyter.commands.Command;
import de.prob2.jupyter.commands.CommandExecutionException;
......@@ -146,6 +147,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
this.commands.put(":initialise", injector.getInstance(InitialiseCommand.class));
this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
this.commands.put(":assert", injector.getInstance(AssertCommand.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));
......
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import io.github.spencerpark.jupyter.kernel.display.mime.MIMEType;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class AssertCommand implements Command {
private final @NotNull AnimationSelector animationSelector;
@Inject
private AssertCommand(final @NotNull AnimationSelector animationSelector) {
super();
this.animationSelector = animationSelector;
}
@Override
public @NotNull String getSyntax() {
return ":assert PREDICATE";
}
@Override
public @NotNull String getShortHelp() {
return "Ensure that the predicate is true, and show an error otherwise.";
}
@Override
public @Nullable DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
final AbstractEvalResult result = this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE);
if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
return null;
}
final DisplayData displayData;
try {
displayData = CommandUtils.displayDataForEvalResult(result);
} catch (final UserErrorException e) {
throw new UserErrorException("Error while evaluating assertion: " + e.getMessage());
}
throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN));
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment