diff --git a/CHANGELOG.md b/CHANGELOG.md
index 388823233cd06e7f2f4212891272e4d6551c31f7..525292e87267f6a53daabed30a1ca02e1bed77dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,8 @@
## [(next version)](./README.md#for-developers)
+* Updated ProB 2 to version 4.0.0-SNAPSHOT.
+* Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine.
* Significantly refactored the logic for parsing commands and their arguments.
* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
* As a side effect, the inspection and code completion features now work better in a few edge cases.
diff --git a/build.gradle b/build.gradle
index 1d79d7cf24963d26188d0d2756d18eed45a0694b..18edb4d51d3c18078db28e052f6915b91175360d 100644
--- a/build.gradle
+++ b/build.gradle
@@ -39,7 +39,7 @@ configurations.all {
dependencies {
implementation(group: "com.google.code.gson", name: "gson", version: "2.8.6")
implementation(group: "com.google.guava", name: "guava", version: "28.2-jre")
- implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.11.0")
+ implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
implementation(group: "org.jetbrains", name: "annotations", version: "18.0.0")
implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 95e5c6909545b61e580ca3cc28cf2b1f8831b369..8513b96debc84b0cdcd582cac9b53defc2139afe 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -16,6 +16,7 @@ import java.util.Map;
import java.util.Optional;
import java.util.Properties;
import java.util.concurrent.atomic.AtomicReference;
+import java.util.function.Function;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import java.util.stream.Collectors;
@@ -25,10 +26,12 @@ import com.google.inject.Inject;
import com.google.inject.Injector;
import com.google.inject.Singleton;
+import de.prob.animator.ReusableAnimator;
import de.prob.animator.domainobjects.ErrorItem;
import de.prob.exception.ProBError;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
import de.prob2.jupyter.commands.AssertCommand;
import de.prob2.jupyter.commands.BrowseCommand;
@@ -218,6 +221,7 @@ public final class ProBKernel extends BaseKernel {
}
private final @NotNull AnimationSelector animationSelector;
+ private final @NotNull ReusableAnimator animator;
private final @NotNull Map<@NotNull String, @NotNull Command> commands;
private final @NotNull AtomicReference<@Nullable Thread> currentEvalThread;
@@ -226,12 +230,13 @@ public final class ProBKernel extends BaseKernel {
private @NotNull Path currentMachineDirectory;
@Inject
- private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
+ private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector, final @NotNull ReusableAnimator animator) {
super();
this.setShouldReplaceStdStreams(false);
this.animationSelector = animationSelector;
+ this.animator = animator;
this.commands = COMMAND_CLASSES.stream()
.map(injector::getInstance)
@@ -240,7 +245,10 @@ public final class ProBKernel extends BaseKernel {
this.currentEvalThread = new AtomicReference<>(null);
this.variables = new HashMap<>();
- this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
+ this.switchMachine(Paths.get(""), stateSpace -> {
+ classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").loadIntoStateSpace(stateSpace);
+ return new Trace(stateSpace);
+ });
this.currentMachineDirectory = Paths.get("");
}
@@ -272,6 +280,28 @@ public final class ProBKernel extends BaseKernel {
this.currentMachineDirectory = currentMachineDirectory;
}
+ public void unloadMachine() {
+ final Trace oldTrace = this.animationSelector.getCurrentTrace();
+ if (oldTrace != null) {
+ assert oldTrace.getStateSpace() == this.animator.getCurrentStateSpace();
+ this.animationSelector.changeCurrentAnimation(null);
+ oldTrace.getStateSpace().kill();
+ }
+ this.setCurrentMachineDirectory(Paths.get(""));
+ }
+
+ public void switchMachine(final @NotNull Path machineDirectory, final @NotNull Function<@NotNull StateSpace, @NotNull Trace> newTraceCreator) {
+ this.unloadMachine();
+ final StateSpace newStateSpace = this.animator.createStateSpace();
+ try {
+ this.animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace));
+ } catch (final RuntimeException e) {
+ newStateSpace.kill();
+ throw e;
+ }
+ this.setCurrentMachineDirectory(machineDirectory);
+ }
+
@Override
public @NotNull String getBanner() {
return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index cc5a928295dd370a6a3b588d108bb5a113443b22..b0525f60c7e1838f8411eef1e099054590ff722c 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -77,10 +77,13 @@ public final class LoadCellCommand implements Command {
final String body = args.get(CODE_PARAM);
final Map<String, String> preferences = CommandUtils.parsePreferences(args.get(PREFS_PARAM));
- this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () ->
- this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)
- )));
- this.proBKernelProvider.get().setCurrentMachineDirectory(Paths.get(""));
+ this.proBKernelProvider.get().switchMachine(Paths.get(""), stateSpace -> {
+ stateSpace.changePreferences(preferences);
+ CommandUtils.withSourceCode(body, () ->
+ this.classicalBFactory.create("(machine from Jupyter cell)", body).loadIntoStateSpace(stateSpace)
+ );
+ return new Trace(stateSpace);
+ });
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
}
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index ccb1456850bf696d1d6a52670a71f013fb51739b..b1cccf91638c0df1086741a676c4c162567568f3 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -101,13 +101,16 @@ public final class LoadFileCommand implements Command {
}
final Map<String, String> preferences = CommandUtils.parsePreferences(args.get(PREFS_PARAM));
- try {
- final ModelFactory<?> factory = this.injector.getInstance(FactoryProvider.factoryClassFromExtension(extension));
- this.animationSelector.changeCurrentAnimation(new Trace(factory.extract(machineFilePath.toString()).load(preferences)));
- this.proBKernelProvider.get().setCurrentMachineDirectory(machineFileDirectory);
- } catch (IOException | ModelTranslationError e) {
- throw new RuntimeException(e);
- }
+ final ModelFactory<?> factory = this.injector.getInstance(FactoryProvider.factoryClassFromExtension(extension));
+ this.proBKernelProvider.get().switchMachine(machineFileDirectory, stateSpace -> {
+ stateSpace.changePreferences(preferences);
+ try {
+ factory.extract(machineFilePath.toString()).loadIntoStateSpace(stateSpace);
+ } catch (final IOException | ModelTranslationError e) {
+ throw new RuntimeException(e);
+ }
+ return new Trace(stateSpace);
+ });
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
}