Skip to content
GitLab
Commit bc7eafab authored by dgelessus's avatar dgelessus
Browse files

Display pretty operation names in operation execution output

parent 24839b33
Pipeline #42289 passed with stage
in 6 minutes and 34 seconds
Hide whitespace changes
Inline Side-by-side
notebooks/tests/animate.ipynb
View file @ bc7eafab
......@@ -281,7 +281,7 @@
{
"data": {
"text/plain": [
"Executed operation: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 11,
......@@ -391,7 +391,7 @@
{
"data": {
"text/plain": [
"Executed operation: $initialise_machine()"
"Executed operation: INITIALISATION()"
]
},
"execution_count": 16,
......@@ -734,7 +734,7 @@
{
"data": {
"text/plain": [
"Executed operation: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 31,
......@@ -754,7 +754,7 @@
{
"data": {
"text/plain": [
"Executed operation: $initialise_machine()"
"Executed operation: INITIALISATION()"
]
},
"execution_count": 32,
......@@ -906,7 +906,7 @@
{
"data": {
"text/plain": [
"Executed operation: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 38,
......@@ -949,7 +949,7 @@
{
"data": {
"text/plain": [
"Executed operation: $initialise_machine()"
"Executed operation: INITIALISATION()"
]
},
"execution_count": 40,
......
%% Cell type:code id: tags:
``` prob
:help :browse
```
%%%% Output: execute_result
```
: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 enabled operations (and possible parameter values) 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 enabled operations (and possible parameter values) in the current state.
%% Cell type:code id: tags:
``` prob
:help :exec
```
%%%% Output: execute_result
```
:exec OPERATION [PREDICATE]
```
Execute an operation.
The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.
If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.
:exec OPERATION [PREDICATE]
Execute an operation.
The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.
If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.
%% Cell type:code id: tags:
``` prob
:help :constants
```
%%%% Output: execute_result
```
: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: execute_result
```
: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: execute_result
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: execute_result
Loaded machine: Counter
%% Cell type:code id: tags:
``` prob
:browse
```
%%%% Output: execute_result
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: error
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
value
```
%%%% Output: error
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:constants min_value=5 & max_value=-5
```
%%%% Output: error
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: execute_result
Executed operation: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:browse
```
%%%% Output: execute_result
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: execute_result
$\{-1,0,1,2\}$
{−1,0,1,2}
%% Cell type:code id: tags:
``` prob
value
```
%%%% Output: error
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:init value=-100
```
%%%% Output: error
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: execute_result
Executed operation: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:code id: tags:
``` prob
:browse
```
%%%% Output: execute_result
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: execute_result
$2$
2
%% Cell type:code id: tags:
``` prob
:exec add diff=-1
```
%%%% Output: execute_result
Executed operation: add(-1)
%% Cell type:code id: tags:
``` prob
:browse
```
%%%% Output: execute_result
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: execute_result
$1$
1
%% Cell type:code id: tags:
``` prob
:stats
```
%%%% Output: execute_result
**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: error
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS
%% Cell type:code id: tags:
``` prob
:init
```
%%%% Output: error
java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION
%% Cell type:code id: tags:
``` prob
:exec nope
```
%%%% Output: error
java.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope
%% Cell type:code id: tags:
``` prob
:exec add 1=0
```
%%%% Output: error
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: execute_result
Loaded machine: NoConstants
%% Cell type:code id: tags:
``` prob
:constants
```
%%%% Output: error
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
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: execute_result
Loaded machine: Foo
%% Cell type:code id: tags:
``` prob
:exec SETUP_CONSTANTS x = 1
```
%%%% Output: execute_result
Executed operation: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:exec INITIALISATION y = 2
```
%%%% Output: execute_result
Executed operation: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:code id: tags:
``` prob
x
```
%%%% Output: execute_result
$1$
1
%% Cell type:code id: tags:
``` prob
y
```
%%%% Output: execute_result
$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: execute_result
Loaded machine: Counter
%% Cell type:code id: tags:
``` prob
:let one 1
```
%%%% Output: execute_result
$1$
1
%% Cell type:code id: tags:
``` prob
:let two 2
```
%%%% Output: execute_result
$2$
2
%% Cell type:code id: tags:
``` prob
:constants min_value=-one & max_value=two
```
%%%% Output: execute_result
Executed operation: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%%%% Output: execute_result
$\{-1,0,1,2\}$
{−1,0,1,2}
%% Cell type:code id: tags:
``` prob
:init value=one
```
%%%% Output: execute_result
Executed operation: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:code id: tags:
``` prob
value
```
%%%% Output: execute_result
$1$
1
%% Cell type:code id: tags:
``` prob
:exec add diff=-one
```
%%%% Output: execute_result
Executed operation: add(-1)
%% Cell type:code id: tags:
``` prob
value
```
%%%% Output: execute_result
$0$
0
......
src/main/java/de/prob2/jupyter/ProBKernel.java
View file @ bc7eafab
......@@ -319,7 +319,7 @@ public final class ProBKernel extends BaseKernel {
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Executed operation: %s", op.getRep()));
return new DisplayData(String.format("Executed operation: %s", op.getPrettyRep()));
}
@Override
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment