diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 920481204c5facf14a68cd264a4073a626d4c385..04add0dafb7ffb1ee755d4f93174a1cd0e18b293 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -29,6 +29,7 @@ import de.prob2.jupyter.commands.ConstantsCommand;
import de.prob2.jupyter.commands.DotCommand;
import de.prob2.jupyter.commands.EvalCommand;
import de.prob2.jupyter.commands.ExecCommand;
+import de.prob2.jupyter.commands.GotoCommand;
import de.prob2.jupyter.commands.GroovyCommand;
import de.prob2.jupyter.commands.HelpCommand;
import de.prob2.jupyter.commands.InitialiseCommand;
@@ -42,6 +43,7 @@ import de.prob2.jupyter.commands.ShowCommand;
import de.prob2.jupyter.commands.SolveCommand;
import de.prob2.jupyter.commands.TableCommand;
import de.prob2.jupyter.commands.TimeCommand;
+import de.prob2.jupyter.commands.TraceCommand;
import de.prob2.jupyter.commands.TypeCommand;
import de.prob2.jupyter.commands.VersionCommand;
@@ -150,9 +152,11 @@ public final class ProBKernel extends BaseKernel {
this.commands.put("::load", injector.getInstance(LoadCellCommand.class));
this.commands.put(":pref", injector.getInstance(PrefCommand.class));
this.commands.put(":browse", injector.getInstance(BrowseCommand.class));
+ this.commands.put(":trace", injector.getInstance(TraceCommand.class));
this.commands.put(":exec", injector.getInstance(ExecCommand.class));
this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
+ this.commands.put(":goto", injector.getInstance(GotoCommand.class));
this.commands.put(":show", injector.getInstance(ShowCommand.class));
this.commands.put(":dot", injector.getInstance(DotCommand.class));
this.commands.put(":assert", injector.getInstance(AssertCommand.class));
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..37f8d862a730677c216ed24d4aea9b0d098f09cc
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -0,0 +1,56 @@
+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class GotoCommand implements Command {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private GotoCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":goto INDEX";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Go to the state with the specified index in the current trace.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\nGoing backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull String argString) {
+ final int index = Integer.parseInt(argString);
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ if (index < -1 || index >= trace.size()) {
+ throw new UserErrorException(String.format("Invalid trace index %d, must be in -1..%d", index, trace.size()-1));
+ }
+ this.animationSelector.changeCurrentAnimation(trace.gotoPosition(index));
+ return new DisplayData("Changed to state with index " + index);
+ }
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+ return null;
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..72ff13fe1dfd3e5a9487df6402b2813d0390b039
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -0,0 +1,86 @@
+package de.prob2.jupyter.commands;
+
+import java.util.List;
+
+import com.google.inject.Inject;
+
+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;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class TraceCommand implements Command {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private TraceCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":trace";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Display all states and transitions in the current trace.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\nThe first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull String argString) {
+ if (!argString.isEmpty()) {
+ throw new UserErrorException("Expected no arguments");
+ }
+
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ final StringBuilder sbPlain = new StringBuilder("-1: Root state");
+ final StringBuilder sbMarkdown = new StringBuilder("* -1: Root state");
+
+ if (trace.getCurrent().getIndex() == -1) {
+ sbPlain.append(" (current)");
+ sbMarkdown.append(" **(current)**");
+ }
+
+ final List<Transition> transitionList = trace.getTransitionList();
+ for (int i = 0; i < transitionList.size(); i++) {
+ final Transition transition = transitionList.get(i);
+ sbPlain.append('\n');
+ sbPlain.append(i);
+ sbPlain.append(": ");
+ sbPlain.append(transition);
+ sbMarkdown.append("\n* ");
+ sbMarkdown.append(i);
+ sbMarkdown.append(": ");
+ sbMarkdown.append(transition);
+
+ if (trace.getCurrent().getIndex() == i) {
+ sbPlain.append(" (current)");
+ sbMarkdown.append(" **(current)**");
+ }
+ }
+
+ final DisplayData result = new DisplayData(sbPlain.toString());
+ result.putMarkdown(sbMarkdown.toString());
+ return result;
+ }
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+ return null;
+ }
+}