diff --git a/build.gradle b/build.gradle
index f56043393ff3c268892159169e5b94e4ffc67569..8949c46329eecca3e747f235501620cce4b2527e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -41,6 +41,7 @@ dependencies {
compile(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.2.10-SNAPSHOT", changing: true)
compile(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.0.0-SNAPSHOT", changing: true)
compile(group: "org.jetbrains", name: "annotations", version: "16.0.1")
+ compile(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
}
sourceCompatibility = "1.8"
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index af0e4be8c8c65138ffc3cf59105422fec6d5919d..24c67c813ac16e5b4c57816bab8be085f83c77dd 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -31,8 +31,9 @@
"data": {
"text/plain": [
":exec OPERATION [PREDICATE]\n",
+ ":exec OPERATION_ID\n",
"\n",
- "Execute an operation with the specified predicate"
+ "Execute an operation with the specified predicate, or by its ID"
]
},
"execution_count": 2,
@@ -101,7 +102,8 @@
"Sets: (none)\n",
"Constants: (none)\n",
"Variables: (none)\n",
- "Operations: (none)\n"
+ "Operations: \n",
+ "0: $initialise_machine()"
]
},
"execution_count": 5,
@@ -122,12 +124,12 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-23 12:33:10,169, T+6055] \"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\n",
- "[2018-05-23 12:33:11,574, T+7460] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52196\n",
- "[2018-05-23 12:33:11,575, T+7461] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1828\n",
- "[2018-05-23 12:33:11,580, T+7466] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-05-23 12:33:11,598, T+7484] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
- "[2018-05-23 12:33:11,866, T+7752] \"ProB Output Logger for instance 5b68ad44\" 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])\u001b[0m\n"
+ "[2018-05-23 15:13:10,940, T+6251] \"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\n",
+ "[2018-05-23 15:13:12,528, T+7839] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 56654\n",
+ "[2018-05-23 15:13:12,530, T+7841] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 3008\n",
+ "[2018-05-23 15:13:12,533, T+7844] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-05-23 15:13:12,554, T+7865] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
+ "[2018-05-23 15:13:12,842, T+8153] \"ProB Output Logger for instance 7bd5a630\" 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])\u001b[0m\n"
]
},
{
@@ -163,6 +165,16 @@
"execution_count": 7,
"metadata": {},
"outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-23 15:13:13,175, T+8486] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 120 ms (walltime: 150 ms)\u001b[0m\n",
+ "[2018-05-23 15:13:13,176, T+8487] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n",
+ "[2018-05-23 15:13:13,182, T+8493] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n",
+ "[2018-05-23 15:13:13,183, T+8494] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n"
+ ]
+ },
{
"data": {
"text/plain": [
@@ -170,7 +182,12 @@
"Sets: (none)\n",
"Constants: min_value, max_value\n",
"Variables: value\n",
- "Operations: add(diff)\n"
+ "Operations: \n",
+ "0: $setup_constants()\n",
+ "1: $setup_constants()\n",
+ "2: $setup_constants()\n",
+ "3: $setup_constants()\n",
+ "More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)"
]
},
"execution_count": 7,
@@ -227,7 +244,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-23 12:33:12,406, T+8292] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 80 ms (walltime: 80 ms)\u001b[0m\n"
+ "[2018-05-23 15:13:13,491, T+8802] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 20 ms (walltime: 20 ms)\u001b[0m\n"
]
},
{
@@ -257,7 +274,12 @@
"Sets: (none)\n",
"Constants: min_value, max_value\n",
"Variables: value\n",
- "Operations: add(diff)\n"
+ "Operations: \n",
+ "4: $initialise_machine()\n",
+ "5: $initialise_machine()\n",
+ "6: $initialise_machine()\n",
+ "7: $initialise_machine()\n",
+ "More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)"
]
},
"execution_count": 11,
@@ -316,9 +338,9 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-23 12:33:12,769, T+8655] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n",
- "[2018-05-23 12:33:12,769, T+8655] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n",
- "[2018-05-23 12:33:12,770, T+8656] \"ProB Output Logger for instance 5b68ad44\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n"
+ "[2018-05-23 15:13:13,866, T+9177] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n",
+ "[2018-05-23 15:13:13,867, T+9178] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n",
+ "[2018-05-23 15:13:13,868, T+9179] \"ProB Output Logger for instance 7bd5a630\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n"
]
},
{
@@ -344,7 +366,15 @@
{
"data": {
"text/plain": [
- "2"
+ "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": 15,
@@ -353,7 +383,7 @@
}
],
"source": [
- "value"
+ ":browse"
]
},
{
@@ -364,7 +394,7 @@
{
"data": {
"text/plain": [
- "Executed operation add"
+ "2"
]
},
"execution_count": 16,
@@ -373,7 +403,7 @@
}
],
"source": [
- ":exec add diff=-1"
+ "value"
]
},
{
@@ -384,7 +414,7 @@
{
"data": {
"text/plain": [
- "1"
+ "Executed operation add"
]
},
"execution_count": 17,
@@ -392,9 +422,123 @@
"output_type": "execute_result"
}
],
+ "source": [
+ ":exec add diff=-1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: Counter\n",
+ "Sets: (none)\n",
+ "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)"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
"value"
]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation 15"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec 15"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "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": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "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"
+ ]
}
],
"metadata": {
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index 8a7a6a9d8a7b0ce7a3a2c0aadbac0bb5508d2661..5bf87dcf9efd0862cfd045b813759bf03d63e661 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -1,17 +1,21 @@
package de.prob2.jupyter.commands;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.List;
import java.util.function.Function;
import java.util.stream.Collectors;
import com.google.inject.Inject;
+import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.BEvent;
import de.prob.model.representation.Constant;
import de.prob.model.representation.Set;
import de.prob.model.representation.Variable;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
+import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
@@ -19,6 +23,8 @@ import io.github.spencerpark.jupyter.messages.DisplayData;
import org.jetbrains.annotations.NotNull;
+import se.sawano.java.text.AlphanumericComparator;
+
public final class BrowseCommand implements LineCommand {
private final @NotNull AnimationSelector animationSelector;
@@ -65,8 +71,18 @@ public final class BrowseCommand implements LineCommand {
sb.append("\nVariables: ");
sb.append(elementsToString(mainComponent, Variable.class, Variable::getName));
sb.append("\nOperations: ");
- sb.append(elementsToString(mainComponent, BEvent.class, Object::toString));
- sb.append('\n');
+ final List<Transition> sortedTransitions = new ArrayList<>(trace.getNextTransitions(true, FormulaExpand.TRUNCATE));
+ // 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());
+ }
+ if (trace.getCurrentState().isMaxTransitionsCalculated()) {
+ sb.append("\nMore operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)");
+ }
return new DisplayData(sb.toString());
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 1ad66e57056764724985eddea4e390ea783c4333..384cacd8637992e4f1e9fbd1bd1b0e071b33598f 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -1,6 +1,7 @@
package de.prob2.jupyter.commands;
import java.util.List;
+import java.util.Optional;
import com.google.inject.Inject;
@@ -26,25 +27,39 @@ public final class ExecCommand implements LineCommand {
@Override
public @NotNull String getSyntax() {
- return ":exec OPERATION [PREDICATE]";
+ return ":exec OPERATION [PREDICATE]\n:exec OPERATION_ID";
}
@Override
public @NotNull String getShortHelp() {
- return "Execute an operation with the specified predicate";
+ return "Execute an operation with the specified predicate, or by its ID";
}
@Override
public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull String argString) {
final String[] split = argString.split("\\h", 2);
assert split.length >= 1;
- final String opName = split[0];
- final String predicate = split.length >= 2 ? split[1] : "1=1";
+ final String opNameOrId = split[0];
+
final Trace trace = this.animationSelector.getCurrentTrace();
- final List<Transition> transitions = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), opName, predicate, 1);
- assert transitions.size() == 1;
- final Transition op = transitions.get(0);
+ // 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.length != 1) {
+ throw new CommandExecutionException(name, "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 predicate = split.length >= 2 ? split[1] : "1=1";
+ final List<Transition> transitions = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), opNameOrId, predicate, 1);
+ assert transitions.size() == 1;
+ op = transitions.get(0);
+ }
+
this.animationSelector.changeCurrentAnimation(trace.add(op));
- return new DisplayData(String.format("Executed operation %s", opName));
+ return new DisplayData(String.format("Executed operation %s", opNameOrId));
}
}