From 56a272ddade3ceb5f2108be63de14bb58c2d4652 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 8 Nov 2021 16:17:26 +0100
Subject: [PATCH] Remove let variables from solution outside of Event-B mode
too
In some cases, ProB apparently "unwraps" LET predicates as well,
not just existential quantifications.
---
notebooks/tests/let.ipynb | 16 ++--------------
src/main/java/de/prob2/jupyter/ProBKernel.java | 7 ++++---
2 files changed, 6 insertions(+), 17 deletions(-)
diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
index 42303a0..9315c64 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -488,22 +488,10 @@
{
"data": {
"text/markdown": [
- "$\\mathit{TRUE}$\n",
- "\n",
- "**Solution:**\n",
- "* $\\mathit{x} = 1$\n",
- "* $\\mathit{X} = \\{0,2,4,6,8,10\\}$\n",
- "* $\\mathit{y} = 2$\n",
- "* $\\mathit{Y} = \\{0,2,4,6,8,10\\}$"
+ "$\\mathit{TRUE}$"
],
"text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = 1\n",
- "\tX = {0,2,4,6,8,10}\n",
- "\ty = 2\n",
- "\tY = {0,2,4,6,8,10}"
+ "TRUE"
]
},
"execution_count": 21,
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index d564bc9..bcff44a 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -445,7 +445,8 @@ public final class ProBKernel extends BaseKernel {
/**
* 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.
+ * Currently this only handles some special cases when local variables are defined,
+ * especially in Event-B mode.
* In all other cases,
* the result is returned unmodified.
*
@@ -453,13 +454,13 @@ public final class ProBKernel extends BaseKernel {
* @return the processed evaluation result
*/
public @NotNull AbstractEvalResult postprocessEvalResult(final @NotNull AbstractEvalResult aer) {
- if (!this.getVariables().isEmpty() && this.isEventBMode() && aer instanceof EvalResult) {
+ if (!this.getVariables().isEmpty() && 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)) {
+ if (this.isEventBMode() && 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);
--
GitLab