diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 5fe919980560ebb51b8be5357075a7104290ff41..ca4c457eb86a5f88411a45bd0ceb66dc53d72e18 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -14,7 +14,7 @@
"\n",
"Show information about the current state.\n",
"\n",
- "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."
],
"text/plain": [
"```\n",
@@ -23,7 +23,7 @@
"\n",
"Show information about the current state.\n",
"\n",
- "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."
]
},
"execution_count": 1,
@@ -45,26 +45,20 @@
"text/markdown": [
"```\n",
":exec OPERATION [PREDICATE]\n",
- ":exec OPERATION_ID\n",
"```\n",
"\n",
- "Execute an operation with the specified predicate, or by its ID.\n",
+ "Execute an operation.\n",
"\n",
- "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."
+ "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."
],
"text/plain": [
"```\n",
":exec OPERATION [PREDICATE]\n",
- ":exec OPERATION_ID\n",
"```\n",
"\n",
- "Execute an operation with the specified predicate, or by its ID.\n",
- "\n",
- "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",
+ "Execute an operation.\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."
+ "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."
]
},
"execution_count": 2,
@@ -159,7 +153,7 @@
"Constants: (none)\n",
"Variables: (none)\n",
"Operations: \n",
- "0: $initialise_machine()"
+ "INITIALISATION()"
]
},
"execution_count": 5,
@@ -217,10 +211,10 @@
"Constants: min_value, max_value\n",
"Variables: value\n",
"Operations: \n",
- "0: $setup_constants()\n",
- "1: $setup_constants()\n",
- "2: $setup_constants()\n",
- "3: $setup_constants()\n",
+ "SETUP_CONSTANTS()\n",
+ "SETUP_CONSTANTS()\n",
+ "SETUP_CONSTANTS()\n",
+ "SETUP_CONSTANTS()\n",
"More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)"
]
},
@@ -329,10 +323,10 @@
"Constants: min_value, max_value\n",
"Variables: value\n",
"Operations: \n",
- "4: $initialise_machine()\n",
- "5: $initialise_machine()\n",
- "6: $initialise_machine()\n",
- "7: $initialise_machine()\n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
"More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)"
]
},
@@ -439,10 +433,10 @@
"Constants: min_value, max_value\n",
"Variables: value\n",
"Operations: \n",
- "8: add(-3)\n",
- "9: add(-2)\n",
- "10: add(-1)\n",
- "11: add(0)"
+ "add(-3)\n",
+ "add(-2)\n",
+ "add(-1)\n",
+ "add(0)"
]
},
"execution_count": 17,
@@ -485,7 +479,7 @@
{
"data": {
"text/plain": [
- "Executed operation 10: add(-1)"
+ "Executed operation: add(-1)"
]
},
"execution_count": 19,
@@ -510,10 +504,10 @@
"Constants: min_value, max_value\n",
"Variables: value\n",
"Operations: \n",
- "12: add(-2)\n",
- "13: add(-1)\n",
- "14: add(0)\n",
- "15: add(1)"
+ "add(-2)\n",
+ "add(-1)\n",
+ "add(0)\n",
+ "add(1)"
]
},
"execution_count": 20,
@@ -552,72 +546,6 @@
"cell_type": "code",
"execution_count": 22,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "Executed operation 15: add(1)"
- ]
- },
- "execution_count": 22,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":exec 15"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 23,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "Machine: Counter\n",
- "Sets: (none)\n",
- "Constants: min_value, max_value\n",
- "Variables: value\n",
- "Operations: \n",
- "8: add(-3)\n",
- "9: add(-2)\n",
- "10: add(-1)\n",
- "11: add(0)"
- ]
- },
- "execution_count": 23,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":browse"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 24,
- "metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":exec: Cannot specify a predicate when executing an operation by ID",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:exec: Cannot specify a predicate when executing an operation by ID\u001b[0m"
- ]
- }
- ],
- "source": [
- ":exec 10 1=1"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 25,
- "metadata": {},
"outputs": [
{
"data": {
@@ -630,7 +558,7 @@
"Transitions: 16"
]
},
- "execution_count": 25,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -648,7 +576,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 23,
"metadata": {},
"outputs": [
{
@@ -675,7 +603,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 24,
"metadata": {},
"outputs": [
{
@@ -702,7 +630,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 25,
"metadata": {},
"outputs": [
{
@@ -713,7 +641,7 @@
"\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:70)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)\u001b[0m",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m",
@@ -729,7 +657,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 26,
"metadata": {},
"outputs": [
{
@@ -740,7 +668,7 @@
"\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:70)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:226)\u001b[0m",
"\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:249)\u001b[0m",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m",
@@ -756,7 +684,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
@@ -765,7 +693,7 @@
"Loaded machine: NoConstants"
]
},
- "execution_count": 30,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -781,7 +709,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
@@ -808,7 +736,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 29,
"metadata": {},
"outputs": [
{
@@ -835,7 +763,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -844,7 +772,7 @@
"Loaded machine: Foo"
]
},
- "execution_count": 33,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -862,16 +790,16 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Executed operation 2: $setup_constants()"
+ "Executed operation: $setup_constants()"
]
},
- "execution_count": 34,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -882,16 +810,16 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Executed operation 7: $initialise_machine()"
+ "Executed operation: $initialise_machine()"
]
},
- "execution_count": 35,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -902,7 +830,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -914,7 +842,7 @@
"1"
]
},
- "execution_count": 36,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -925,7 +853,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -937,7 +865,7 @@
"2"
]
},
- "execution_count": 37,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index c95f78d9c3dc17e9c8ba4e593afd234ce411fd28..d6b8d353cf4b894572bc360f75fb5ee08a8a39b2 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -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)");
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 75453e702fac5ba0b3f1be75570646a504576fc3..8d679fc0386dbb89e838ef3597e2b561409bbf39 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -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 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 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();
+ 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()