Skip to content
Snippets Groups Projects
Commit 16b727b1 authored by dgelessus's avatar dgelessus
Browse files

Fix missing source code for evaluation errors

parent cc86c232
No related branches found
No related tags found
No related merge requests found
Pipeline #88830 passed
Stage: test
Show whitespace changes
Inline Side-by-side
notebooks/tests/eval.ipynb
+ 14
− 11
View file @ 16b727b1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :eval :help :eval
``` ```
%% Output %% Output
``` ```
FORMULA FORMULA
// or // or
:eval FORMULA :eval FORMULA
``` ```
Evaluate a formula and display the result. Evaluate a formula and display the result.
Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`). Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).
If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command. If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.
FORMULA FORMULA
// or // or
:eval FORMULA :eval FORMULA
Evaluate a formula and display the result. Evaluate a formula and display the result.
Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`). Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).
If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command. If the formula is a $\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Expressions can be evaluated. Expressions can be evaluated.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
123 123
``` ```
%% Output %% Output
$123$ $123$
123 123
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
123 + 456 123 + 456
``` ```
%% Output %% Output
$579$ $579$
579 579
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1, 2} \/ {5, 6} {1, 2} \/ {5, 6}
``` ```
%% Output %% Output
$\{1,2,5,6\}$ $\{1,2,5,6\}$
{1,2,5,6} {1,2,5,6}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..5 1..5
``` ```
%% Output %% Output
$\{1,2,3,4,5\}$ $\{1,2,3,4,5\}$
{1,2,3,4,5} {1,2,3,4,5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
MAXINT MAXINT
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Solution variables are displayed. Solution variables are displayed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
#xx.(xx : NAT1 & xx mod 3 = 0) #xx.(xx : NAT1 & xx mod 3 = 0)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
#xx, yy.(xx > 2 & yy < 5 & xx < yy) #xx, yy.(xx > 2 & yy < 5 & xx < yy)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Various kinds of evaluation errors are displayed. Various kinds of evaluation errors are displayed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
unknown unknown \/ nonsense
``` ```
%% Output %% Output
Error from ProB: ERROR Error from ProB: ERROR
2 errors:
Error: Unknown identifier "unknown" (:1:0 to 1:7) Error: Unknown identifier "unknown" (:1:0 to 1:7)
// Source code not known unknown \/ nonsense
Error: Unknown identifier "nonsense" (:1:11 to 1:19)
unknown \/ nonsense
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({x | x > 0 & x mod 2 = 0}) card({x | x > 0 & x mod 2 = 0})
``` ```
%% Output %% Output
Error from ProB: UNKNOWN (enumeration warning) Error from ProB: UNKNOWN (enumeration warning)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2 mod -1 1 + (2 mod -1)
``` ```
%% Output %% Output
Error from ProB: NOT-WELL-DEFINED Error from ProB: NOT-WELL-DEFINED
Error: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8) Error: mod not defined for negative numbers: 2 mod-1 (:1:5 to 1:13)
// Source code not known 1 + (2 mod -1)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Expressions can be multiline. Expressions can be multiline.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ {
1, 2, 3, 1, 2, 3,
4, 5, 6, 4, 5, 6,
7, 8, 9 7, 8, 9
} }
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7,8,9\}$ $\{1,2,3,4,5,6,7,8,9\}$
{1,2,3,4,5,6,7,8,9} {1,2,3,4,5,6,7,8,9}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The `:eval` command is equivalent to entering a bare expression. The `:eval` command is equivalent to entering a bare expression.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:eval #xx, yy.(xx > 2 & yy < 5 & xx < yy) :eval #xx, yy.(xx > 2 & yy < 5 & xx < yy)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:eval { :eval {
1, 2, 3, 1, 2, 3,
4, 5, 6, 4, 5, 6,
7, 8, 9 7, 8, 9
} }
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7,8,9\}$ $\{1,2,3,4,5,6,7,8,9\}$
{1,2,3,4,5,6,7,8,9} {1,2,3,4,5,6,7,8,9}
......
notebooks/tests/let.ipynb
+ 12
− 6
View file @ 16b727b1
%% 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"? Error from ProB: ERROR
Error: Unknown identifier "n", did you mean "IN"? (:2:0 to 2:1)
LET hello BE hello={1,2,3,4,5,10} IN(
n
)END
%% 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" Error from ProB: ERROR
Error: Unknown identifier "hello" (:1:0 to 1:5)
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}
......
notebooks/tests/solve.ipynb
+ 9
− 8
View file @ 16b727b1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :solve :help :solve
``` ```
%% Output %% Output
``` ```
:solve SOLVER PREDICATE :solve SOLVER PREDICATE
``` ```
Solve a predicate with the specified solver. Solve a predicate with the specified solver.
The following solvers are currently available: The following solvers are currently available:
* `cvc4` * `cvc4`
* `dpllt` * `dpllt`
* `kodkod` * `kodkod`
* `prob` * `prob`
* `smt_supported_interpreter` * `smt_supported_interpreter`
* `z3` * `z3`
* `z3axm` * `z3axm`
* `z3cns` * `z3cns`
:solve SOLVER PREDICATE :solve SOLVER PREDICATE
Solve a predicate with the specified solver. Solve a predicate with the specified solver.
The following solvers are currently available: The following solvers are currently available:
* `cvc4` * `cvc4`
* `dpllt` * `dpllt`
* `kodkod` * `kodkod`
* `prob` * `prob`
* `smt_supported_interpreter` * `smt_supported_interpreter`
* `z3` * `z3`
* `z3axm` * `z3axm`
* `z3cns` * `z3cns`
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Different solvers can be used to solve a predicate. Different solvers can be used to solve a predicate.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob xx > 2 & yy < 5 & xx < yy :solve prob xx > 2 & yy < 5 & xx < yy
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve kodkod xx > 2 & yy < 5 & xx < yy :solve kodkod xx > 2 & yy < 5 & xx < yy
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy :solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy
``` ```
%% Output %% Output
Error from ProB: Unhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4427626972),0,procedure,:(z3interface,/(pop_frame,0)),0))) Error from ProB: Unhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4545727948),0,procedure,:(z3interface,/(pop_frame,0)),0)))
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 xx > 2 & yy < 5 & xx < yy :solve z3 xx > 2 & yy < 5 & xx < yy
``` ```
%% Output %% Output
Error from ProB: ProB reported Errors Error from ProB: ProB reported Errors
Internal error: Call for event start_solving failed. init_smt_supported_interpreter Internal error: Call for event start_solving failed. init_smt_supported_interpreter
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Machine variables can be used in `:solve` predicates. Machine variables can be used in `:solve` predicates.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE SolveTest MACHINE SolveTest
VARIABLES z VARIABLES z
INVARIANT z : MININT..MAXINT INVARIANT z : MININT..MAXINT
INITIALISATION z :: MININT..MAXINT INITIALISATION z :: MININT..MAXINT
END END
``` ```
%% Output %% Output
Loaded machine: SolveTest Loaded machine: SolveTest
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
z z
``` ```
%% Output %% Output
:eval: NOT-INITIALISED Error from ProB: NOT-INITIALISED
ProB returned no error messages.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init z = 2 :init z = 2
``` ```
%% Output %% Output
Executed operation: INITIALISATION() Executed operation: INITIALISATION()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
z z
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob x <= z & x >= z :solve prob x <= z & x >= z
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 2$ * $\mathit{x} = 2$
* $\mathit{z} = 2$ * $\mathit{z} = 2$
TRUE TRUE
Solution: Solution:
x = 2 x = 2
z = 2 z = 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob z /= 2 :solve prob z /= 2
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Local variables can be used in `:solve` predicates. Local variables can be used in `:solve` predicates.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let five 5 :let five 5
``` ```
%% Output %% Output
$5$ $5$
5 5
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob xx > 2 & yy < five & xx < yy :solve prob xx > 2 & yy < five & xx < yy
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve kodkod xx > 2 & yy < five & xx < yy :solve kodkod xx > 2 & yy < five & xx < yy
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xx} = 3$ * $\mathit{xx} = 3$
* $\mathit{yy} = 4$ * $\mathit{yy} = 4$
TRUE TRUE
Solution: Solution:
xx = 3 xx = 3
yy = 4 yy = 4
......
src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+ 5
− 3
View file @ 16b727b1
...@@ -5,6 +5,7 @@ import java.util.Collections; ...@@ -5,6 +5,7 @@ import java.util.Collections;
import com.google.inject.Inject; import com.google.inject.Inject;
import com.google.inject.Injector; import com.google.inject.Injector;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.FormulaExpand; import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement; import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector; import de.prob.statespace.AnimationSelector;
...@@ -65,9 +66,10 @@ public final class EvalCommand implements Command { ...@@ -65,9 +66,10 @@ public final class EvalCommand implements Command {
public @NotNull DisplayData run(final @NotNull ParsedArguments args) { public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class); final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND); final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND);
return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(formula, () -> return CommandUtils.withSourceCode(formula, () -> {
kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula)) final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula);
)); return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(aer));
});
} }
@Override @Override
......
src/main/java/de/prob2/jupyter/commands/LetCommand.java
+ 1
− 1
View file @ 16b727b1
...@@ -85,7 +85,7 @@ public final class LetCommand implements Command { ...@@ -85,7 +85,7 @@ public final class LetCommand implements Command {
if (evaluated instanceof EvalResult) { if (evaluated instanceof EvalResult) {
kernel.getVariables().put(name, ((EvalResult)evaluated).getValue()); kernel.getVariables().put(name, ((EvalResult)evaluated).getValue());
} }
return CommandUtils.displayDataForEvalResult(evaluated); return CommandUtils.withSourceCode(formula, () -> CommandUtils.displayDataForEvalResult(evaluated));
} }
@Override @Override
......
src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+ 4
− 2
View file @ 16b727b1
...@@ -89,8 +89,10 @@ public final class SolveCommand implements Command { ...@@ -89,8 +89,10 @@ public final class SolveCommand implements Command {
final IEvalElement predicate = kernel.parseFormula(args.get(PREDICATE_PARAM), FormulaExpand.EXPAND); final IEvalElement predicate = kernel.parseFormula(args.get(PREDICATE_PARAM), FormulaExpand.EXPAND);
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState()); final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
return CommandUtils.withSourceCode(predicate, () -> {
trace.getStateSpace().execute(cmd); trace.getStateSpace().execute(cmd);
return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(cmd.getValue())); return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(cmd.getValue()));
});
} }
@Override @Override
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment