-
- Downloads
Allow spaces around equals sign in :let
%% 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}$ | ||
TRUE | TRUE | ||
%% 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} | ||
... | ... |
Please register or sign in to comment