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

Fix error messages from ProB not being shown when executing operations 

This fix removes the need for the kernel's custom error messages that
were previously shown.
parent cb55a9c0
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tests/animate.ipynb
+ 76
− 20
View file @ a3c67017
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :browse :help :browse
``` ```
%% Output %% Output
``` ```
:browse :browse
``` ```
Show information about the current state. 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. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition. 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. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition.
``` ```
:browse :browse
``` ```
Show information about the current state. 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. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition. 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. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :exec :help :exec
``` ```
%% Output %% Output
``` ```
:exec OPERATION [PREDICATE] :exec OPERATION [PREDICATE]
:exec OPERATION_ID :exec OPERATION_ID
``` ```
Execute an operation with the specified predicate, or by its ID. Execute an operation with the specified predicate, or by its ID.
In the first form, the given operation is 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. In the first form, the given operation is 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.
In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed. In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed.
``` ```
:exec OPERATION [PREDICATE] :exec OPERATION [PREDICATE]
:exec OPERATION_ID :exec OPERATION_ID
``` ```
Execute an operation with the specified predicate, or by its ID. Execute an operation with the specified predicate, or by its ID.
In the first form, the given operation is 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. In the first form, the given operation is 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.
In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed. In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :constants :help :constants
``` ```
%% Output %% Output
``` ```
:constants [PREDICATE] :constants [PREDICATE]
``` ```
Set up the current machine's constants. Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`. This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
``` ```
:constants [PREDICATE] :constants [PREDICATE]
``` ```
Set up the current machine's constants. Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`. This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :init :help :init
``` ```
%% Output %% Output
``` ```
:init [PREDICATE] :init [PREDICATE]
``` ```
Initialise the current machine with the specified predicate Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`. This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
``` ```
:init [PREDICATE] :init [PREDICATE]
``` ```
Initialise the current machine with the specified predicate Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`. This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: repl Machine: repl
Sets: (none) Sets: (none)
Constants: (none) Constants: (none)
Variables: (none) Variables: (none)
Operations: Operations:
0: $initialise_machine() 0: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Counter MACHINE Counter
CONSTANTS min_value, max_value CONSTANTS min_value, max_value
PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
VARIABLES value VARIABLES value
INVARIANT value : min_value..max_value INVARIANT value : min_value..max_value
INITIALISATION value :: min_value..max_value INITIALISATION value :: min_value..max_value
OPERATIONS OPERATIONS
add(diff) = SELECT add(diff) = SELECT
value+diff : min_value..max_value value+diff : min_value..max_value
THEN THEN
value := value+diff value := value+diff
END END
END END
``` ```
%% Output %% Output
Loaded machine: Counter Loaded machine: Counter
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
0: $setup_constants() 0: $setup_constants()
1: $setup_constants() 1: $setup_constants()
2: $setup_constants() 2: $setup_constants()
3: $setup_constants() 3: $setup_constants()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached) More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
min_value..max_value min_value..max_value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants min_value=5 & max_value=-5 :constants min_value=5 & max_value=-5
``` ```
%% Output %% Output
:constants: Could not setup constants with the specified predicate ---------------------------------------------------------------------------
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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
:constants min_value=-1 & max_value=2 :constants min_value=-1 & max_value=2
``` ```
%% Output %% Output
Machine constants set up using operation 2: $setup_constants() Machine constants set up using operation 2: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
4: $initialise_machine() 4: $initialise_machine()
5: $initialise_machine() 5: $initialise_machine()
6: $initialise_machine() 6: $initialise_machine()
7: $initialise_machine() 7: $initialise_machine()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached) More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
min_value..max_value min_value..max_value
``` ```
%% Output %% Output
$\{-1,0,1,2\}$ $\{-1,0,1,2\}$
{−1,0,1,2} {−1,0,1,2}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init value=-100 :init value=-100
``` ```
%% Output %% Output
Error from ProB: ProB reported Errors 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) Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)
Error start line 6 out of bounds (1..1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init value=2 :init value=2
``` ```
%% Output %% Output
Machine initialised using operation 7: $initialise_machine() Machine initialised using operation 7: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
8: add(-3) 8: add(-3)
9: add(-2) 9: add(-2)
10: add(-1) 10: add(-1)
11: add(0) 11: add(0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec add diff=-1 :exec add diff=-1
``` ```
%% Output %% Output
Executed operation 10: add(-1) Executed operation 10: add(-1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
12: add(-2) 12: add(-2)
13: add(-1) 13: add(-1)
14: add(0) 14: add(0)
15: add(1) 15: add(1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec 15 :exec 15
``` ```
%% Output %% Output
Executed operation 15: add(1) Executed operation 15: add(1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
8: add(-3) 8: add(-3)
9: add(-2) 9: add(-2)
10: add(-1) 10: add(-1)
11: add(0) 11: add(0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec 10 1=1 :exec 10 1=1
``` ```
%% Output %% Output
:exec: Cannot specify a predicate when executing an operation by ID :exec: Cannot specify a predicate when executing an operation by ID
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Useful error messages are shown when an operation cannot be executed. Useful error messages are shown when an operation cannot be executed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
:constants: Machine constants are already set up ---------------------------------------------------------------------------
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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
:init: Machine is already initialised ---------------------------------------------------------------------------
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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
:exec nope :exec nope
``` ```
%% Output %% Output
:exec: Could not execute operation nope ---------------------------------------------------------------------------
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:70)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
:exec add 1=0 :exec add 1=0
``` ```
%% Output %% Output
:exec: Could not execute operation add with the given predicate ---------------------------------------------------------------------------
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:70)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NoConstants MACHINE NoConstants
VARIABLES z VARIABLES z
INVARIANT z : MININT..MAXINT INVARIANT z : MININT..MAXINT
INITIALISATION z :: {0, 1} INITIALISATION z :: {0, 1}
END END
``` ```
%% Output %% Output
Loaded machine: NoConstants Loaded machine: NoConstants
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
:constants: Machine has no constants, use :init instead ---------------------------------------------------------------------------
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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)
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: %% Cell type:code id: tags:
``` prob ``` prob
:init z = -1 :init z = -1
``` ```
%% Output %% Output
Error from ProB: ProB reported Errors 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) Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)
Error start line 4 out of bounds (1..1)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
`SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names. `SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Foo MACHINE Foo
CONSTANTS x CONSTANTS x
PROPERTIES x : MININT..MAXINT PROPERTIES x : MININT..MAXINT
VARIABLES y VARIABLES y
INVARIANT y : MININT..MAXINT INVARIANT y : MININT..MAXINT
INITIALISATION y :: MININT..MAXINT INITIALISATION y :: MININT..MAXINT
END END
``` ```
%% Output %% Output
Loaded machine: Foo Loaded machine: Foo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec SETUP_CONSTANTS x = 1 :exec SETUP_CONSTANTS x = 1
``` ```
%% Output %% Output
Executed operation 2: $setup_constants() Executed operation 2: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec INITIALISATION y = 2 :exec INITIALISATION y = 2
``` ```
%% Output %% Output
Executed operation 7: $initialise_machine() Executed operation 7: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x x
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
y y
``` ```
%% Output %% Output
$2$ $2$
2 2
......
src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+ 4
− 13
View file @ a3c67017
...@@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector; ...@@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace; import de.prob.statespace.Trace;
import de.prob.statespace.Transition; import de.prob.statespace.Transition;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions; import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData; import io.github.spencerpark.jupyter.kernel.display.DisplayData;
...@@ -45,17 +43,10 @@ public final class ConstantsCommand implements Command { ...@@ -45,17 +43,10 @@ public final class ConstantsCommand implements Command {
@Override @Override
public @NotNull DisplayData run(final @NotNull String argString) { public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace(); final Trace trace = this.animationSelector.getCurrentTrace();
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString); final String predicate = argString.isEmpty() ? "1=1" : argString;
final Transition op = trace.getCurrentState().findTransition("$setup_constants", predicates); final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
if (op == null) { assert !ops.isEmpty();
if (trace.gotoPosition(-1).canExecuteEvent("$initialise_machine")) { final Transition op = ops.get(0);
throw new UserErrorException("Machine has no constants, use :init instead");
} else if (trace.getCurrent().getIndex() > -1) {
throw new UserErrorException("Machine constants are already set up");
} else {
throw new UserErrorException("Could not setup constants" + (argString.isEmpty() ? "" : " with the specified predicate"));
}
}
this.animationSelector.changeCurrentAnimation(trace.add(op)); this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); 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())); return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep()));
......
src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+ 4
− 5
View file @ a3c67017
...@@ -66,11 +66,10 @@ public final class ExecCommand implements Command { ...@@ -66,11 +66,10 @@ public final class ExecCommand implements Command {
} else { } else {
// Transition not found, assume that the argument is an operation name instead. // Transition not found, assume that the argument is an operation name instead.
final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId); final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId);
final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1)); final String predicate = split.size() < 2 ? "1=1" : split.get(1);
op = trace.getCurrentState().findTransition(translatedOpName, predicates); final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
if (op == null) { assert !ops.isEmpty();
throw new UserErrorException("Could not execute operation " + opNameOrId + (split.size() < 2 ? "" : " with the given predicate")); op = ops.get(0);
}
} }
this.animationSelector.changeCurrentAnimation(trace.add(op)); this.animationSelector.changeCurrentAnimation(trace.add(op));
......
src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+ 4
− 13
View file @ a3c67017
...@@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector; ...@@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace; import de.prob.statespace.Trace;
import de.prob.statespace.Transition; import de.prob.statespace.Transition;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions; import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData; import io.github.spencerpark.jupyter.kernel.display.DisplayData;
...@@ -45,17 +43,10 @@ public final class InitialiseCommand implements Command { ...@@ -45,17 +43,10 @@ public final class InitialiseCommand implements Command {
@Override @Override
public @NotNull DisplayData run(final @NotNull String argString) { public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace(); final Trace trace = this.animationSelector.getCurrentTrace();
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString); final String predicate = argString.isEmpty() ? "1=1" : argString;
final Transition op = trace.getCurrentState().findTransition("$initialise_machine", predicates); final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
if (op == null) { assert !ops.isEmpty();
if (trace.getCurrentState().isInitialised()) { final Transition op = ops.get(0);
throw new UserErrorException("Machine is already initialised");
} else if (trace.getHead().getPrevious() == null && trace.canExecuteEvent("$setup_constants")) {
throw new UserErrorException("Machine constants are not yet set up, use :constants first");
} else {
throw new UserErrorException("Could not initialise machine" + (argString.isEmpty() ? "" : " with the specified predicate"));
}
}
this.animationSelector.changeCurrentAnimation(trace.add(op)); this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep())); return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment