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

Remove ability to execute transitions by ID 

Transition IDs are not necessarily stable across multiple runs, so it's
not a good idea to depend on them in a notebook.
parent 9bf39a3a
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tests/animate.ipynb
+ 47
− 119
View file @ 7c3fc0a6
%% 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. 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.
```
: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. 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.
%% 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.
Execute an operation.
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.
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]
:exec OPERATION_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.
Execute an operation.
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.
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:
0: $initialise_machine()
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:
0: $setup_constants()
1: $setup_constants()
2: $setup_constants()
3: $setup_constants()
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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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:
4: $initialise_machine()
5: $initialise_machine()
6: $initialise_machine()
7: $initialise_machine()
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:
8: add(-3)
9: add(-2)
10: add(-1)
11: add(0)
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 10: add(-1)
Executed operation: 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)
add(-2)
add(-1)
add(0)
add(1)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
$1$
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: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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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:70)
at de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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:70)
at de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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:47)
at de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)
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:
``` 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 2: $setup_constants()
Executed operation: $setup_constants()
%% Cell type:code id: tags:
``` prob
:exec INITIALISATION y = 2
```
%% Output
Executed operation 7: $initialise_machine()
Executed operation: $initialise_machine()
%% Cell type:code id: tags:
``` prob
x
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
y
```
%% Output
$2$
2
......
src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+ 3
− 4
View file @ 7c3fc0a6
......@@ -44,7 +44,7 @@ public final class BrowseCommand implements Command {
@Override
public @NotNull String getHelpBody() {
return "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.";
return "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.";
}
private static @NotNull String listToString(final List<String> list) {
......@@ -69,13 +69,12 @@ public final class BrowseCommand implements Command {
sb.append(listToString(lm.getVariableNames()));
sb.append("\nOperations: ");
final List<Transition> sortedTransitions = new ArrayList<>(trace.getNextTransitions(true, FormulaExpand.TRUNCATE));
// Sort transitions by ID to get a consistent ordering.
// Transition IDs are strings, but they almost always contain numbers.
sortedTransitions.sort(Comparator.comparing(Transition::getId, new AlphanumericComparator()));
for (final Transition t : sortedTransitions) {
sb.append('\n');
sb.append(t.getId());
sb.append(": ");
sb.append(t.getRep());
sb.append(t.getPrettyRep());
}
if (trace.getCurrentState().isMaxTransitionsCalculated()) {
sb.append("\nMore operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)");
......
src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+ 12
− 29
View file @ 7c3fc0a6
......@@ -2,10 +2,8 @@ package de.prob2.jupyter.commands;
import java.util.Collections;
import java.util.List;
import java.util.Optional;
import java.util.regex.Matcher;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import com.google.inject.Inject;
......@@ -14,8 +12,6 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
......@@ -33,48 +29,34 @@ public final class ExecCommand implements Command {
@Override
public @NotNull String getSyntax() {
return ":exec OPERATION [PREDICATE]\n:exec OPERATION_ID";
return ":exec OPERATION [PREDICATE]";
}
@Override
public @NotNull String getShortHelp() {
return "Execute an operation with the specified predicate, or by its ID.";
return "Execute an operation.";
}
@Override
public @NotNull String getHelpBody() {
return "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.\n\n"
+ "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.";
return "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.";
}
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final List<String> split = CommandUtils.splitArgs(argString, 2);
assert !split.isEmpty();
final String opNameOrId = split.get(0);
final Trace trace = this.animationSelector.getCurrentTrace();
// Check if the argument is an ID, by searching for a transition with that ID.
final Optional<Transition> opt = trace.getNextTransitions().stream().filter(t -> t.getId().equals(opNameOrId)).findAny();
final Transition op;
if (opt.isPresent()) {
// Transition found, nothing else needs to be done.
if (split.size() != 1) {
throw new UserErrorException("Cannot specify a predicate when executing an operation by ID");
}
op = opt.get();
} else {
// Transition not found, assume that the argument is an operation name instead.
final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId);
final String translatedOpName = CommandUtils.unprettyOperationName(split.get(0));
final String predicate = split.size() < 2 ? "1=1" : split.get(1);
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
assert !ops.isEmpty();
op = ops.get(0);
}
final Transition op = ops.get(0);
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Executed operation %s: %s", op.getId(), op.getRep()));
return new DisplayData(String.format("Executed operation: %s", op.getRep()));
}
@Override
......@@ -92,12 +74,13 @@ public final class ExecCommand implements Command {
final ReplacementOptions replacements = CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString.substring(opNameEnd), at - opNameEnd);
return CommandUtils.offsetReplacementOptions(replacements, opNameEnd);
} else {
// Cursor is in the first part of the arguments, provide possible operation names and transition IDs.
// Cursor is in the first part of the arguments, provide possible operation names.
final String prefix = argString.substring(0, at);
final List<String> opNames = this.animationSelector.getCurrentTrace()
.getNextTransitions()
.stream()
.flatMap(t -> Stream.of(CommandUtils.prettyOperationName(t.getName()), t.getId()))
.map(Transition::getName)
.map(CommandUtils::prettyOperationName)
.distinct()
.filter(s -> s.startsWith(prefix))
.sorted()
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment