From d7c9a23df952e03372b5b0e2be1b6d9c286ec3fd Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 8 Nov 2021 15:37:45 +0100
Subject: [PATCH] Fix local variables in Event-B mode
Event-B/Rodin does not support LET like ProB does, so we need to use
some workarounds to provide similar functionality in Event-B mode.
---
CHANGELOG.md | 1 +
notebooks/tests/let.ipynb | 171 ++++++++++++++++++
.../java/de/prob2/jupyter/CommandUtils.java | 27 ++-
.../java/de/prob2/jupyter/ProBKernel.java | 83 ++++++++-
.../prob2/jupyter/commands/AssertCommand.java | 4 +-
.../prob2/jupyter/commands/EvalCommand.java | 4 +-
.../de/prob2/jupyter/commands/LetCommand.java | 6 +-
.../prob2/jupyter/commands/SolveCommand.java | 2 +-
8 files changed, 291 insertions(+), 7 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1ca4148..205ba9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,7 @@
* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
* As a side effect, the inspection and code completion features now work better in a few edge cases.
* Fixed a bug where interrupting a command could make the kernel completely stop responding, requiring a manual restart.
+* Fixed syntax errors when using local variables (`:let`) in Event-B mode.
* Fixed the `:trace` command sometimes displaying transitions as `null`.
## [1.2.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.2.0-all.jar)
diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
index 5db7904..1b4533e 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -355,6 +355,177 @@
"source": [
"hello"
]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Local variables can be used in Event-B mode."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to Event-B (forced)"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language event_b"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5,10\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5,10}"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1..5 \\/ {10}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5,10\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5,10}"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":let hello 1..5 \\/ {10}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5,10\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5,10}"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "hello"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "hello = {}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "hello /= {}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{A} = \\{0,1\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tA = {0,1}"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card(A) = 2 & hello /= A"
+ ]
}
],
"metadata": {
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index 659e297..450b68b 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -47,6 +47,7 @@ public final class CommandUtils {
private static final @NotNull Pattern BODY_SPLIT_PATTERN = Pattern.compile("\\n");
public static final @NotNull Pattern ARG_SPLIT_PATTERN = Pattern.compile("\\s+");
private static final @NotNull Pattern B_IDENTIFIER_PATTERN = Pattern.compile("[A-Za-z][A-Za-z0-9_]*");
+ public static final @NotNull String JUPYTER_RESULT_VARIABLE_NAME = "__jUpYtEr_rEsUlT__";
private CommandUtils() {
super();
@@ -219,7 +220,7 @@ public final class CommandUtils {
withSourceCode(formula.getCode(), action);
}
- public static @NotNull String insertLetVariables(final @NotNull String code, final @NotNull Map<@NotNull String, @NotNull String> variables) {
+ public static @NotNull String insertClassicalBLetVariables(final @NotNull String code, final @NotNull Map<@NotNull String, @NotNull String> variables) {
if (variables.isEmpty()) {
return code;
} else {
@@ -230,6 +231,30 @@ public final class CommandUtils {
}
}
+ public static @NotNull String insertEventBPredicateLetVariables(final @NotNull String predicate, final @NotNull Map<@NotNull String, @NotNull String> variables) {
+ if (variables.isEmpty()) {
+ return predicate;
+ } else {
+ final String varNames = String.join(",", variables.keySet());
+ final PredicateBuilder varAssignments = new PredicateBuilder();
+ varAssignments.addMap(variables);
+ varAssignments.add(predicate);
+ return String.format("#%s.(\n%s\n)", varNames, varAssignments);
+ }
+ }
+
+ public static @NotNull String insertEventBExpressionLetVariables(final @NotNull String expression, final @NotNull Map<@NotNull String, @NotNull String> variables) {
+ if (variables.isEmpty()) {
+ return expression;
+ } else {
+ final String varNames = String.join(",", variables.keySet());
+ final PredicateBuilder varAssignments = new PredicateBuilder();
+ varAssignments.addMap(variables);
+ varAssignments.add(JUPYTER_RESULT_VARIABLE_NAME, expression);
+ return String.format("#%s.(\n%s\n)", varNames, varAssignments);
+ }
+ }
+
public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) {
final StringBuilder sb = new StringBuilder();
final StringBuilder sbMarkdown = new StringBuilder();
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index bbfbf75..d564bc9 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -34,12 +34,16 @@ import com.google.inject.Injector;
import com.google.inject.Singleton;
import de.prob.animator.ReusableAnimator;
+import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ClassicalB;
import de.prob.animator.domainobjects.ErrorItem;
+import de.prob.animator.domainobjects.EvalElementType;
+import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.EventB;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.exception.ProBError;
+import de.prob.model.eventb.EventBModel;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.StateSpace;
@@ -344,6 +348,17 @@ public final class ProBKernel extends BaseKernel {
this.setCurrentMachineDirectory(machineDirectory);
}
+ /**
+ * Return whether user-entered formulas are currently being parsed using Event-B syntax.
+ * This is true if the user has explicitly enabled Event-B mode,
+ * or when the default mode is used while an Event-B model is loaded.
+ *
+ * @return whether formulas are currently parsed as Event-B
+ */
+ public boolean isEventBMode() {
+ return this.getCurrentFormulaLanguage() == FormulaLanguage.EVENT_B || this.animationSelector.getCurrentTrace().getModel() instanceof EventBModel;
+ }
+
/**
* Parse the given formula code into an {@link IEvalElement}.
* The language used for parsing depends on the current formula language (see {@link #getCurrentFormulaLanguage()}.
@@ -381,7 +396,33 @@ public final class ProBKernel extends BaseKernel {
* @return the parsed formula
*/
public IEvalElement parseFormula(final String code, final FormulaExpand expand) {
- return this.parseFormulaWithoutLetVariables(CommandUtils.insertLetVariables(code, this.getVariables()), expand);
+ if (this.getVariables().isEmpty()) {
+ // Shortcut: if no local variables are defined,
+ // the code doesn't need to be changed at all.
+ return this.parseFormulaWithoutLetVariables(code, expand);
+ } else if (this.isEventBMode()) {
+ // Implementing local variables in Event-B mode is not straightforward,
+ // because Rodin does not support LET expressions/predicates
+ // like ProB does for classical B.
+ // For predicates,
+ // we can use an existential quantifier in place of LET.
+ // For expressions this is not possible,
+ // so as a workaround we construct a predicate with a new free variable equal to the expression.
+ // This helper predicate is unpacked again after evaluation.
+ final String predicateCode = CommandUtils.insertEventBPredicateLetVariables(code, this.getVariables());
+ final EventB predicate = (EventB)this.parseFormulaWithoutLetVariables(predicateCode, FormulaExpand.TRUNCATE);
+ if (predicate.getKind() == EvalElementType.PREDICATE) {
+ return predicate;
+ } else {
+ final String expressionAsPredicateCode = CommandUtils.insertEventBExpressionLetVariables(code, this.getVariables());
+ return this.parseFormulaWithoutLetVariables(expressionAsPredicateCode, FormulaExpand.TRUNCATE);
+ }
+ } else {
+ // Assume that we are using classical B syntax.
+ // This is the case for most other supported languages
+ // (the main exception is CSP).
+ return this.parseFormulaWithoutLetVariables(CommandUtils.insertClassicalBLetVariables(code, this.getVariables()), expand);
+ }
}
public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
@@ -402,6 +443,46 @@ public final class ProBKernel extends BaseKernel {
return new DisplayData(String.format("Executed operation: %s", op.getPrettyRep()));
}
+ /**
+ * Post-process an evaluation result returned by ProB.
+ * Currently this only handles some special cases when evaluating Event-B formulas while local variables are defined.
+ * In all other cases,
+ * the result is returned unmodified.
+ *
+ * @param aer the evaluation result to postprocess
+ * @return the processed evaluation result
+ */
+ public @NotNull AbstractEvalResult postprocessEvalResult(final @NotNull AbstractEvalResult aer) {
+ if (!this.getVariables().isEmpty() && this.isEventBMode() && aer instanceof EvalResult) {
+ final EvalResult result = (EvalResult)aer;
+
+ final Map<String, String> solutionValues = new HashMap<>(result.getSolutions());
+
+ final String resultValue;
+ if (result.getValue().equals(EvalResult.TRUE.getValue()) && result.getSolutions().containsKey(CommandUtils.JUPYTER_RESULT_VARIABLE_NAME)) {
+ // Special case for expressions rewritten to predicates by CommandUtils.insertEventBExpressionLetVariables:
+ // extract the special result variable and use it in place of the predicate result (TRUE).
+ resultValue = solutionValues.remove(CommandUtils.JUPYTER_RESULT_VARIABLE_NAME);
+ } else {
+ resultValue = result.getValue();
+ }
+
+ // Special case for predicates or expressions
+ // that had local variables inserted using an existential quantification
+ // (by insertEventBPredicateLetVariables or insertEventBExpressionLetVariables).
+ // ProB sometimes treats variables in a top-level existential quantification
+ // as if they were free variables
+ // and returns their values as part of the solution.
+ // We don't want this for local variables,
+ // so manually remove them from the solution again.
+ solutionValues.keySet().removeAll(this.getVariables().keySet());
+
+ return new EvalResult(resultValue, solutionValues);
+ }
+
+ return aer;
+ }
+
@Override
public @NotNull String getBanner() {
return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 1ba3378..31a2f55 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -70,7 +70,9 @@ public final class AssertCommand implements Command {
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.kernelProvider.get();
final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.TRUNCATE);
- final AbstractEvalResult result = CommandUtils.withSourceCode(formula, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula));
+ final AbstractEvalResult result = CommandUtils.withSourceCode(formula, () ->
+ kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+ );
if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
return CommandUtils.displayDataForEvalResult(EvalResult.TRUE);
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index bc6271f..1693bf0 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -65,7 +65,9 @@ public final class EvalCommand implements Command {
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND);
- return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(formula, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula)));
+ return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(formula, () ->
+ kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+ ));
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 0d0a059..1ee993d 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -70,9 +70,11 @@ public final class LetCommand implements Command {
final String name = args.get(NAME_PARAM);
final ProBKernel kernel = this.kernelProvider.get();
final IEvalElement formula = kernel.parseFormula(args.get(EXPRESSION_PARAM), FormulaExpand.EXPAND);
- final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula));
+ final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () ->
+ kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+ );
if (evaluated instanceof EvalResult) {
- kernel.getVariables().put(name, evaluated.toString());
+ kernel.getVariables().put(name, ((EvalResult)evaluated).getValue());
}
return CommandUtils.displayDataForEvalResult(evaluated);
}
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index c92210b..d8e59a3 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -90,7 +90,7 @@ public final class SolveCommand implements Command {
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
trace.getStateSpace().execute(cmd);
- return CommandUtils.displayDataForEvalResult(cmd.getValue());
+ return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(cmd.getValue()));
}
@Override
--
GitLab