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

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.
parent ed137199
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tests/let.ipynb
+ 2
− 14
View file @ 56a272dd
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :let :help :let
``` ```
%% Output %% Output
``` ```
:let NAME EXPR :let NAME EXPR
:let NAME=EXPR :let NAME=EXPR
``` ```
Evaluate an expression and store it in a local variable. Evaluate an expression and store it in a local variable.
The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine. The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.
Variables created by `:let` are discarded when a new machine is loaded (or the current machine is reloaded). The `:unlet` command can also be used to manually remove local variables. Variables created by `:let` are discarded when a new machine is loaded (or the current machine is reloaded). The `:unlet` command can also be used to manually remove local variables.
**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues. **Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.
:let NAME EXPR :let NAME EXPR
:let NAME=EXPR :let NAME=EXPR
Evaluate an expression and store it in a local variable. Evaluate an expression and store it in a local variable.
The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine. The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.
Variables created by `:let` are discarded when a new machine is loaded (or the current machine is reloaded). The `:unlet` command can also be used to manually remove local variables. Variables created by `:let` are discarded when a new machine is loaded (or the current machine is reloaded). The `:unlet` command can also be used to manually remove local variables.
**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues. **Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :unlet :help :unlet
``` ```
%% Output %% Output
``` ```
:unlet NAME :unlet NAME
``` ```
Remove a local variable. Remove a local variable.
:unlet NAME :unlet NAME
Remove a local variable. Remove a local variable.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let hello 1..5 \/ {10} :let hello 1..5 \/ {10}
``` ```
%% Output %% Output
$\{1,2,3,4,5,10\}$ $\{1,2,3,4,5,10\}$
{1,2,3,4,5,10} {1,2,3,4,5,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
hello hello
``` ```
%% Output %% Output
$\{1,2,3,4,5,10\}$ $\{1,2,3,4,5,10\}$
{1,2,3,4,5,10} {1,2,3,4,5,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let n 2 :let n 2
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
n n
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x : hello & x mod n = 0} {x | x : hello & x mod n = 0}
``` ```
%% Output %% Output
$\{2,4,10\}$ $\{2,4,10\}$
{2,4,10} {2,4,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet n :unlet n
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
n n
``` ```
%% Output %% Output
:eval: Computation not completed: Unknown identifier "n", did you mean "IN"? :eval: Computation not completed: Unknown identifier "n", did you mean "IN"?
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Local variables can be used when setting a local variable. Local variables can be used when setting a local variable.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let n 1 :let n 1
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let m n + 1 :let m n + 1
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let m m + 1 :let m m + 1
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
m m
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Local variables are not persisted when a new machine is loaded. Local variables are not persisted when a new machine is loaded.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Empty MACHINE Empty
END END
``` ```
%% Output %% Output
Loaded machine: Empty Loaded machine: Empty
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
hello hello
``` ```
%% Output %% Output
:eval: Computation not completed: Unknown identifier "hello" :eval: Computation not completed: Unknown identifier "hello"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Local variables can be assigned with or without `=`. Local variables can be assigned with or without `=`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let x 1 :let x 1
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let y=2 :let y=2
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:assert x + 1 = y :assert x + 1 = y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let X {x | x : 0..10 & x mod 2 = 0} :let X {x | x : 0..10 & x mod 2 = 0}
``` ```
%% Output %% Output
$\{0,2,4,6,8,10\}$ $\{0,2,4,6,8,10\}$
{0,2,4,6,8,10} {0,2,4,6,8,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let Y={x | x : 0..10 & x mod 2 = 0} :let Y={x | x : 0..10 & x mod 2 = 0}
``` ```
%% Output %% Output
$\{0,2,4,6,8,10\}$ $\{0,2,4,6,8,10\}$
{0,2,4,6,8,10} {0,2,4,6,8,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
X = Y X = Y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 1$
* $\mathit{X} = \{0,2,4,6,8,10\}$
* $\mathit{y} = 2$
* $\mathit{Y} = \{0,2,4,6,8,10\}$
TRUE TRUE
Solution:
x = 1
X = {0,2,4,6,8,10}
y = 2
Y = {0,2,4,6,8,10}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Local variables can be used in Event-B mode. Local variables can be used in Event-B mode.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:language event_b :language event_b
``` ```
%% Output %% Output
Changed language for user input to Event-B (forced) Changed language for user input to Event-B (forced)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..5 \/ {10} 1..5 \/ {10}
``` ```
%% Output %% Output
$\{1,2,3,4,5,10\}$ $\{1,2,3,4,5,10\}$
{1,2,3,4,5,10} {1,2,3,4,5,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let hello 1..5 \/ {10} :let hello 1..5 \/ {10}
``` ```
%% Output %% Output
$\{1,2,3,4,5,10\}$ $\{1,2,3,4,5,10\}$
{1,2,3,4,5,10} {1,2,3,4,5,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
hello hello
``` ```
%% Output %% Output
$\{1,2,3,4,5,10\}$ $\{1,2,3,4,5,10\}$
{1,2,3,4,5,10} {1,2,3,4,5,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
hello = {} hello = {}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
hello /= {} hello /= {}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(A) = 2 & hello /= A card(A) = 2 & hello /= A
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{A} = \{0,1\}$ * $\mathit{A} = \{0,1\}$
TRUE TRUE
Solution: Solution:
A = {0,1} A = {0,1}
......
src/main/java/de/prob2/jupyter/ProBKernel.java
+ 4
− 3
View file @ 56a272dd
...@@ -445,7 +445,8 @@ public final class ProBKernel extends BaseKernel { ...@@ -445,7 +445,8 @@ public final class ProBKernel extends BaseKernel {
/** /**
* Post-process an evaluation result returned by ProB. * 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, * In all other cases,
* the result is returned unmodified. * the result is returned unmodified.
* *
...@@ -453,13 +454,13 @@ public final class ProBKernel extends BaseKernel { ...@@ -453,13 +454,13 @@ public final class ProBKernel extends BaseKernel {
* @return the processed evaluation result * @return the processed evaluation result
*/ */
public @NotNull AbstractEvalResult postprocessEvalResult(final @NotNull AbstractEvalResult aer) { 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 EvalResult result = (EvalResult)aer;
final Map<String, String> solutionValues = new HashMap<>(result.getSolutions()); final Map<String, String> solutionValues = new HashMap<>(result.getSolutions());
final String resultValue; 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: // 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). // extract the special result variable and use it in place of the predicate result (TRUE).
resultValue = solutionValues.remove(CommandUtils.JUPYTER_RESULT_VARIABLE_NAME); resultValue = solutionValues.remove(CommandUtils.JUPYTER_RESULT_VARIABLE_NAME);
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment