Add :browse command to view the current state (#15)

notebooks/tests/exec.ipynb → notebooks/tests/animate.ipynb

@@ -4,6 +4,28 @@
    "cell_type": "code",
    "execution_count": 1,
    "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       ":browse\n",
+       "\n",
+       "Show information about the current state"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":help :browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -13,7 +35,7 @@
        "Execute an operation with the specified predicate"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -24,19 +46,43 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: repl\n",
+       "Sets: (none)\n",
+       "Constants: (none)\n",
+       "Variables: (none)\n",
+       "Operations: (none)\n"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "[2018-05-16 14:33:33,768, T+5453] \"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-16 14:33:35,223, T+6908] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55956\n",
-      "[2018-05-16 14:33:35,225, T+6910] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2510\n",
-      "[2018-05-16 14:33:35,228, T+6913] \"ProB Output Logger for instance 5f27dee3\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
-      "[2018-05-16 14:33:35,251, T+6936] \"ProB Output Logger for instance 5f27dee3\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
-      "[2018-05-16 14:33:35,524, T+7209] \"ProB Output Logger for instance 5f27dee3\" 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-16 15:24:23,150, T+8559] \"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-16 15:24:24,859, T+10268] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 60969\n",
+      "[2018-05-16 15:24:24,860, T+10269] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2734\n",
+      "[2018-05-16 15:24:24,866, T+10275] \"ProB Output Logger for instance 5602ac4c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+      "[2018-05-16 15:24:24,881, T+10290] \"ProB Output Logger for instance 5602ac4c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
+      "[2018-05-16 15:24:25,134, T+10543] \"ProB Output Logger for instance 5602ac4c\" 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"
      ]
     },
     {
@@ -45,7 +91,7 @@
        "Loaded machine: Counter : []\n"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -67,7 +113,31 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine: Counter\n",
+       "Sets: (none)\n",
+       "Constants: (none)\n",
+       "Variables: value\n",
+       "Operations: add(diff)\n"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
    "metadata": {},
    "outputs": [
     {
@@ -85,16 +155,16 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "[2018-05-16 14:33:35,862, T+7547] \"ProB Output Logger for instance 5f27dee3\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n",
-      "[2018-05-16 14:33:35,863, T+7548] \"ProB Output Logger for instance 5f27dee3\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n",
-      "[2018-05-16 14:33:35,864, T+7549] \"ProB Output Logger for instance 5f27dee3\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n"
+      "[2018-05-16 15:24:25,522, T+10931] \"ProB Output Logger for instance 5602ac4c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n",
+      "[2018-05-16 15:24:25,523, T+10932] \"ProB Output Logger for instance 5602ac4c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n",
+      "[2018-05-16 15:24:25,524, T+10933] \"ProB Output Logger for instance 5602ac4c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n"
      ]
     },
     {
@@ -103,7 +173,7 @@
        "Executed operation $initialise_machine"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 7,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -114,7 +184,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -123,7 +193,7 @@
        "2"
       ]
      },
-     "execution_count": 5,
+     "execution_count": 8,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -134,7 +204,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 9,
    "metadata": {},
    "outputs": [
     {
@@ -143,7 +213,7 @@
        "Executed operation add"
       ]
      },
-     "execution_count": 6,
+     "execution_count": 9,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -154,7 +224,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
@@ -163,7 +233,7 @@
        "1"
       ]
      },
-     "execution_count": 7,
+     "execution_count": 10,
      "metadata": {},
      "output_type": "execute_result"
     }

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -21,6 +21,7 @@ import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.unicode.UnicodeTranslator;
 
+import de.prob2.jupyter.commands.BrowseCommand;
 import de.prob2.jupyter.commands.CellCommand;
 import de.prob2.jupyter.commands.ExecCommand;
 import de.prob2.jupyter.commands.GroovyCommand;
@@ -63,6 +64,7 @@ public final class ProBKernel extends BaseKernel {
 		this.lineCommands.put(":help", help);
 		this.lineCommands.put(":load", injector.getInstance(LoadFileCommand.class));
 		this.lineCommands.put(":pref", injector.getInstance(PrefCommand.class));
+		this.lineCommands.put(":browse", injector.getInstance(BrowseCommand.class));
 		this.lineCommands.put(":exec", injector.getInstance(ExecCommand.class));
 		this.lineCommands.put(":groovy", injector.getInstance(GroovyCommand.class));
 		

src/main/java/de/prob2/jupyter/commands/BrowseCommand.java

+package de.prob2.jupyter.commands;
+
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+import com.google.inject.Inject;
+
+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.prob2.jupyter.ProBKernel;
+
+import io.github.spencerpark.jupyter.messages.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class BrowseCommand implements LineCommand {
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private BrowseCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":browse";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Show information about the current state";
+	}
+	
+	private static <T extends AbstractElement> @NotNull String elementsToString(
+		final @NotNull AbstractElement element,
+		final @NotNull Class<T> clazz,
+		final @NotNull Function<@NotNull T, @NotNull String> func
+	) {
+		final String elements = element.getChildrenOfType(clazz).stream().map(func).collect(Collectors.joining(", "));
+		return elements.isEmpty() ? "(none)" : elements;
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull String argString) {
+		if (!argString.isEmpty()) {
+			throw new CommandExecutionException(name, "Unexpected argument: " + argString);
+		}
+		
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		final StringBuilder sb = new StringBuilder("Machine: ");
+		final AbstractElement mainComponent = trace.getStateSpace().getMainComponent();
+		sb.append(mainComponent);
+		sb.append("\nSets: ");
+		sb.append(elementsToString(mainComponent, Set.class, Set::getName));
+		sb.append("\nConstants: ");
+		sb.append(elementsToString(mainComponent, Constant.class, Object::toString));
+		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');
+		return new DisplayData(sb.toString());
+	}
+}