diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index c2f7f87119fb3d96db2e95f7387f2d2d3c92323b..5fe919980560ebb51b8be5357075a7104290ff41 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -283,8 +283,8 @@
"\u001b[1m\u001b[31mjava.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\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.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -398,7 +398,7 @@
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
"\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m",
- "\u001b[1m\u001b[31mError start line 6 out of bounds (1..1)\u001b[0m"
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
@@ -614,6 +614,31 @@
":exec 10 1=1"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "**Explored States:** 4/9 \n",
+ "**Transitions:** 16"
+ ],
+ "text/plain": [
+ "Explored States: 4/9\n",
+ "Transitions: 16"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":stats"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -623,7 +648,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 26,
"metadata": {},
"outputs": [
{
@@ -635,8 +660,8 @@
"\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\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.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -650,7 +675,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
@@ -662,8 +687,8 @@
"\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\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.InitialiseCommand.run(InitialiseCommand.java:47)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -677,7 +702,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
@@ -689,8 +714,8 @@
"\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.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -704,7 +729,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 29,
"metadata": {},
"outputs": [
{
@@ -716,8 +741,8 @@
"\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.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -731,7 +756,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -740,7 +765,7 @@
"Loaded machine: NoConstants"
]
},
- "execution_count": 29,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -756,7 +781,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
@@ -768,8 +793,8 @@
"\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS\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.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\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",
"\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
"\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
@@ -783,7 +808,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -793,7 +818,7 @@
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
"\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
- "\u001b[1m\u001b[31mError start line 4 out of bounds (1..1)\u001b[0m"
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
@@ -810,7 +835,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -819,7 +844,7 @@
"Loaded machine: Foo"
]
},
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -837,7 +862,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -846,7 +871,7 @@
"Executed operation 2: $setup_constants()"
]
},
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -857,7 +882,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 35,
"metadata": {},
"outputs": [
{
@@ -866,7 +891,7 @@
"Executed operation 7: $initialise_machine()"
]
},
- "execution_count": 34,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -877,7 +902,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
@@ -889,7 +914,7 @@
"1"
]
},
- "execution_count": 35,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
@@ -900,7 +925,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -912,7 +937,7 @@
"2"
]
},
- "execution_count": 36,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index f01fbbcceed8d3df72efa9d10503e13d2645b3eb..0c0269267795ab658ee4396483be58dc60447d3a 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -42,6 +42,7 @@ import de.prob2.jupyter.commands.PrettyPrintCommand;
import de.prob2.jupyter.commands.RenderCommand;
import de.prob2.jupyter.commands.ShowCommand;
import de.prob2.jupyter.commands.SolveCommand;
+import de.prob2.jupyter.commands.StatsCommand;
import de.prob2.jupyter.commands.TableCommand;
import de.prob2.jupyter.commands.TimeCommand;
import de.prob2.jupyter.commands.TraceCommand;
@@ -155,6 +156,7 @@ public final class ProBKernel extends BaseKernel {
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(":stats", injector.getInstance(StatsCommand.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));
diff --git a/src/main/java/de/prob2/jupyter/commands/StatsCommand.java b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..c208bcfd885341e44559b9cf1c897a0252f1847b
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
@@ -0,0 +1,79 @@
+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.command.ComputeStateSpaceStatsCommand;
+import de.prob.check.StateSpaceStats;
+import de.prob.statespace.AnimationSelector;
+
+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 StatsCommand implements Command {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private StatsCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":stats";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Show statistics about the state space.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull String argString) {
+ if (!argString.isEmpty()) {
+ throw new UserErrorException("Expected no arguments");
+ }
+ final ComputeStateSpaceStatsCommand cmd = new ComputeStateSpaceStatsCommand();
+ this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
+ final StateSpaceStats stats = cmd.getResult();
+
+ final StringBuilder sbPlain = new StringBuilder();
+ final StringBuilder sbMarkdown = new StringBuilder();
+
+ sbPlain.append("Explored States: ");
+ sbPlain.append(stats.getNrProcessedNodes());
+ sbPlain.append('/');
+ sbPlain.append(stats.getNrTotalNodes());
+ sbPlain.append('\n');
+ sbMarkdown.append("**Explored States:** ");
+ sbMarkdown.append(stats.getNrProcessedNodes());
+ sbMarkdown.append('/');
+ sbMarkdown.append(stats.getNrTotalNodes());
+ sbMarkdown.append(" \n");
+
+ sbPlain.append("Transitions: ");
+ sbPlain.append(stats.getNrTotalTransitions());
+ sbMarkdown.append("**Transitions:** ");
+ sbMarkdown.append(stats.getNrTotalTransitions());
+
+ 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;
+ }
+}