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

Add support :let variables to more commands

Previously local variables could only be used in top-level expressions
(:eval).
parent 0f33ea07
Branches
Tags
No related merge requests found
Showing
with 933 additions and 182 deletions
%% Cell type:code id: tags:
``` prob
:help :browse
```
%% Output
```
:browse
```
Show information about the current state.
The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state.
:browse
Show information about the current state.
The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state.
%% Cell type:code id: tags:
``` prob
:help :exec
```
%% Output
```
:exec OPERATION [PREDICATE]
```
Execute an operation.
A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.
:exec OPERATION [PREDICATE]
Execute an operation.
A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.
%% Cell type:code id: tags:
``` prob
:help :constants
```
%% Output
```
:constants [PREDICATE]
```
Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
:constants [PREDICATE]
Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
%% Cell type:code id: tags:
``` prob
:help :init
```
%% Output
```
:init [PREDICATE]
```
Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
:init [PREDICATE]
Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: repl
Sets: (none)
Constants: (none)
Variables: (none)
Operations:
INITIALISATION()
%% Cell type:code id: tags:
``` prob
::load
MACHINE Counter
CONSTANTS min_value, max_value
PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
VARIABLES value
INVARIANT value : min_value..max_value
INITIALISATION value :: min_value..max_value
OPERATIONS
add(diff) = SELECT
value+diff : min_value..max_value
THEN
value := value+diff
END
END
```
%% Output
Loaded machine: Counter
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
SETUP_CONSTANTS()
SETUP_CONSTANTS()
SETUP_CONSTANTS()
SETUP_CONSTANTS()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%% Output
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
value
```
%% Output
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:constants min_value=5 & max_value=-5
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS with additional predicate
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate
%% Cell type:code id: tags:
``` prob
:constants min_value=-1 & max_value=2
```
%% Output
Machine constants set up using operation 2: $setup_constants()
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
INITIALISATION()
INITIALISATION()
INITIALISATION()
INITIALISATION()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%% Output
$\{-1,0,1,2\}$
{−1,0,1,2}
%% Cell type:code id: tags:
``` prob
value
```
%% Output
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:init value=-100
```
%% Output
Error from ProB: ProB reported Errors
Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)
// Source code not known
%% Cell type:code id: tags:
``` prob
:init value=2
```
%% Output
Machine initialised using operation 7: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
add(-3)
add(-2)
add(-1)
add(0)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
:exec add diff=-1
```
%% Output
Executed operation: add(-1)
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
add(-2)
add(-1)
add(0)
add(1)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
:stats
```
%% Output
**Explored States:** 4/9
**Transitions:** 16
Explored States: 4/9
Transitions: 16
%% Cell type:markdown id: tags:
Useful error messages are shown when an operation cannot be executed.
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.InitialiseCommand.run(InitialiseCommand.java:48)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
%% Cell type:code id: tags:
``` prob
:exec nope
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
%% Cell type:code id: tags:
``` prob
:exec add 1=0
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
java.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)
%% Cell type:code id: tags:
``` prob
::load
MACHINE NoConstants
VARIABLES z
INVARIANT z : MININT..MAXINT
INITIALISATION z :: {0, 1}
END
```
%% Output
Loaded machine: NoConstants
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
---------------------------------------------------------------------------
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)
at de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root
%% Cell type:code id: tags:
``` prob
:init z = -1
```
%% Output
Error from ProB: ProB reported Errors
Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)
// Source code not known
%% Cell type:markdown id: tags:
`SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Foo
CONSTANTS x
PROPERTIES x : MININT..MAXINT
VARIABLES y
INVARIANT y : MININT..MAXINT
INITIALISATION y :: MININT..MAXINT
END
```
%% Output
Loaded machine: Foo
%% Cell type:code id: tags:
``` prob
:exec SETUP_CONSTANTS x = 1
```
%% Output
Executed operation: $setup_constants()
%% Cell type:code id: tags:
``` prob
:exec INITIALISATION y = 2
```
%% Output
Executed operation: $initialise_machine()
%% Cell type:code id: tags:
``` prob
x
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
y
```
%% Output
$2$
2
%% Cell type:markdown id: tags:
Local variables can be used in operation predicates.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Counter
CONSTANTS min_value, max_value
PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
VARIABLES value
INVARIANT value : min_value..max_value
INITIALISATION value :: min_value..max_value
OPERATIONS
add(diff) = SELECT
value+diff : min_value..max_value
THEN
value := value+diff
END
END
```
%% Output
Loaded machine: Counter
%% Cell type:code id: tags:
``` prob
:let one 1
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
:let two 2
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
:constants min_value=-one & max_value=two
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%% Output
$\{-1,0,1,2\}$
{−1,0,1,2}
%% Cell type:code id: tags:
``` prob
:init value=one
```
%% Output
Machine initialised using operation 3: $initialise_machine()
%% Cell type:code id: tags:
``` prob
value
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
:exec add diff=-one
```
%% Output
Executed operation: add(-1)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
$0$
0
......
%% Cell type:code id: tags:
``` prob
:help :assert
```
%% Output
```
:assert PREDICATE
```
Ensure that the predicate is true, and show an error otherwise.
This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.
:assert PREDICATE
Ensure that the predicate is true, and show an error otherwise.
This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\mathit{FALSE}$ result as an error. If the result is $\mathit{TRUE}$, solutions for free variables (if any) are not displayed.
Only predicates and $\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.
%% Cell type:markdown id: tags:
Asserting a true predicate shows $\mathit{TRUE}$.
%% Cell type:code id: tags:
``` prob
:assert 1 = 1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:assert TRUE
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Asserting a predicate doesn't show any solutions.
%% Cell type:code id: tags:
``` prob
:assert x > 1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Asserting a false predicate shows an error.
%% Cell type:code id: tags:
``` prob
:assert 0 = 1
```
%% Output
:assert: Assertion is not true: FALSE
%% Cell type:code id: tags:
``` prob
:assert FALSE
```
%% Output
:assert: Assertion is not true: FALSE
%% Cell type:markdown id: tags:
Asserting something that isn't a predicate/boolean shows an error.
%% Cell type:code id: tags:
``` prob
:assert 123
```
%% Output
:assert: Assertion is not true: 123
%% Cell type:code id: tags:
``` prob
:assert {}
```
%% Output
:assert: Assertion is not true: ∅
%% Cell type:markdown id: tags:
Asserting a formula with errors shows an error.
%% Cell type:code id: tags:
``` prob
:assert 123 + {}
```
%% Output
:assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'
%% Cell type:markdown id: tags:
Local variables can be used in assertions.
%% Cell type:code id: tags:
``` prob
:let trü TRUE
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:let flasche FALSE
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
:assert trü
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:assert flasche
```
%% Output
:assert: Assertion is not true: FALSE
......
This diff is collapsed.
%% Cell type:code id: tags:
``` prob
:help :let
```
%% Output
```
:let NAME EXPR
```
Evaluate an expression and store it in a local variable.
The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.
**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
Evaluate an expression and store it in a local variable.
The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.
**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:
``` prob
:help :unlet
```
%% Output
```
:unlet NAME
```
Remove a local variable.
:unlet NAME
Remove a local variable.
%% Cell type:code id: tags:
``` prob
:let hello 1..5 \/ {10}
```
%% Output
$\{1,2,3,4,5,10\}$
{1,2,3,4,5,10}
%% Cell type:code id: tags:
``` prob
hello
```
%% Output
$\{1,2,3,4,5,10\}$
{1,2,3,4,5,10}
%% Cell type:code id: tags:
``` prob
:let n 2
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
n
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
{x | x : hello & x mod n = 0}
```
%% Output
$\{2,4,10\}$
{2,4,10}
%% Cell type:code id: tags:
``` prob
:unlet n
```
%% Cell type:code id: tags:
``` prob
n
```
%% Output
:eval: Computation not completed: Unknown identifier "n", the possible completion is "not"
%% Cell type:markdown id: tags:
Local variables can be used when setting a local variable.
%% Cell type:code id: tags:
``` prob
:let n 1
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
:let m n + 1
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
:let m m + 1
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
m
```
%% Output
$3$
3
......
%% Cell type:code id: tags:
``` prob
:help :solve
```
%% Output
```
:solve SOLVER PREDICATE
```
Solve a predicate with the specified solver.
The following solvers are currently available:
* `cvc4`
* `kodkod`
* `prob`
* `smt_supported_interpreter`
* `z3`
:solve SOLVER PREDICATE
Solve a predicate with the specified solver.
The following solvers are currently available:
* `cvc4`
* `kodkod`
* `prob`
* `smt_supported_interpreter`
* `z3`
%% Cell type:markdown id: tags:
Different solvers can be used to solve a predicate.
%% Cell type:code id: tags:
``` prob
:solve prob xx > 2 & yy < 5 & xx < yy
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:solve kodkod xx > 2 & yy < 5 & xx < yy
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy
```
%% Output
Error from ProB: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4531520732),0,procedure,:(z3interface,/(pop_frame,0)),0)))
Error from ProB: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4401885196),0,procedure,:(z3interface,/(pop_frame,0)),0)))
%% Cell type:code id: tags:
``` prob
:solve z3 xx > 2 & yy < 5 & xx < yy
```
%% Output
Error from ProB: ProB reported Errors
Internal error: Call for event start_solving failed. init_interface(z3)
%% Cell type:markdown id: tags:
Machine variables can be used in `:solve` predicates.
%% Cell type:code id: tags:
``` prob
::load
MACHINE SolveTest
VARIABLES z
INVARIANT z : MININT..MAXINT
INITIALISATION z :: MININT..MAXINT
END
```
%% Output
Loaded machine: SolveTest
%% Cell type:code id: tags:
``` prob
z
```
%% Output
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:init z = 2
```
%% Output
Machine initialised using operation 0: $initialise_machine()
%% Cell type:code id: tags:
``` prob
z
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
:solve prob x <= z & x >= z
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 2$
* $\mathit{z} = 2$
TRUE
Solution:
x = 2
z = 2
%% Cell type:code id: tags:
``` prob
:solve prob z /= 2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Local variables can be used in `:solve` predicates.
%% Cell type:code id: tags:
``` prob
:let five 5
```
%% Output
$5$
5
%% Cell type:code id: tags:
``` prob
:solve prob xx > 2 & yy < five & xx < yy
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:solve kodkod xx > 2 & yy < five & xx < yy
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xx} = 3$
* $\mathit{yy} = 4$
TRUE
Solution:
xx = 3
yy = 4
......
%% Cell type:code id: tags:
``` prob
:help :table
```
%% Output
```
:table EXPRESSION
```
Display an expression as a table.
Although any expression is accepted, this command is most useful for sets of tuples.
:table EXPRESSION
Display an expression as a table.
Although any expression is accepted, this command is most useful for sets of tuples.
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 0: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:table {1, 2, 3, 4}
```
%% Output
|Elements|
|---|
|$1$|
|$2$|
|$3$|
|$4$|
Elements
1
2
3
4
%% Cell type:code id: tags:
``` prob
:table [1, 2, 3, 4]
```
%% Output
|prj1|prj2|
|---|---|
|$1$|$1$|
|$2$|$2$|
|$3$|$3$|
|$4$|$4$|
prj1 prj2
1 1
2 2
3 3
4 4
%% Cell type:code id: tags:
``` prob
:table {(1, 2, 3), (4, 5, 6), (7, 8, 9)}
```
%% Output
|prj11|prj12|prj2|
|---|---|---|
|$1$|$2$|$3$|
|$4$|$5$|$6$|
|$7$|$8$|$9$|
prj11 prj12 prj2
1 2 3
4 5 6
7 8 9
%% Cell type:code id: tags:
``` prob
:table {({}, {})}
```
%% Output
|prj1|prj2|
|---|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$\emptyset$|
prj1 prj2
{} {}
%% Cell type:code id: tags:
``` prob
:table {({1|->2, 3|->4}, {5|->6, 7|->8}), ({2|->1, 4|->3}, {6|->5, 8|->7})}
```
%% Output
|prj1|prj2|
|---|---|
|$\{(1\mapsto 2),(3\mapsto 4)\}$|$\{(5\mapsto 6),(7\mapsto 8)\}$|
|$\{(2\mapsto 1),(4\mapsto 3)\}$|$\{(6\mapsto 5),(8\mapsto 7)\}$|
prj1 prj2
{(1|->2),(3|->4)} {(5|->6),(7|->8)}
{(2|->1),(4|->3)} {(6|->5),(8|->7)}
%% Cell type:markdown id: tags:
Local variables can be used in expressions visualised as table.
%% Cell type:code id: tags:
``` prob
:let thing {(1, 2, 3), (4, 5, 6), (7, 8, 9)}
```
%% Output
$\{(1\mapsto 2\mapsto 3),(4\mapsto 5\mapsto 6),(7\mapsto 8\mapsto 9)\}$
{(1↦2↦3),(4↦5↦6),(7↦8↦9)}
%% Cell type:code id: tags:
``` prob
:table thing
```
%% Output
|prj11|prj12|prj2|
|---|---|---|
|$1$|$2$|$3$|
|$4$|$5$|$6$|
|$7$|$8$|$9$|
prj11 prj12 prj2
1 2 3
4 5 6
7 8 9
......
%% Cell type:code id: tags:
``` prob
:help :type
```
%% Output
```
:type FORMULA
```
Display the type of a formula.
The returned types are *not* standard B types. They are human-readable, but cannot be used in code.
:type FORMULA
Display the type of a formula.
The returned types are *not* standard B types. They are human-readable, but cannot be used in code.
%% Cell type:markdown id: tags:
`:type` works on expressions.
%% Cell type:code id: tags:
``` prob
:type 1
```
%% Output
integer
INTEGER
%% Cell type:code id: tags:
``` prob
:type {}
```
%% Output
set(any)
POW(?)
%% Cell type:code id: tags:
``` prob
:type {1, 2, 3}
```
%% Output
set(integer)
POW(INTEGER)
%% Cell type:code id: tags:
``` prob
:type 1..5
```
%% Output
set(integer)
POW(INTEGER)
%% Cell type:code id: tags:
``` prob
:type [1, 2, 3]
```
%% Output
seq(integer)
seq(INTEGER)
%% Cell type:code id: tags:
``` prob
:type {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}
```
%% Output
set(set(couple(couple(integer,integer),integer)))
POW(((INTEGER*INTEGER)<->INTEGER))
%% Cell type:markdown id: tags:
`:type` works on predicates.
%% Cell type:code id: tags:
``` prob
:type 1 = 1
```
%% Output
pred
predicate
%% Cell type:code id: tags:
``` prob
:type #x.(x : INT & x > 1)
```
%% Output
pred
predicate
%% Cell type:markdown id: tags:
`:type` displays type errors.
%% Cell type:code id: tags:
``` prob
:type {1, TRUE, "string", {}}
```
%% Output
Error from ProB: Type errors in formula
3 errors:
Error: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)
// Source code not known
Error: Type mismatch: Expected INTEGER, but was STRING in '"string"' (:1:10 to 1:16)
Error: Type mismatch: Expected INTEGER, but was STRING in '"string"' (:1:10 to 1:18)
// Source code not known
Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)
// Source code not known
%% Cell type:code id: tags:
``` prob
:type 1 + {}
```
%% Output
Error from ProB: Type errors in formula
Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)
// Source code not known
%% Cell type:markdown id: tags:
Local variables can be passed to `:type`.
%% Cell type:code id: tags:
``` prob
:let thing {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}
```
%% Output
$\{\{(1\mapsto 2\mapsto 3),(4\mapsto 5\mapsto 6)\},\{(7\mapsto 8\mapsto 9)\}\}$
{{(1↦2↦3),(4↦5↦6)},{(7↦8↦9)}}
%% Cell type:code id: tags:
``` prob
:type thing
```
%% Output
POW(((INTEGER*INTEGER)<->INTEGER))
%% Cell type:code id: tags:
``` prob
:type thing, 123
```
%% Output
POW(((INTEGER*INTEGER)<->INTEGER))*INTEGER
......
......@@ -495,4 +495,8 @@ public final class ProBKernel extends BaseKernel {
throw e2;
}
}
public @NotNull String insertLetVariables(final @NotNull String code) {
return CommandUtils.insertLetVariables(code, this.getVariables());
}
}
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
......@@ -17,12 +18,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class AssertCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private AssertCommand(final @NotNull AnimationSelector animationSelector) {
private AssertCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -44,7 +47,8 @@ public final class AssertCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final AbstractEvalResult result = CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE));
final String code = this.kernelProvider.get().insertLetVariables(argString);
final AbstractEvalResult result = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.TRUNCATE));
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);
......
......@@ -8,6 +8,7 @@ import java.util.List;
import java.util.Map;
import java.util.NoSuchElementException;
import java.util.Set;
import java.util.StringJoiner;
import java.util.function.Supplier;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
......@@ -128,6 +129,20 @@ public final class CommandUtils {
});
}
public static @NotNull String insertLetVariables(final @NotNull String code, final @NotNull Map<@NotNull String, @NotNull String> variables) {
if (variables.isEmpty()) {
return code;
} else {
final StringJoiner varNames = new StringJoiner(",");
final StringJoiner varAssignments = new StringJoiner("&");
variables.forEach((name, value) -> {
varNames.add(name);
varAssignments.add(name + "=(" + value + ')');
});
return String.format("LET %s BE %s IN(%s)END", varNames, varAssignments, code);
}
}
public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) {
final StringBuilder sb = new StringBuilder();
final StringBuilder sbMarkdown = new StringBuilder();
......
......@@ -4,11 +4,13 @@ import java.util.Collections;
import java.util.List;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -17,12 +19,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ConstantsCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private ConstantsCommand(final @NotNull AnimationSelector animationSelector) {
private ConstantsCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -44,7 +48,12 @@ public final class ConstantsCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate = argString.isEmpty() ? "1=1" : argString;
final String predicate;
if (argString.isEmpty()) {
predicate = "1=1";
} else {
predicate = this.kernelProvider.get().insertLetVariables(argString);
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
assert !ops.isEmpty();
final Transition op = ops.get(0);
......
......@@ -10,6 +10,7 @@ import java.util.stream.Collectors;
import java.util.stream.Stream;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.command.GetAllDotCommands;
import de.prob.animator.command.GetSvgForVisualizationCommand;
......@@ -18,7 +19,7 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
......@@ -28,12 +29,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class DotCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private DotCommand(final @NotNull AnimationSelector animationSelector) {
private DotCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -76,11 +79,13 @@ public final class DotCommand implements Command {
assert !split.isEmpty();
final String command = split.get(0);
final List<IEvalElement> args;
final String code;
if (split.size() > 1) {
final String code = split.get(1);
code = this.kernelProvider.get().insertLetVariables(split.get(1));
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND));
args = Collections.singletonList(formula);
} else {
code = null;
args = Collections.emptyList();
}
......@@ -101,8 +106,8 @@ public final class DotCommand implements Command {
final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), args);
// Provide source code (if any) to error highlighter
final Runnable execute = () -> trace.getStateSpace().execute(cmd2);
if (split.size() > 1) {
CommandUtils.withSourceCode(split.get(1), execute);
if (code != null) {
CommandUtils.withSourceCode(code, execute);
} else {
execute.run();
}
......
package de.prob2.jupyter.commands;
import java.util.Map;
import java.util.StringJoiner;
import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
......@@ -47,19 +43,7 @@ public final class EvalCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
final String code;
if (variables.isEmpty()) {
code = argString;
} else {
final StringJoiner varNames = new StringJoiner(",");
final StringJoiner varAssignments = new StringJoiner("&");
variables.forEach((name, value) -> {
varNames.add(name);
varAssignments.add(name + "=(" + value + ')');
});
code = String.format("LET %s BE %s IN(%s)END", varNames, varAssignments, argString);
}
final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(argString);
return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.EXPAND)));
}
......
......@@ -5,11 +5,13 @@ import java.util.List;
import java.util.stream.Collectors;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -18,12 +20,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ExecCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private ExecCommand(final @NotNull AnimationSelector animationSelector) {
private ExecCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -49,7 +53,12 @@ public final class ExecCommand implements Command {
final Trace trace = this.animationSelector.getCurrentTrace();
final String translatedOpName = CommandUtils.unprettyOperationName(split.get(0));
final String predicate = split.size() < 2 ? "1=1" : split.get(1);
final String predicate;
if (split.size() < 2) {
predicate = "1=1";
} else {
predicate = this.kernelProvider.get().insertLetVariables(split.get(1));
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
assert !ops.isEmpty();
final Transition op = ops.get(0);
......
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -14,12 +16,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class FindCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private FindCommand(final @NotNull AnimationSelector animationSelector) {
private FindCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -41,8 +45,9 @@ public final class FindCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final Trace newTrace = CommandUtils.withSourceCode(argString, () -> {
final IEvalElement pred = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
final String code = this.kernelProvider.get().insertLetVariables(argString);
final Trace newTrace = CommandUtils.withSourceCode(code, () -> {
final IEvalElement pred = trace.getModel().parseFormula(code, FormulaExpand.EXPAND);
return trace.getStateSpace().getTraceToState(pred);
});
this.animationSelector.changeCurrentAnimation(newTrace);
......
......@@ -4,11 +4,13 @@ import java.util.Collections;
import java.util.List;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -17,12 +19,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class InitialiseCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private InitialiseCommand(final @NotNull AnimationSelector animationSelector) {
private InitialiseCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -44,7 +48,12 @@ public final class InitialiseCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate = argString.isEmpty() ? "1=1" : argString;
final String predicate;
if (argString.isEmpty()) {
predicate = "1=1";
} else {
predicate = this.kernelProvider.get().insertLetVariables(argString);
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
assert !ops.isEmpty();
final Transition op = ops.get(0);
......
......@@ -3,7 +3,7 @@ package de.prob2.jupyter.commands;
import java.util.List;
import com.google.inject.Inject;
import com.google.inject.Injector;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
......@@ -19,14 +19,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LetCommand implements Command {
private final @NotNull Injector injector;
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
public LetCommand(final @NotNull Injector injector, final @NotNull AnimationSelector animationSelector) {
public LetCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.injector = injector;
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -52,10 +52,10 @@ public final class LetCommand implements Command {
throw new UserErrorException("Expected 2 arguments, not " + split.size());
}
final String name = split.get(0);
final String expr = split.get(1);
final String expr = this.kernelProvider.get().insertLetVariables(split.get(1));
final AbstractEvalResult evaluated = CommandUtils.withSourceCode(expr, () -> this.animationSelector.getCurrentTrace().evalCurrent(expr, FormulaExpand.EXPAND));
if (evaluated instanceof EvalResult) {
this.injector.getInstance(ProBKernel.class).getVariables().put(name, evaluated.toString());
this.kernelProvider.get().getVariables().put(name, evaluated.toString());
}
return CommandUtils.displayDataForEvalResult(evaluated);
}
......
......@@ -6,6 +6,7 @@ import java.util.Map;
import java.util.stream.Collectors;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.command.CbcSolveCommand;
import de.prob.animator.domainobjects.FormulaExpand;
......@@ -13,6 +14,7 @@ import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
......@@ -25,12 +27,14 @@ public final class SolveCommand implements Command {
private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private SolveCommand(final @NotNull AnimationSelector animationSelector) {
private SolveCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -67,7 +71,7 @@ public final class SolveCommand implements Command {
if (solver == null) {
throw new UserErrorException("Unknown solver: " + split.get(0));
}
final String code = split.get(1);
final String code = this.kernelProvider.get().insertLetVariables(split.get(1));
final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
......
......@@ -5,6 +5,7 @@ import java.util.List;
import java.util.stream.Collectors;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.command.GetAllTableCommands;
import de.prob.animator.command.GetTableForVisualizationCommand;
......@@ -15,6 +16,7 @@ import de.prob.animator.domainobjects.TableData;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -23,12 +25,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TableCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private TableCommand(final @NotNull AnimationSelector animationSelector) {
private TableCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -50,7 +54,8 @@ public final class TableCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND));
final String code = this.kernelProvider.get().insertLetVariables(argString);
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState());
trace.getStateSpace().execute(cmd1);
......
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import com.google.inject.Provider;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
......@@ -8,6 +9,7 @@ import de.prob.animator.domainobjects.TypeCheckResult;
import de.prob.exception.ProBError;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -16,12 +18,14 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TypeCommand implements Command {
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@Inject
private TypeCommand(final @NotNull AnimationSelector animationSelector) {
private TypeCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
super();
this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
......@@ -43,7 +47,8 @@ public final class TypeCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND));
final String code = this.kernelProvider.get().insertLetVariables(argString);
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
if (result.isOk()) {
return new DisplayData(result.getType());
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment