Skip to content
Snippets Groups Projects
Commit 9359f89b authored by Michael Leuschel's avatar Michael Leuschel
Browse files

Merge branch 'master' of gitlab.cs.uni-duesseldorf.de:dgelessus/prob2-jupyter-kernel

parents ecdcfea9 44b9eef1
Branches
Tags
No related merge requests found
%% Cell type:code id: tags:
``` prob
:help :browse
```
%% Output
```
:browse
```
Show information about the current state
:browse
Show information about the current state
%% Cell type:code id: tags:
``` prob
:help :exec
```
%% Output
```
:exec OPERATION [PREDICATE]
:exec OPERATION_ID
```
Execute an operation with the specified predicate, or by its ID
:exec OPERATION [PREDICATE]
:exec OPERATION_ID
Execute an operation with the specified predicate, or by its ID
%% Cell type:code id: tags:
``` prob
:help :constants
```
%% Output
```
:constants [PREDICATE]
```
Set up the current machine's constants with the specified predicate
:constants [PREDICATE]
Set up the current machine's constants with the specified predicate
%% Cell type:code id: tags:
``` prob
:help :init
```
%% Output
```
:initialise [PREDICATE]
:init [PREDICATE]
```
Initialise the current machine with the specified predicate
:initialise [PREDICATE]
:init [PREDICATE]
Initialise the current machine with the specified predicate
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: repl
Sets: (none)
Constants: (none)
Variables: (none)
Operations:
0: $initialise_machine()
%% 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
[2018-05-23 15:21:30,908, T+6149] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-23 15:21:32,323, T+7564] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57370
[2018-05-23 15:21:32,325, T+7566] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 3128
[2018-05-23 15:21:32,327, T+7568] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-23 15:21:32,346, T+7587] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-23 15:21:32,610, T+7851] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 13:34:59.07),Counter,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests])
[2018-06-04 12:13:17,947, T+13580] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-06-04 12:13:19,470, T+15103] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52560
[2018-06-04 12:13:19,472, T+15105] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1092
[2018-06-04 12:13:19,480, T+15113] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-06-04 12:13:19,507, T+15140] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
Loaded machine: Counter : []
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
[2018-05-23 15:21:32,861, T+8102] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 90 ms (walltime: 90 ms)
[2018-05-23 15:21:32,862, T+8103] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-05-23 15:21:32,863, T+8104] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-05-23 15:21:32,863, T+8104] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:20,152, T+15785] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 100 ms (walltime: 100 ms)
[2018-06-04 12:13:20,153, T+15786] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:20,153, T+15786] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:20,154, T+15787] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
0: $setup_constants()
1: $setup_constants()
2: $setup_constants()
3: $setup_constants()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%% Output
NOT-INITIALISED
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
value
```
%% Output
NOT-INITIALISED
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:constants min_value=5 & max_value=-5
```
%% Output
[2018-06-04 12:13:20,510, T+16143] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime to FINALISE SETUP_CONSTANTS: 20 ms (walltime: 20 ms)
:constants: Could not setup constants with the specified predicate
%% Cell type:code id: tags:
``` prob
:constants min_value=-1 & max_value=2
```
%% Output
[2018-05-23 15:21:33,128, T+8369] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 20 ms (walltime: 20 ms)
[2018-06-04 12:13:20,595, T+16228] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
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:
4: $initialise_machine()
5: $initialise_machine()
6: $initialise_machine()
7: $initialise_machine()
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}
%% Cell type:code id: tags:
``` prob
value
```
%% Output
NOT-INITIALISED
:eval: NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:init value=-100
```
%% Output
[2018-06-04 12:13:21,030, T+16663] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-06-04 12:13:21,031, T+16664] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(initialisation_fails)
[2018-06-04 12:13:21,032, T+16665] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! INITIALISATION FAILS
[2018-06-04 12:13:21,045, T+16678] "Shell-0" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:105): [ERROR] ProB raised exception(s):
[2018-06-04 12:13:21,049, T+16682] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Line: 6 Column: 15 until 44 in file: /Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests
[2018-06-04 12:13:21,047, T+16680] "Shell-0" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:107): [ERROR] Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:6:15 to 6:44)
---------------------------------------------------------------------------
de.prob.exception.ProBError: ProB reported Errors
ProB returned error messages:
Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:6:15 to 6:44)
at de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:137)
at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:81)
at de.prob.statespace.StateSpace.execute(StateSpace.java:549)
at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:277)
at de.prob.statespace.State.findTransitions(State.java:153)
at de.prob.statespace.State.findTransition(State.java:136)
at de.prob2.jupyter.commands.InitialiseCommand.run(InitialiseCommand.java:44)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:98)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:113)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)
%% Cell type:code id: tags:
``` prob
:init value=2
```
%% Output
[2018-05-23 15:21:33,520, T+8761] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-05-23 15:21:33,520, T+8761] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED
[2018-05-23 15:21:33,521, T+8762] "ProB Output Logger for instance 3145296" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-06-04 12:13:21,224, T+16857] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-06-04 12:13:21,226, T+16859] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED
[2018-06-04 12:13:21,226, T+16859] "ProB Output Logger for instance 27a0802c" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
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:
8: add(-3)
9: add(-2)
10: add(-1)
11: add(0)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
2
%% Cell type:code id: tags:
``` prob
:exec add diff=-1
```
%% Output
Executed operation 10: add(-1)
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
12: add(-2)
13: add(-1)
14: add(0)
15: add(1)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
1
%% Cell type:code id: tags:
``` prob
:exec 15
```
%% Output
Executed operation 15: add(1)
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
8: add(-3)
9: add(-2)
10: add(-1)
11: add(0)
%% Cell type:code id: tags:
``` prob
:exec 10 1=1
```
%% Output
:exec: Cannot specify a predicate when executing an operation by ID
%% Cell type:markdown id: tags:
Useful error messages are shown when an operation cannot be executed.
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
:constants: Could not setup constants
%% Cell type:code id: tags:
``` prob
:constants 1=1
```
%% Output
:constants: Could not setup constants with the specified predicate
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
:init: Could not initialise machine
%% Cell type:code id: tags:
``` prob
:init 1=1
```
%% Output
:init: Could not initialise machine with the specified predicate
%% Cell type:code id: tags:
``` prob
:exec nope
```
%% Output
:exec: Could not execute operation nope
%% Cell type:code id: tags:
``` prob
:exec add 1=0
```
%% Output
:exec: Could not execute operation add with the given predicate
%% 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
[2018-06-04 12:13:22,299, T+17932] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-06-04 12:13:23,889, T+19522] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52592
[2018-06-04 12:13:23,890, T+19523] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1096
[2018-06-04 12:13:23,909, T+19542] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-06-04 12:13:23,922, T+19555] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-06-04 12:13:24,268, T+19901] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % unused_constants(1,[x])
Loaded machine: Foo : []
%% Cell type:code id: tags:
``` prob
:exec SETUP_CONSTANTS x = 1
```
%% Output
[2018-06-04 12:13:24,473, T+20106] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 80 ms (walltime: 90 ms)
[2018-06-04 12:13:24,474, T+20107] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:24,474, T+20107] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:24,475, T+20108] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-06-04 12:13:24,537, T+20170] "ProB Output Logger for instance 2120e79e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 20 ms (walltime: 30 ms)
Executed operation 2: $setup_constants()
%% Cell type:code id: tags:
``` prob
:exec INITIALISATION y = 2
```
%% Output
Executed operation 7: $initialise_machine()
%% Cell type:code id: tags:
``` prob
x
```
%% Output
1
%% Cell type:code id: tags:
``` prob
y
```
%% Output
2
......
......@@ -11,6 +11,7 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -41,6 +42,9 @@ public final class ConstantsCommand implements Command {
final Trace trace = this.animationSelector.getCurrentTrace();
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
final Transition op = trace.getCurrentState().findTransition("$setup_constants", predicates);
if (op == null) {
throw new UserErrorException("Could not setup constants" + (argString.isEmpty() ? "" : " with the specified predicate"));
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep()));
......
......@@ -56,8 +56,19 @@ public final class ExecCommand implements Command {
op = opt.get();
} else {
// Transition not found, assume that the argument is an operation name instead.
final String translatedOpName;
if ("SETUP_CONSTANTS".equals(opNameOrId)) {
translatedOpName = "$setup_constants";
} else if ("INITIALISATION".equals(opNameOrId)) {
translatedOpName = "$initialise_machine";
} else {
translatedOpName = opNameOrId;
}
final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1));
op = trace.getCurrentState().findTransition(opNameOrId, predicates);
op = trace.getCurrentState().findTransition(translatedOpName, predicates);
if (op == null) {
throw new UserErrorException("Could not execute operation " + opNameOrId + (split.size() < 2 ? "" : " with the given predicate"));
}
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
......
......@@ -11,6 +11,7 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -41,6 +42,9 @@ public final class InitialiseCommand implements Command {
final Trace trace = this.animationSelector.getCurrentTrace();
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
final Transition op = trace.getCurrentState().findTransition("$initialise_machine", predicates);
if (op == null) {
throw new UserErrorException("Could not initialise machine" + (argString.isEmpty() ? "" : " with the specified predicate"));
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment